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

Дорешивать придется. Есть пример, на котором алгоритм всегда выдает ложноположительный ответ. Особый случай КНФ, в котором алгоритм не может разрешить две или более невыполнимых циклических зависимости, взаимоотрицающих друг друга. В разделе samples лежит файл Mikhail_unsat.cnf , содержащий восемь таких циклов. Как найти и разрешить такие зависимости я вполне представляю и сейчас занимаюсь алгоритмом этой проблемы. Других вариантов ложноположительных ответов не существует. Уже написана большая часть формального доказательства работы алгоритма, в котором подробно рассматривается это исключение. Так же есть доказательство того, что невозможно получить ложноотрицательное решение.

Вы серьезно? Может мне сюда проект весь выложить в отдельную тему специально для тех, кто не увидел тут ссылки на проект github? Думаю модераторы будут очень рады такому.

Согласен. После моего алгоритма в случае положительного ответа придется запускать алгоритм или получения всех ответов - он экспоненциальный, так как решение может содержать все 2 ⁿ возможных решений, но может быть выгоден, если количество оставшихся "в живых" состояний крайне мало и соответственно решений тоже очень мало, или алгоритм с построением направленного графа таких зависимостей, он неприятный, требует дополнительно N ⁶ памяти и работает соответственно не меньше чем за N ⁶ времени, хотя на фоне общего времени получения решения N ¹⁰ его стоимость мала.

Aleksandr Sharahov,

Есть пока только гипотеза, что исследовать нужно не только пространство возможных решений, но и пространство нулей - тех состояний которые были выкинуты на этапе работы алгоритма консенсуса. Если среди них есть циклические зависимости, то вероятно они являются отражением наших циклов на область нулей. Плюс такого подхода в том, что при ложноположительном результате в области нулей практически отсутствуют состояния, что значительно сокращает пространство поиска такой зависимости. Например со случаем файла mikhail_unsat в пространство нулей кроме самой КНФ вобще ничего не попадает.

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

Интересно, да, если имеет место расщепление по какой-то переменной, то сумма всех нулевых векторов в обоих половинах не может превышать сумму таких векторов в общем решении. Но я не уверен, что это нам что-то даёт.

Можно нулевые вектора попробовать проверить на наличие цепочек приводящих к какому-то локальному решению. Консенсус среди нулей. Пусть сами выберут кто лишний.

Решение готово. Надо просто ХРАНИТЬ все построенные векторы и сравнивать не с тремя переменными комбинации, а с вектором целиком. Новое решение решает проблему, жрёт в 2n раз больше памяти и соответственно времени. Исходники можно найти тут: https://github.com/gromas/polysat/tree/extended_vector

• хранятся векторы значений размера 2n для каждого сочетания трёх переменных из n. По два бита на значение. Принимают значения 0/1 + бит на хранение статуса Set/Unset
  
• сравниваются между собой вектор одного сочетания со всеми векторами остальных сочетаний. При совпадении вектор проверяемого сочетания дополняется (выставляются совпадающие биты), при отстутствии совпадений вектор удаляется (последний бит в наборе байтов вектора хранит признак удаления)
  
• при полном удалении всех 8 векторов сочетания получаем UNSAT
  
• при отсутствии изменений в очередном цикле сравнения получаем SAT. Цикл do ... while(changed). Максимальное количество циклов в худшем случае составляет 2n^4, если в каждом цикле обновляется один единственный бит, обычно занимает от трёх до пяти циклов.
  

Вопрос интересный. Сейчас сижу описываю принцип работы. Смысл следующий.

• Изначально решение представляет набор векторов назначения переменных (состояний) всех возможных сочетаний по 3 переменных из n. Каждое такое сочетание может содержать не более 2^3 = 8 векторов для каждого варианта назначения трёх переменных 0/1.
  
• Что бы построить полный вектор конкретного решения, требуется что бы каждое сочетание содержало в себе как минимум один вектор побитно совпадающий с решением.
  
• Соответственно, если в одном из сочетаний отсутствуют векторы, ни одного решения не существует.
  
• Удаляем из нашего набора все векторы, назначения которых соответствуют клозам КНФ.
  
• Для каждого вектора в каждом сочетании пытаемся построить полную цепочку решения, соответственно поочередно перебираем все сочетания и из каждого выбираем совместимые с проверяемым вектором векторы и в случае разрешения какого-либо нового бита обновляем исходный вектор. Если совместимых векторов не обнаружено, значит для исследуемого вектора невозможно построить полную цепочку из векторов всех остальных сочетаний, соответственно он в решении лишнее звено - удаляем его.
  
• Расчёт заканчивается когда либо в одном из сочетаний удалены все векторы либо больше не существует противоречий между векторами. Отсутствие противоречий объясняет возможность построения полного решения. Сам полученный набор векторов является суперпозицией всех возможных решений, соответственно если он существует - решения есть, не существует - решений нет.
  

На пальцах сложно объяснить. Общий смысл такой: допустим у нас в списке существует некоторый вектор, для которого решение (полный вектор размером n) построить нельзя. Предыдущий алгоритм пропускал такие векторы по той причине, что он каждый раз начинал строиться не учитывая предыдущей истории, а проверяя соответствие только текущему назначению трёх переменных. Теперь если вектору соответствует какая-то цепочка, не приводящая к решению, то в ней как минимум две маски сочетаний будут противоречить друг другу. Это означает две вещи - что данная пара конфликтующих векторов единственная и другого варианта выбора (расщепления пространства решений с другими значениями маски) для этого конфликта у нас нет, иначе бы мы не получили конфликт, так как каждый вектор соответствует хотя бы одному другому в каждом сочетании, ну и из этого следует, что два проверяемых вектора конфликтуют с единственным возможным вектором, что невозможно в силу того, что алгоритм как раз такие конфликтующие пары удаляет. На а про то, что цепочки из возможных решений не могут быть удалены объяснение совсем простое. Если существует решение (полный вектор размером n), то для него в каждой комбинации должен существовать вектор как минимум размером 3. При этом для каждого такого вектора в одной комбинации переменных должен существовать как минимум один не противоречащий ему вектор в следующей комбинации и их полные вектора будут полностью соответствовать друг другу и всем последующим, подходящим к решению, так как они не могут конфликтовать друг с другом в силу того, что являются частью одного решения.

могла существовать в прошлом варианте. тут нет как таковой длинной цепочки, так как вектор после пересчета по сути сам является концом длинной цепочки "слева" и по сути в бесконечном плане происходит замыкание начала и конца цепочки (раньше так сделать было невозможно, так как истории слева не было) - цепочки, где любой выбор не противоречит любому другому дальше.