Собственно сабж.

исходники на гитхабе: https://github.com/gromas/polysat
видео на ютубе:

Не доделан до all-3-sat. Просто 3-sat он решает.

Спасибо. От волнения это.

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

Объясню. Вот ты взял одно состояние и построил по нему часть решения. Неразрешенные биты соответствуют той части пространства решений, которое мы выберем при разветвлении. При этом в каждой итерации по новому состоянию заполнится как минимум один бит маски. То есть общее число итераций не может превышать n*n^3. При этом если учесть, что для построения следующего бита нам нужны только те состояния, в которых один бит соответствует текущему набору переменных и один не соответствует, то ходить мы будем не n*n^3, а n*n^2 максимум. Ну и для выгрузки всех возможных решений нам надо просто хранить маску до последнего ветвления и после получения одного решения, продолжать с того места, где было предыдущее ветвление

1. Сначала создается массив комбинаций троек по N
2. Затем накатывается КНФ, состояния, которые описаны в КНФ удаляются (обнуляются биты)
3. Затем идет цикл по каждому биту, представляющему собой некоторое состояние трёх переменных и для него делается расчет решения, то есть проверяется, что ни одно другое состояние из одного или двух битов не противоречит ему. Если получаем противоречие - сбрасываем конфликтный бит и смотрим следующие. Цикл заканчивается, если больше нет состояний в одном сочетании (байт равен 0) или если в предыдущей итерации не было удалено ни одного состояния.

выше написал. там нет рекурсии

1. расчет совместимости состояния: за одну итерацию по маске у нас получается или меняется как минимум один бит в маске, или мы получаем противоречие. максимум итераций n - маска размером n. если противоречий и изменений в маске нет, выходим.
2. расчет происходит по всем состояниям: за одну итерацию мы или удаляем хотя бы одно состояние или выходим с сообщением SAT.
Тут нет никаких рекурсий. п.1 выполняется максимум за n^4, п.2 - максимум n^6. один вложен в другой, суммарное время n^10. Но учитывая мою статистику по нескольким десяткам тысяч различных CNF цикл из п.2 завершается уже на 4-5 итерации, n^3 там не знаю на какой случай, надо видимо специально такой придумывать.

попадает. прорешано уже несколько десятков тысяч различных cnf из интернетов, решены все. на миллион не рассчитываю - пусть в зад себе запихают, бюрократы сраные

Aleksandr Sharahov,

Да, я понял. Строгое доказательство будет. Начал писать функцию, возвращающую все возможные результаты решения и похоже всё оно так и есть как я говорил, последовательно переключая состояния дерева мы за n^3 итераций точно приходим к следующему решению. То есть массив, оставшийся после алгоритма голосования содержит не просто все неконфликтующие друг с другом состояния, он содержит суперпозицию всех возможных решений и ни одного который не подходит под наш КНФ.

А мы и не пытаемся угадывать значение переменной. Если для какой-то переменной не существует однозначного назначения, мы оставляем её в суперпозиции состояний. Из этого как раз и следует тот факт, что если на очередной итерации маска не изменилась, мы просто заканчиваем работу и говорим, что состояние согласовано.