В самом начале это когда? До применения КНФ существуют все возможные решения, они согласованы и равны 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

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