You are viewing zelych

?!

> recent entries
> calendar
> friends
> profile
> previous 20 entries

Monday, August 10th, 2020
11:58 am - Библиотека
У меня собралось несколько книжек, которые не в каждом московском магазине можно купить.
Сам я их не каждый день читаю, а книжкам обидно лежать мёртвым грузом на полке.
Поэтому могу дать кому-нибудь на почитать.
изрядно устаревший списокCollapse )

Как получить книжку:
* сообщить мне свою контактную информацию
* и когда обещаете вернуть
* встретиться (я живу в Москве, бываю в Питере)
* сказать: "Мамой клянусь, отдам!"

(6 comments | comment on this)

Sunday, September 14th, 2014
10:56 pm - CNF shuffling
Читаю замечательную книжку Algebraic Cryptanalysis by Gregory V. Bard.
В ней мимоходом одним предложением упоминается, что скорость решения SAT радикально зависит от порядка дизъюнктов в формуле.
Я выкачал бенчмарки из http://satcompetition.org/2014/ и провёл несколько экспериментов с lingeling и minisat.
Действительно, простой sort -R может на пару порядков ускорить решение.

Думаю, что задача поиска оптимальной перестановки как минимум не проще исходной SAT, поэтому возможность практического применения этого забавного эффекта не очевидна.
Read more...Collapse )

(3 comments | comment on this)

Tuesday, September 2nd, 2014
4:21 pm - coq детям
Воеводский на днях в coq.club написал:

I have this idea that it would be good to:
1. Make a webpage for school kids where they could register, learn some basic Coq, and solve problems (in Coq).
2. To organize a camp where the winners (those who solved most problems) could go - some with stipends and some paying money.
3. Have such camps also organized by other people in other countries.
4. Eventually to have a network which will bring talented young people into math through formal proofs.

Мне кажется у идеи отличное будущее: интерактивные доказательства затягивают не хуже игрушек. Особенно если добавить к этому всякие рейтинги, экспу и бейджики.

(2 comments | comment on this)

Friday, August 1st, 2014
4:17 pm - про ghc немножко
На днях в haskell-russian случился небольшой срачик в результате которого моё представление об устройстве мира было безнадёжно подорвано и теперь я в недоумении. Поэтому хочу зафиксировать.
Read more...Collapse )

(6 comments | comment on this)

Thursday, July 31st, 2014
2:31 am - внезапно
seL4 открыли под GPL: http://sel4.systems/

