3SAT решается за полиномиальное время?
Я видел несколько ошибок в файлах cnf как для удовлетворительных, так и для неудовлетворительных файлов предложений. Задачи SATLIB Benchmark
Чтобы быть более конкретным, я обнаружил, что 1-й файл в папке zip здесь: 20 переменных, 91 предложение - 1000 экземпляров, все выполнимые содержит файл с названием "uf20-01", уравнение которого неудовлетворительно ясно как 7-е предложение в 15-й строке и 87-е предложение в строке № 4 являются точными обратными друг другу!((5 19 17) и (-5 -19 -17))
Таким образом, операция И, имеющая их в любой момент времени, приведет к тому, что уравнение будет неудовлетворительным.
Я пришел к выводу, что если два предложения являются точными обратными друг к другу, то и только тогда уравнение является неудовлетворительным, в противном случае уравнение является выполнимым. Я попытался еще один файл UNSAT по вышеуказанной ссылке методом проб и ошибок, и хотя MINISAT Версия браузера также говорит, что тот же файл является неудовлетворительным. Я нашел решение для того же самого в 1 и 0 для каждой переменной.
Алгоритм выше был опубликован мной в журнале, но был отклонен.
Мой вопрос: может ли кто-нибудь привести мне пример неудовлетворительного уравнения 3SAT, которое содержит только 3 переменные (или, может быть, немного больше...), не имея при этом ни одного предложения, являющегося точным обратным к другому?
Если я смогу получить такое предложение, тогда алгоритм ошибочен (но все же он доказывает, что многие проблемы с тестами SAT являются UNSAT), и это не доказывает, что многие проблемы UNSAT в 1-м канале действительно являются SAT.
Это дразнит мой разум и надеюсь, что вы все это понимаете, как будто приведенный выше алгоритм верен, тогда я доказал P=NP! Это может начать революцию также..
Кстати, я также отправил электронное письмо контактному лицу SATLIB, но по-прежнему не получил ответа через 2 дня относительно файла 2-й ссылки.
2 ответа
В 3-Sat в CNF все предложения являются OR-предложениями, и они объединяются с помощью AND. Таким образом, две строки, которые вы цитируете, определяют следующие два пункта
x5 or x17 or x19
(not x5) or (not x17) or (not x19)
и то, и другое можно удовлетворить, например, установив x5 в true, x17 в false и x19 в произвольный.
Их много:(x1 или x2 или x3) и (не x1 или x2), а не x2 и не x3
В общем, чтобы показать это, вам нужно будет ввести больше переменных. Но интуитивно даже не кажется правдой, что инверсия всех переменных любого предложения не требуется для выполнения UNSAT. Как указывает другой ответ, даже в самом простом случае это все еще SAT, когда это происходит. Возможно, эталонный тестовый набор имеет тенденцию иметь это, но это не обобщает.