Я понимаю причину вашего недоверия и я тоже заинтересован в проверке правильности доказательства.
Многие в Иинтернете обратили внимание на публикацию только из-за наличия открытого исходного кода, хотя я бы не хотел, чтобы о статье судили по реализации алгоритма. Реализация может помочь в понимании того, что написано в статье. В реализации могут быть баги, которые могут быть никак не связаны с доказательством. Их, конечно, тоже надо искать и исправлять — но это совершенно другая история.
Поиск изъянов исходя из анализа доказательства — это хороший подход. Я очень рад, что нашлись компетентные люди, которые обратили на доказательство внимание. Я постараюсь всячески содействовать в разъяснении положений статьи. Я буду стараться ответить на вопросы исходя из своего понимания и по необходимости буду привлекать В.Ф. Романова.
я предлагаю на сегодня закончить обсуждение. Если честно я уже просто физически устал — всю ночь фиксил баги :)
Обещаю завтра сделать новый топик (этот уже тяжелый), в котором мы разберем на примере этой формулы (она же исходная, да? :) все алгоритмы, включая унификацию и build HSS.
Я это понял, но нельзя проверять алгоритм изменяя в нем первые шаги. Теоретически не может получиться CTS с количеством уровней 8. Все остальное — может быть. Может быть даже пустая CTS, что будет свидетельствовать о невыполнимости формулы.
Насчет тождественной истины — да, меня это смущает :) Потому что в постановке 3-SAT участвуют скобки с тремя переменными. Я смогу объяснить как работает алгоритм, если вы добавите таких несвязанных литералов и покажете всю формулу целиком. Например в DIMACS CNF. Например, вот ваши 6 CTF уже в этом формате, сможете добавить остальные скобки?
Как так? Обязятельно входят, также по построению.
Только в другом порядке (имеют другую перестановку).
Набор переменных в начальной формуле и в CTS — одни и те же. В CTF — может быть только подмножество, но при преобразовании CTF -> CTS, переменные, которых нет в CTF дописываются к перестановке CTS (например, справа).
Базовая CTS не обязана накладывать никаких ограничений на остальные CTS. Они могут и должны быть несогласованными (discordant). Отсюда и название статьи.
Если у нас CTF_k будет пустым множеством, то мы должны определить дизъюнкцию как операцию над булевой переменной и пустым множеством. Как такое может быть?
Многие в Иинтернете обратили внимание на публикацию только из-за наличия открытого исходного кода, хотя я бы не хотел, чтобы о статье судили по реализации алгоритма. Реализация может помочь в понимании того, что написано в статье. В реализации могут быть баги, которые могут быть никак не связаны с доказательством. Их, конечно, тоже надо искать и исправлять — но это совершенно другая история.
Поиск изъянов исходя из анализа доказательства — это хороший подход. Я очень рад, что нашлись компетентные люди, которые обратили на доказательство внимание. Я постараюсь всячески содействовать в разъяснении положений статьи. Я буду стараться ответить на вопросы исходя из своего понимания и по необходимости буду привлекать В.Ф. Романова.
я предлагаю на сегодня закончить обсуждение. Если честно я уже просто физически устал — всю ночь фиксил баги :)
Обещаю завтра сделать новый топик (этот уже тяжелый), в котором мы разберем на примере этой формулы (она же исходная, да? :) все алгоритмы, включая унификацию и build HSS.
github.com/anjlab/sat3/wiki/How-to-read-output-files
То есть, в результате у нас множество CTS будет как там плюс одна CTS (седьмая, назовем ее CTS_7), которая включает тройку (a, b, c), вот она:
a b c
0 0 1
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1
Дальше мы должны все эти 7 CTS унифицировать.
Следующий шаг — выбрать одну CTS в качестве базовой (любую), например, ту, которую я только что привел выше.
Дальше мы должны построить 6 гиперструктур, в качестве базовой будет CTS_7, в качестве парной — соответственно одна из остальных.
Нужно ли пояснять, как делается унификация?
Это нужно принимать во внимание в доказательствах. CTS в данном случае — это не любая произвольная структура. А только та, которая получена из CTF.
Можете написать исходную формулу целиком? Тогда я точно пойму.
Это уже я загавариваюсь.
Теоретически не может получиться CTS с колчеством строк равным 8 на <u<каждом уровне. Обязательно в одном будет максимум 7.
Самое большое что может быть — это 8 строк на всех уровнях кроме одного. На одном будет максимум 7.
Я запутался :) То есть эти 6 структур — это CTS?
c habrahabr.ru/blogs/computer_science/112161/#comment_3592699
p cnf 0 0
1 2 6 0
1 -2 -6 0
-1 2 -6 0
-1 -2 6 0
3 4 7 0
3 -4 -7 0
-3 4 -7 0
-3 -4 7 0
5 6 7 0
5 -6 -7 0
-5 6 -7 0
-5 -6 7 0
1 2 8 0
1 -2 -8 0
-1 2 -8 0
-1 -2 8 0
3 4 9 0
3 -4 -9 0
-3 4 -9 0
-3 -4 9 0
5 8 -9 0
5 -8 9 0
-5 8 9 0
-5 -8 -9 0
Только в другом порядке (имеют другую перестановку).
Набор переменных в начальной формуле и в CTS — одни и те же. В CTF — может быть только подмножество, но при преобразовании CTF -> CTS, переменные, которых нет в CTF дописываются к перестановке CTS (например, справа).
F = (x_1 | x_2 | x_3)&(-x_1 | x_2 | x_3)&...&(x_(n-2) | x_(n-1) | x_n)
Декомпозиция формулы дает множество CTF:
F = CTF_1 & CTF_2 &… & CTF_k
Если у нас CTF_k будет пустым множеством, то мы должны определить дизъюнкцию как операцию над булевой переменной и пустым множеством. Как такое может быть?
Разве нет?
Она так строится. В CTF входят тройки из исходной формулы.