The release happened at noon of Tuesday, 29 July 2014 AEST (UTC+10), in celebration of International Proof Day (the fifth aniversary of the completion of seL4's functional correctness proof).

(comment on this)

Monday, June 9th, 2014
12:09 am
Продолжение http://zelych.livejournal.com/21224.html.

Методы решения нелинейных систем над конечными полями активно исследуются в алгебраическом криптоанализе. Но, похоже, что общие методы к таким большим системам не применимы (в тех статьях что я видел, системы были с <10k переменных).
Приведённая в прошлом посте система слабо связная, можно попробовать как-нибудь её divide & conquer. Например, поделить на подсистемы. Т.е. как-то сгруппировать уравнения, решить каждую подсистему отдельно и потом что-нибудь с этими решениями сделать.

Приятно, если у каждой подсистемы будет не так много решений (чтобы можно было их компактно хранить и быстро обрабатывать). Т.е., предположительно, нужно сгруппировать уравнения так, чтобы минимизировать призведение количества решений в группах.

Совершенно не понятно как это делать, но можно попробовать жадную стратегию:
 - выбираем случайное уравнение, добавлем в группу;
 - вычисляем grpVars -- множество переменных встречающихся в группе;
 - из уравнений не включённых в группы, находим такое у которого максимально пересечение можества встречающихся в нём переменных и grpVars;
 - добавляем уравнение в группу;
 - продолжаем таким образом расширять группу, пока она не достигнет какого-то заранее заданного размера (по количеству уравнений или по числу используемых переменных).

Предположительно, должны получиться группы, которые друг с другом слабо связаны общими переменными. Т.е. например если какая-то переменная встречается всего 5 раз, то хорошо, если все 5 этих уравнений будут в одной группе.

(comment on this)

Saturday, June 7th, 2014
4:08 pm
Есть система нелинейных уравнений над GF(2). Нужно эту систему как-то преобразовать чтобы можно было быстро отвечать на серию запросов вида: "Зафиксируем значения некоторых переменных. Если существует решение системы с такими значениями переменных, тогда покажите мне значения некоторых других переменных из этого решения".

Пример такой системы вот тут: https://github.com/jorpic/xxx/blob/master/system.eqs
В ней 131387 уравнений и 131843 переменных.
Ниже распределения числа мономов и переменных в уравнениях и степеней уравнений.


Видно что половина уравнений линейные и почти все состоят из четырёх слагаемых.

Система описывает свойства некоторого устройства -- оно в цикле обрабатывает какие-то данные и у него очень мало памяти. Из-за этого система имеет странный вид: бо́льшая часть переменных используется лишь в нескольких уравнениях.

(5 comments | comment on this)

Wednesday, June 4th, 2014
2:15 pm - Как забанить тор в биткоин-сети
По мотивам Deanonymisation of clients in Bitcoin P2P network by Biryukov, Khovratovich, Pustogarov.

Стандартная реализация биткоин-протокола bitcoind имеет защиту от DoS атак. Для этого, во-первых, узлы не передают неформатные транзакции и блоки дальше по сети, а во-вторых, они отслеживают от каких пиров приходят неформатные данные и банят их.

Т.е. когда по соединению приходит неправильное сообщение, для этого соединения увеличивается счётчик штрафов. Когда он достигает сотни, соединение обрывается и узел банит входящие соединения от того же IP на 24 часа.

Для разных сообщений разные штрафы, если приходит блок без транзакций, то соединение банится сразу же.

Дальше мы из тора подключаемся к узлам биткоин-сети (их около 10 тысяч https://getaddr.bitnodes.io) и отправялем плохие пакеты.
Все соединения из тора в интернет проходят через Tor Exit Node (их чуть больше тысячи https://check.torproject.org/exit-addresses).

Т.е. достаточно отправить 10млн пакетов и на 24 часа биткоинами из тора никто пользоваться не сможет.

(comment on this)

Thursday, May 8th, 2014
11:47 am - transalg
Сегодня утром на архиве появилась статья Transalg: a Tool for Translating Procedural Descriptions of Discrete Functions to SAT. В авторах три товарища из Иркутска.

Предлагается транслятор из небольшого си-подобого язычка в CNF, AIG и систему полиномиальных уравнений.
7k строк на C++, код тут: https://gitorious.org/transalg

Хвастаются, что:
For example, if we consider the DES algorithm that takes 1 block of plaintext (64 bits), the corresponding CNF obtained with TRANSALG has 26400 clauses over the set of 1912 variables. In [9] CNF for the same problem has 61935 clauses over the set of 10336 variables.

Нашёл кандидатскую одного из авторов: Методы и средства преобразования процедурных описаний дискретных функций в булевы уравнения Отпущенников И. В. (собственно он весь код и писал, остальные, видимо, руководили).
Трансляция делается с помощью символьной интерпретации программы.
Из интересного:
В комплексе Transalg преобразования Цейтина осуществляются в отношении подформул от многих переменных
(до 15 переменных). При этом КНФ-представление булевой функции [...] строится в два этапа: сначала строится СКНФ по таблице истинности, а затем данная СКНФ минимизируется при помощи свободно распространяемой утилиты Espresso [...] Вычислительные эксперименты показали, что ис­пользование Espresso позволяет сократить общий объем пропозиционального кода (в КНФ) в среднем на 30 процентов.

Я сейчас занимаюсь примерно тем же самым -- из небольшого специализированного DSL делаю систему полиномиальных уравнений и CNF. Интересно сравнить результаты.

(5 comments | comment on this)

Friday, April 25th, 2014
11:30 pm - PPSZ, Uniquie 3-SAT
Если 3-CNF имеет только одно решение, то найти его можно быстрее.
Асимптотически быстрее. Всё ещё экспоненциально, но основание степени немножко меньше.

Алгоритм в [1] называется ResolveSat, но в других статьях его называют PPSZ (по инициалам авторов [1]).
Состоит из двух этапов.
Сначала в цикле применяем правило резолюции. При этом дизъюнкты склеиваются дуг с другом. Цель первого этапа -- сделать как можно больше дизъюнктов размером в 4-5 литералов (но не больше).

Затем, переменным по очереди, в случайном порядке, присваиваются значения. После каждого присвоения продвигаются константы (и фиксируются значения переменных из диъзюнктов с одним литералом). Если обнаружили конфликт, все присваивания откатываются, выбирается новый случайный порядок и второй этап начинается заново.

В статье доказывается, что если решение только одно, то на втором этапе будет больше переменных, значение которых не угадывается, а является следствием других угаданных (т.е. определяется из однолитеральных дизъюнктов).

С деталями я не разобрался, но результат очень интересный.

[1] An Improved Exponential-Time Algorithm for k-SAT
[2] The PPSZ Algorithm
[3] Exponential Lower Bounds for the PPSZ k-SAT Algorithm
[4] Improving PPSZ for 3-SAT using Critical Variables
[5]* Breaking the PPSZ Barrier for Unique 3-SAT
[6] http://cstheory.stackexchange.com/questions/22093/examples-where-the-uniqueness-of-the-solution-makes-it-easier-to-find

(6 comments | comment on this)

Wednesday, April 16th, 2014
8:59 am
Вчера написал что "самая простая и быстрая операция в DPLL и CDCL -- это распространение констант".
На самом деле [1]:
In practice, for most SAT problems, a major potion (greater than 90% in most cases) of the solvers’ run time is spent in the BCP process.

Чтобы BCP была ещё быстрее, используются watched literals.

[1] Chaff: Engineering an Efficient SAT Solver

(4 comments | comment on this)

Tuesday, April 15th, 2014
7:20 pm - CNF implicativity, Plaisted-Greenbaum
Уличная магия. Как ускорить minisat в 50 раз.

Я недавно жаловался, что решение для в 10 раз более компактной CNF ищется в пять раз дольше.

Перерыл пачку статей и случайно наткнулся на Translating Pseudo-Boolean Constraints into SAT.

Там, среди прочего, вскользь упоминается про CNF implicativity.
Самая простая и быстрая операция в DPLL и CDCL -- это распространение констант (constant propagation).
Implicativity -- это как раз мера того, насколько хорошо в данной формуле эти константы распространяются (т.е. если зафиксировать значение некоторой переменной, сколько ещё переменных получат фиксированные значения). Термин вводится в статье Foundations of Hierarchical SAT-Solving, которую я не читал.

При преобразовании из BDD, каждый узел диаграммы представляется в виде if-then-else. Т.е. в CNF добавляются дизъюнкты вида
    x = ITE c t f
  ≡ x = (c ∧ t) ∨ (-c ∧ f)

Проблема в том, что значение какой-то переменной можно получить, только если зафиксировать все три другие переменные. Можно немножко помочь решателю и добавить (логически избыточный) факт -t ∧ -f => -x. Это поможет в некоторых случаях не зависеть от значения переменной c.

Итого:
- меняем три строчки кода
- количество переменных в CNF не меняется
- количество дизъюнктов увеличивается на 25%
- minisat находит решение за 2.5 секунды вместо пяти минут (на чистом преобразовании Цейтина он работал 45 секунд)


В рамках перерывания статей таки разобрался что такое Plaisted-Greenbaum transformation.
В двух словах, при преобразовании Цейтина, когда вводится новая переменная, иногда можно писать не равенство, а импликацию. Это уменьшает количество дизъюнктов в CNF.
- меняем 5 строчек
- количество дизъюнктов уменьшается обратно на 35%
- minisat находит решение за 0.8 секунд и кушает памяти 90 Мб (против 150 в прошлый раз)
- ...
- profit

Чудесное подтверждение регулярно встречающегося в статьях утверждения, что сложность SAT катастрофически зависит от способа кодирования проблемы.


Надо ещё ускорить truth table -> BDD и совсем круто будет.

(7 comments | comment on this)

Saturday, April 5th, 2014
5:00 pm - Про Tor и анонимность
Почему-то вдруг начал читать про Tor. Оказалось, что в нынешних реалиях гарантия анонимности не велика.

Под катом краткий конспект первой части статьи Seeking Anonymity in an Internet Panopticon
(во второй части предлагается альтернативное решение, которое "offer measurable anonymity guarantees").

Read more...Collapse )

(2 comments | comment on this)

Thursday, April 3rd, 2014
7:31 pm - Ещё раз про CNF из ограничений (практические результаты)
Продолжаю биться над загадкой.
Сделал преобразование ограничений в BDD и преобразование BDD в CNF.
CNF получается на порядок меньше чем при преобразовании Цейтина, но minisat ищет решение в пять раз дольше.

Под катом кратко про преобразование Цейтина и про получение CNF из BDD, а ещё опыты и вопросы.
Read more...Collapse )

(comment on this)

Friday, March 28th, 2014
10:32 pm - btc, Mt.Gox и наглая ложь
Кто хоть немного интересуется криптовалютами, скорее всего знает, что месяц назад официально ёкнулась старейшая (самая первая) и крупнейшая (70% оборота) биржа биткоинов.
История примерно такая:

  • с весны прошлого года у них были проблемы с выводом $

  • в конце 2013 года начались проблемы с выводом btc

  • 2014-02-07 они заморозили вывод btc (к этому времени вывод $ фактически не работал уже совсем)

  • 2014-02-10 выпустили пресс-релиз с оправданиями, типа "извините, мы тут дырку нашли in the bitcoin software называется она transaction malleability, тесно работаем с Bitcoin core development team to mitigate this issue"

  • 2014-02-17 и 2014-02-20 -- ещё пресс-релизы: "почти исправили, скоро всё будет"

  • ну а 2014-02-28 была персс-конференция, на которой заявили, что через этот transaction malleability у них украли 850k биткоинов, и они начинают процедуру банкротства.

Такая вот печальная история.

А пару дней назад на архиве появиласть статья: Bitcoin Transaction Malleability and MtGox.
Её авторы с января 2013 года собирали все транзакции которые появлялись в сети (т.е. в том числе и те, которые потом не попали в blockchain).
Используя эти данные они обнаружили 29 тысяч попыток использовать transaction malleability, всего на сумму 302k btc (сколько из них имело отношение к Mt.Gox -- не известно). Это немножко меньше чем пропавшие 850k. Более того, 85% атак было совершено после того как вывод биткоинов с Mt.Gox был заморожен, и успешных попыток было всего 20%. Итого, через transaction malleability могло быть украдено всего 386 биткоинов (не тысяч, просто триста восемьдесят шесть).

Такие дела.

Кстати, по поводу "мы тут дырку нашли in the bitcoin software" -- эта дырка была известна с 2010 года и в стандартной реализации протокола github.com/bitcoin/bitcoin она с тех пор и прикрыта (это авторы статьи утверждают, я не нашёл там релевантного кода).

(comment on this)

Sunday, March 16th, 2014
12:48 am
Из таблички-ограничения в 24 переменных и 100k строчек получается CNF с 500k переменных и 1.5M конъюнктов.
Натравил на неё coprocessor -- он после пяти минут шуршания вернул исходную CNF без изменений.

(2 comments | comment on this)

Thursday, March 13th, 2014
12:40 am - ослабление ограничений
thesz подсказал интересную идею с ослаблением ограничений в обмен на производительность SAT.
Я по этому поводу обратил внимание на характер формул, которые получаются в результате Tseitin transoform.

Основной шаг там -- преобразование цепочки конъюнкций:
abcd ≡ (x = ab)(y = xc)(z = yd)z
А равенство разворачивается в CNF вот таким образом:
y = xc ≡ (¬y ∨ x)(¬y ∨ c)(y ∨ ¬x ∨ ¬c)
Если из последнего дизъюнкта убрать ¬x и построить таблицу истинности для исходой формулы (f) и модифицированной (g):
  y x c  f g
  0 0 0  1 1
  0 0 1  1 0
  0 1 0  1 1
  0 1 1  0 0
  1 0 0  0 0
  1 0 1  0 0
  1 1 0  0 0
  1 1 1  1 1
можно заметить, что они отличаются только в одной строчке. Т.е. если заменить f на g, вероятность ошибки будет в среднем 1/8. И это как раз будет false positive.
Можно ещё строить баесовскую сеть, чтобы отбрасывать те переменные, у которых больше вероятность что они равны единице, тогда вероятность ошибки ещё меньше.

Правда не факт, что испорченная формула будет действительно проще для SAT солвера.
Она может быть проще из-за того, что преобразование увеличивает в CNF долю конъюнктов состоящих из двух литералов, а 2-SAT решается за полиномиальное время.
Нужно поэкспериментировать.

(1 comment | comment on this)

Wednesday, March 12th, 2014
11:44 pm - преобразование ограничений в CNF
Первые шаги в решении вчерашней загадки оборачиваются неожиданными сложностями.

Чтобы запихнуть набор ограничений в SAT их нужно сначала преобразовать в CNF.
Написал кусочек кода (https://github.com/jorpic/xxx) который делает это с помощью Tseitin Transformation (кстати он в СПбГУ преподаёт).

Преобразование это заключается в добавлении новых переменных для подвыражений формулы. В результате получается не эквивалентная, но equisatisfiable формула в CNF.

При этом добавляется линейное (от числа битов таблицах с ограничениями) количество переменных. Т.е. формула изрядно раздувается. В статье Successful SAT Encoding Techniques [1] предлагается несколько более свежих методов преобразования, позволяющих получать чуть более компактные формулы.

Первый из них -- by Plaisted & Greenbaum [5]. Попробую сделать его.
Два ещё более свежих метода в [3,4].

При этом в [1,2] предостерегают, что "Plaisted and Greenbaum's algorithm produces a smaller encoding but it is not certain whether it is more efficient for SAT solving, since it may have worse propagation behavior."

Бонусы от более сложных методов могут нивелироваться постобработкой в SatElite или Coprocessor [6].
Нужно экспериментировать. Если будут результаты -- напишу.


[1] Successful SAT Encoding Techniques
[2] Niklas Eén. Practical SAT - a tutorial on applied satisfiability solving
[3] Paul Jackson and Daniel Sheridan. Clause form conversions for boolean circuits
[4] Panagiotis Manolios and Daron Vroon. Efficient circuit to CNF conversion
[5] http://www-ise4.ist.osaka-u.ac.jp/~t-tutiya/sources/bool2cnf/README.pdf
[6] http://tools.computational-logic.org/content/coprocessor.php

(2 comments | comment on this)

Sunday, March 9th, 2014
1:33 pm - загадка
Например, есть n булевых переменных x1, ..., xn.
И на значения этих переменных накладываются ограничения, которые имеют некоторый специальный вид.

Ограничение -- это множество всех допустимых значений некоторого подмножества переменных. Записать его можно в виде таблички или в виде предиката:
    x₁ x₂
    0  1
    1  0          или (x₁=0 ∧ x₂=1) ∨ (x₁=1 ∧ x₂=0) ∨ (x₁=1 ∧ x₂=1)
    1  1

Пусть есть несколько таких ограничений. Если зафиксировать значения нескольких переменных, то такое присваивание либо будет противоречить набору ограничений, либо не будет.

Например, n=4 и заданы такие ограничения:
         x₁ x₂        x₂ x₄        x₁ x₄
         0  1         1  1         1  1
    C₁ = 1  0    C₂ = 0  0    C₃ = 1  0
         1  1         0  1

Если зафиксировать x₁=0, тогда
- из C₁ получаем x₂=0
- далее из C₂ и x₂=0 получаем x₄=1
- а из C₃ и x₄=1 -- противоречие x₁=1.
Т.е. x₁=0 не согласуется с заданным набором ограничений.

Если x₁=1, тогда
- (x₁=1 ∧ C₁) => x₂∊{0,1}
- (x₂∊{0,1} ∧ C₂) => x₄∊{0,1}
- (x₄∊{0,1} ∧ C₃) => x₁∊{0,1}
Т.е. противоречия не получается.

Внимание вопрос!
Как имея фиксированный набор ограничений быстро отвечать на серию запросов типа: "А не противоречит ли этим ограничениям такое-то присваивание значений переменных"?

Допускаются false positives: можно иногда ответить "не противоречит", даже если на самом деле это не так.


У меня в мыслях пока только один подход -- закодировать ограничения в булеву формулу, добавить присвоенные значения переменных, скормить в SAT solver и надеяться на его магию.
Как-то так:
  C₁ = (¬x₁ ∧ x₂) ∨ (x₁ ∧ ¬x₂) ∨ (x₁ ∧ x₂)
  C₂ = ...
  C₃ = ...
  SAT(C₁ ∧ C₂ ∧ C₃ ∧ x₁)

Ну а дальше простор для творчества:
- предварительное преобразование ограничений;
- CNF будет иметь специальный вид, можно упростить с помощью SatElite или ещё как-то;
- Incremental SAT;
- ...

(10 comments | comment on this)

Friday, March 7th, 2014
4:35 pm - Who is I?
Наткнулся на публикации японского товарища по фамилии I: Tomohiro I.
Не Роберт В Флоид конечно же, но тоже забавно.

(comment on this)


> previous 20 entries
> top of page
LiveJournal.com