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

исходники на гитхабе: 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 итераций точно приходим к следующему решению. То есть массив, оставшийся после алгоритма голосования содержит не просто все неконфликтующие друг с другом состояния, он содержит суперпозицию всех возможных решений и ни одного который не подходит под наш КНФ.

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

В самом начале это когда? До применения КНФ существуют все возможные решения, они согласованы и равны 1. И да, и их 2^n )). После применения КНФ часть состояний становится несовместима друг с другом. Для согласования применяется алгоритм консенсуса с удалением участников (конфликтующих состояний). После работы алгоритма все состояния опять согласованы и их набор содержит суперпозицию всех возможных решений.



Александр, вы видео смотрели? Там подробно рассмотрены все варианты действий. И в презентации pptx на гитхабе.

Я решал примеры, которые есть в папке /samples
Там и положительные и отрицательные и с разным числом переменных. Больше тысячи штук.

Выяснил один неприятный момент. Если мы хотим получить решение для какой-то ветки, то просто пройтись по ней и выбрать не получится. Хотя на некоторых примерах работает. После каждого выбора необходимо схлопнуть суперпозицию, удалив НЕВЫБРАННЫЕ состояния и запустив алгоритм консенсуса еще раз. Естественно, если хочется потом получить еще одно решения, потребуется скопировать оригинальный массив.

Нет там рекурсии. От слова совсем. Набор неизвестных битов конечен и не превышает число переменных. То есть максимум оценка может оказаться выше в n раз. Но уже нашли другую проблему, более серьёзную. Замыкание цепочек назначений через отрицание группы состояний. В результате получаем SAT вместо UNSAT. Вот тут да, придется в результате вычисления эти циклы искать отдельным алгоритмом. Надеюсь что решится и очень странно что среди найденных в интернете нескольких десятков тысяч тестов ни одного с таким циклом не попалось.

Перебором я выбираю решения, а не создаю их и не решаю. Стоимость - разница между 3-SAT и ALL-3-SAT.
Вы не сможете выбрать все 2^n степени решений за время меньшее количества этих решений. Построить можете, выбрать нет. Думаю разница вполне должна быть понятна. Алгоритм строит все решения. Результат работы - информация об их наличии или отсутствии. Выбор всех решений вопрос отдельный, к задаче выполнимости не имеющий ни какого отношения.

Не ВОЗМОЖНО. А есть. При чем только они. С циклами, которые алгоритм не обнаруживает в силу локальности я проблему решу. Перебиралку решений вчера вечером делал и она выбирала решения однозначно и ничего лишнего, ни каких бэктрекингов и прочих проблем решателей класса 2^n

Хотя наверное соглашусь, пока нет формального доказательства это всего лишь гипотезы.

Именно это я пытаюсь сделать. Вчера пытался. Пока мне не подкинули пример с циклом, для которого алгоритм как раз пустые пропускает. Из других проверенных тестовых примеров неправильных решений не получалось выбрать, как я не старался. Понять и осознать сложно почему так, хотя я как раз представлял именно такой вариант решения, когда дошел до алгоритма. Но вот доказать что так всегда... Один пример уже есть, что это может быть не так, но там проблема понятна почему.

Удачные назначения как раз и остаются после работы алгоритма. И только удачные, и других нет. Не учитывая логической проблемы с циклами с отрицанием друг друга (два невыполнимых состояния рекурсивно отрицают друг друга, получается логическая проблема, которую мой алгоритм не умеет находить).

Да, по решениям думаю пока составлять матрицу инцидентности и её исследовать. Может еще какие проблемы найдутся.

20 переменных решение находит в среднем 6 секунд на моем ноуте
50 переменных отсутствие решения находит в среднем за 20 секунд
50 переменных существование решения находит примерно за 12 минут. Мой старенький ноут неспособен перебрать 10^15 вариантов, что бы найти решение наверное даже за месяц ))) это если кто-то будет утверждать, что тут есть экспоненциальная сложность. Хотя n^10 это уже слишком много.

Ну и собственно само наблюдение не нужно. Есть же исходники на гитхабе, там текста на две страницы всего. Проверить, что бесконечных циклов нет проблемы не должно быть.

https://github.com/gromas/polysat

Отрицательный ответ алгоритм наоборот даёт очень быстро, так как с каждым шагом пространство возможных решений резко уменьшается в размере. Долго считается как раз вариант если решения есть.

Мы видимо так и будем тут говорить о разном ) Нет там экспоненты вообще. Откройте уже исходный код и убедитесь. Две страницы текста всего.