http://fmv.jku.at/papers/HeuleJarvisaloBiere-LPAR10.pdfRead more... )

https://ojs.aaai.org/index.php/AAAI/article/download/10114/9973Read more... )

Алгоритмы случайного поиска решения лучше справляются со случайными задачами логической выполнимости, а алгоритмы с перебором и распространением (DPLL) со структурированными задачами.

(я делал алгоритм доказательства работы на основе случайной SAT - с 5SAT вблизи фазового перехода ни один из современных структурных решателей справиться не мог, а ( Read more... )

Самый первый алгоритм проверки разрешимости логической формулы использовал "разрешение" ограничений (resolution): для ограничений вида (a∨b∨c) и (-a∨b∨d) мы можем вывести ограничение (b∨c∨d), устранив переменную a. Так вот, алгоритм Davis-Putnam выбирал переменную для устранения и устранял все ограничения, выводя новые и проверяя их на тавтологию ( ( Read more... )

Вот пример решателя SAT, основанного на случайном поиске вокруг текущего присваивания: http://fmv.jku.at/yalsat/

Основной алгоритм у него таков:

1. если нет неудовлетворённых ограничений, остановиться
2. если есть неудовлетворённые ограничения, взять первое (или второе - или какое-то, там шесть ( Read more... )

Я был неправ в указании источника NP-полноты проблемы получения наименьшего конфликта.

Моё текущее понимание таково: если мы удаляем литерал l из некоторого набора путей {P}l{S}, то нам надо добавить пути {P}⨯{S} - все пути до литерала l должны вести во все пути после. Собственно, это всё то же правило разрешения, только вылезшее в другом месте.

Начало про общую идею, необходимые структуры данных и тп ( Read more... )

Я тут в твиттере распространялся про поиск наикратчайшего ограничения при поиске решения в алгоритме выведения ограничений из конфликтов (решение задачи логической разрешимости).

Важно найти наикратчайшее ограничение. "Сила" ограничения пропорциональна 2-длина ограниченияПри поиске ограничений мы 1) имеем дело с множеством "нарезаний" фронтов ( Read more... )

Обобщённое усиление выведенных из конфликтов ограничений - показывает, что отыскание ограничения конфликта минимального размера является, само по себе, NP-трудной задачей (то есть, даже проверка является NP-полной задачей ( Read more... )

Я тут собрал на коленке решатель задач булевской выполнимости (SAT, boolean satisfiability). Отличие от обычных решателей в том, что он позволяет запускать параллельно множество тесно взаимодействующих тупых решателей (совсем тупых), ну, и обработка конфликтов в нём отличается от обычных SAT решателей (нет отката, например ( Read more... )