Я видел несколько ошибок в файлах cnf как для удовлетворительных, так и для невыполнимых файлов предложений SATLIB Проблемы с тестированием
Чтобы быть более конкретным, я обнаружил, что 1-й файл zip-папки здесь: 20 переменных, 91 пункт - 1000 экземпляров, все выполнимы, содержит файл с заголовком uf20-01, уравнение которого явно неудовлетворительно, поскольку 7-е предложение в 15-я строка и 87-е предложение в строке номер 4 в точности противоположны друг другу! ((5 19 17) и (-5-19-17))
Таким образом, операция И, имеющая их в любой момент времени, приведет к тому, что уравнение будет невыполнимым.
Я пришел к выводу, что если два предложения являются точными обратными друг другу, тогда и только тогда уравнение невыполнимо, иначе уравнение выполнимо .. Я попытался выполнить другой файл UNSAT по указанной выше ссылке методом проб и ошибок и хотя MINISAT Версия браузера также говорит, что тот же файл не удовлетворяет. Я нашел решение для того же самого в единицах и нулях для каждой переменной.
Вышеупомянутый алгоритм был мной опубликован в журнале, но был отклонен.
Мой вопрос: может ли кто-нибудь дать мне пример неудовлетворительного уравнения 3SAT, которое содержит только 3 переменные (или, может быть, немного больше ...) без какого-либо предложения, которое является точным обратным другому?
Если я смогу получить такое предложение, то алгоритм неверен (но все же он доказывает, что многие проблемы тестов SAT являются UNSAT), и это не докажет, что многие проблемы UNSAT в 1-й ссылке действительно являются SAT.
Это дразнит мой разум, и я надеюсь, что вы все это поймете, так как если приведенный выше алгоритм верен, то я доказал, что P = NP! Это также может начать революцию.
Кстати: я также отправил электронное письмо контактному лицу SATLIB, но через 2 дня все еще не получил ответа по поводу 2-го файла ссылки.
