Усовершенствованный брутфорс 3-sat выражения. За 6 минут на старом дряхлом ноуте в один поток выдаёт все варианты решения задачи из 50 переменных.

Да, забыл. Обычный брутфорс на том же ноуте считает это же больше двух суток, может дольше, ждать не стал.

Посчитал сложность. Если для брутфорса сложность равна O(2^n), то для моего алгоритма она равна O((7/8)^m*2^n), где n - число переменных, m - число клозов в выражении.

А он есть.

Это нижняя граница. Верхняя O((7/8)^n*2^n). Для анализа формулы с 20 переменными брутфорсу требуется 1047576 итераций, моему алгоритму максимум 72570. Если конечное число решений не больше этой цифры.

Сам алгоритм.

1. Пронумеруем все n битов задачи.
2. Отсортируем переменные в каждом клозе выражения в порядке возрастания.
3. Отсортируем все клозы выражения в порядке возрастания переменных, которые в них входят.
4. Инициализируем переменные нулями.
5. В порядке сортировки клозов проверяем их на выполнимость, пока не найдём невыполнимую клозу.
6. В невыполнимой клозе увеличим значение последнего бита, что бы клоза стала выполнимой. Если последний бит был единицей, применим правило переноса на следующий бит задачи.
7. Повторяем пункты 5 - 7 до тех пор, пока выражение не будет выполнимо. Если при выполнении переноса мы получаем все биты равные 0, выражение не имеет решений.

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

Еще ускорение нашел. К каждой переменной добавить id клозов которые изменяются при изменении этой переменной и строить обход клозов не в лоб по очереди, а в порядке их изменения. В результате получается граф зависимостей переменных и частей формулы. И мне кажется, что так можно даже алгоритм PPSZ обогнать или приблизиться к нему. Возможно, если дальше проанализировать этот граф обхода, можно найти зависимости выполнимых выражений от невыполнимых.