Библиотека

У меня собралось несколько книжек, которые не в каждом московском магазине можно купить.
Сам я их не каждый день читаю, а книжкам обидно лежать мёртвым грузом на полке.
Поэтому могу дать кому-нибудь на почитать.
Collapse )

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

CNF shuffling

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

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

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.

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

про ghc немножко

На днях в haskell-russian случился небольшой срачик в результате которого моё представление об устройстве мира было безнадёжно подорвано и теперь я в недоумении. Поэтому хочу зафиксировать.
Collapse )

внезапно

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).

(no subject)

Продолжение http://zelych.livejournal.com/21224.html.

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

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

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

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

(no subject)

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

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


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

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

Как забанить тор в биткоин-сети

По мотивам 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 часа биткоинами из тора никто пользоваться не сможет.

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. Интересно сравнить результаты.

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