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)

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)

Sunday, April 6th, 2014
10:45 pm
Вангую, что биткоины скоро накроются звездой (не совсем, но протокол придётся обновить).
Неделю назад случайно обнаружил, что в последнее время почти 1% блоков не содержит транзакций кроме coinbase.
А тут вот ещё такие аномалии: 18 blocks per day with power 2 number of transactions.

Очень похоже, что фиксированный merkle root даёт преимущество при майнинге, а это прямая дорога к тому, что реальные транзакции перестанут включаться в блоки.

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

Friday, April 4th, 2014
7:34 pm
via sober_space узнал, что Брендана Айка вынудили уйти с поста CEO Мозилы за то, что он поддержал поправку в конституцию Калифорнии о непризнании однополых браков*.

Никак не могу решить как к относиться к тому факту, что человека фактически "уволили" за то, что он публично выразил своё мнение по какому-то поводу.

Что, если бы он поддержал поправку о непризнании браков с детьми 8-и лет?
Что, если бы он поддержал поправку о непризнании межконфессиональных браков?

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

* Три раза сверился с википедией что же именно он там поддержал, надеюсь не ошибся.

(15 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)

Monday, December 9th, 2013
12:48 pm
Полиномиальное уравнение f : F2n -> F2 можно представить в виде f(x) = fL(xL) + fNL(xNL), где fL -- линейная функция от некоторого подмножества переменных xL \in x, а fNL -- нелинейная функция.
При этом xL и xNL не имеют общих элементов.
Т.е. xL -- переменные, которые используются в f только линейным образом, а xNL -- все остальные.

Для любого набора значений переменных из xNL у f(x) = 0 будет 2|XL|-1 решений.

Это тривиальное наблюдение можно использовать чтобы быстрее перебирать решения f(x) = 0 или чтобы компактнее их хранить.

(comment on this)

Friday, November 29th, 2013
9:56 am - Про полиномы
А вот, например, у меня есть полиномиальное уравнение над GF(2):
x0x1 + x1 + x0x3x4 + x1x4 + x25 = 0
Read more...Collapse )

(1 comment | comment on this)

Monday, March 5th, 2012
7:01 pm - Москва, УИК 2021
По данным избиркома (2021, у меня в протоколе такие же цифры):
- явка: 60.87%
- путин: 45.95% (624 чел)
На соседних участках (в той же школе):
- 2022 64.30 / 43.65% (643)
-
2023 66.31 / 41.41% (723)

На нашем участке было шесть наблюдателей, но это не помешало комиссии устроить трэш и угар при подсчёте голосов.
Итого: 26 часов на участке, протокол в ТИК сдавали самыми последними по округу, уже после 9-00.

Из развлечений: проставление галочек во время подсчёта голосов, отстранение трёх членов ИК, отказ подписывать протокол, визит председателя ТИК и наряда милиции.
Это не считая всяких мелочей типа обзвона пенсионеров для формирования списков голосования на дому и консультации с анонимами в ТИКе по поводу цифр в протоколе.
Позже, административщину и уголовщину решили замять в обмен на лояльность комиссии.

Из любопытного: в дополнительный список избирателей было внесено около 50 человек (не считая тех, что по открепительным). Т.е. это товарищи, которых нет в основном списке: они показывают прописку в паспорте и секретарь их вписывает в дополнительный список. Что у них на самом деле в прописке, никто кроме секретаря не знает. Председатель объясняет это проблемами с актуальностью данных в паспортном столе по нескольком домам*.

Вывод: обязательно пойду наблюдателем (а почему бы и не членом?!) на любые следующие выборы. Этим людям нельзя доверить даже подсчёт голосов за цвет обоев в туалете.

Справедливости ради, отмечу, что самые безобразия устраивали всего трое-четверо членов из десяти.

*Кто нибудь знает, что с этим делать? куда жаловаться? или где узнать?

(comment on this)

Tuesday, February 7th, 2012
2:56 pm
Нашёл в бэкапах файлик слова.txtCollapse )

У кого-нибудь есть что добавить?

(6 comments | comment on this)

Friday, December 3rd, 2010
6:45 pm - blaze-builder
Самое большое зло в интернете -- это ссылки.
Понятное дело, наткнулся ты на какую-то офигенную штуку -- нужно обязательно со всеми поделиться: вдруг дружбаны-то и не в курсе совсем.
Но, бля, раз уж такая офигенная ссылка, неужели сложно написать маленький абзац о том, что за ссылкой скрывается и почему она заслуживает нажатия, траффика, внимания, времени?!

http://lambda-view.blogspot.com/2010/11/blaze-builder-library-faster.html

(8 comments | comment on this)

Monday, November 29th, 2010
8:12 pm - картинки
Наверное все видели видео "fractals without a computer" (http://www.youtube.com/watch?v=Jj9pbs-jjis)
Очень красиво.
Я вот тоже решил такое сделать, только с компьютером вместо трёх проектеров.
Под катом скрипт для gstreamer'а и пaрa картинок.Read more...Collapse )

(comment on this)

Tuesday, November 23rd, 2010
5:12 pm - загадка: Jean-Michel Muller sequence
Нужно посчитать, чему равен предел вот такой последовательности:
f 0 = 11/2
f 1 = 61/11
f n = 111 - (1130 - 3000 / f (n-1)) / f (n-2)

Обещают, что fn = (6n+1 + 5n+1) / (6n + 5n),
но как это показать, не признаются. Я пробовал подставлять kxn, но быстро сдался.
Собственно, вопрос №2: такие вот нелинейные реккурентные соотношения каким-нибудь простым способом решаются?

(13 comments | comment on this)


> previous 20 entries
> top of page
LiveJournal.com