SatWalker и второй раунд Intel Threading Challenge 2009

Так как мое решение стало самым быстрым во втором раунде ("These were three entries that could handle the expression with 100 variables. The fastest of these was submitted by jne100."), решил запостить его тут, чтобы можно было сравнить со своим, ну или просто посмотреть.

Немного теории. Для решения проблемы 3-разрешимости я использовал алгоритм WalkSat. Нашел его не сразу, сначала пытался решать проблему перебором, а еще как то интеллектуально подобрать значения булевых переменных, но очень скоро понял что все это бесполезно. Алгоритм WalkSat заключается в следующем: сначала значения всех переменных устанавливаются произольным образом (вообще то я устанавливал их наилучшим образом). Затем находятся все неудовлетворяющие скобки (т.е. тройки переменных объединенных операцией логиского "ИЛИ"). На каждой итерации случайным образом выбирается одна из неудовлетворяющих скобок, а далее в зависимости от значения вероятности (0.5 by default) может произойти одно из двух действий - либо алгоритм пытается улучшить ситуацию инвертированием наиболее подходящей переменной (инвертирование которой уменьшит количество неудовлетворяющих скобок), либо инвертирует произвольную из трех переменных, что обеспечивает ему выход из локальных максимумов. Все заканчивается если решение найдено, или совершено максимальное количество итераций (это скорее всего означает что решения вообще нет).

В параллельной версии я просто запускал несколько потоков (8 конечно) поиска решения с разным значением вероятности (0.5, 0.55, 0.60...) выбора между двумя действиями. На практике все это работает чертовски хорошо, и решение находится очень быстро.

Кстати еще двое участников из Китая, чьи решения могли обрабатывать болшое количество переменных, использовали примерно такие же способы (еще один WalkSat и один GSat). Жаль конечно что райтап я слил - совсем не было времени его писать. Теперь скачав идеальный райтап одного из китайских участников, все буду делать по его образцу.

А вот и сама ссылка на мое решение - /sites/default/files/m/d/4/1/d/8/jne100_3sat.zip.
For more complete information about compiler optimizations, see our Optimization Notice.
Categories: