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

Тут еще один момент замечу на всякий. У нас, что бы цепочка после замыкания привела к ложноположительному результату необходимо сделать так, что бы в пути в разных векторах этой цепочки была назначена одна и та же переменная разными способами (0 или 1). Это единственный вариант, который делает решение невозможным. При этом тогда в одном из векторов должно быть четкое назначение 1 или 0. То есть ему соответствует один единственный вариант решения вместе со следующим вектором. Из этого следует, что этот 0 будет реплицирован по всей цепочке векторов до того вектора, где переменной назначается значение 1. И тут как раз алгоритм отсекает вектор с единицей, так как он не совпадает с предыдущим... Не отсечь он может только если ранее существует ветвление, сбрасывающее значение этой переменной, то есть деление по значению самой этой переменной. Но тогда наш вариант цепочки с установленным 0 не попадет в эту ветку с установленной 1 вообще, то есть конфликта не будет.

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

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

Что бы не говорить на пустом месте, я тут картинку быстро набросал. Кривая ну и пофиг.

Вот если в abc мы назначили b = 1. Алгоритм жадный и пытается распространить назначенное нами значение на как можно большее число векторов. Он утащит его сначала в abd, затем в acd, затем в bcd и при отсутствии ветвлений в конце концов это назначение вернется обратно в abc. Теперь, допустим у нас есть ветвление, в котором переменной b мы назначаем 0. Соответственно это назначение также будет распространено вплоть до разветвления. При этом алгоритм обнаружит, что в нашей ветке оно не соответствует назначению b = 1 и назначение b = 0 будет удалено. При этом в другую сторону наш алгоритм или оставит разветвление без назначения, пока до него не распространится b=0, либо если оно уже тут - выберет другую ветку и будет распространять нашу 1 на неё.

Собственно тестовый файл Mikhail как раз такой случай - там не восьмерка даже, там 8 колец в одной точке соединяются. Старый алгоритм не умел это решать, новый сразу говорит UNSAT.
При чем рядом лежит второй файл, в котором как раз два кольца оставлено - у него решение есть.

https://github.com/gromas/polysat/tree/extended_vector/samples/Circular logical deadlock

Хотя выше как раз про восьмерку объяснение ) Консенсус он такой, внутри общей части тоже есть назначение, и оно тоже распространяется в разные стороны. И когда к разветвлению придут две ветки с назначением b = 1 и одна с назначением b = 0, то b=0 умрёт.

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

За ночь сделал описание работы алгоритма и ответы на частые вопросы

https://github.com/gromas/polysat/blob/main/docs/Polysat.docx

Интересно. Почитаю. 10 лет и тишина - странно.

Оказывается вот так. (((

Автор признал, что его вариант не решает проблему 3-SAT, придумал новый алгоритм, но не успел его даже опробовать и умер.

тогда вот это очень старая статья

Вот последняя статья. Но под неё так и не смогли сделать решатель, как я понял. Ибо автор умер и выяснить непонятности не удалось.

https://arxiv.org/pdf/1309.6078.pdf

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

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