Комментарии 132
Первую публикацию не видел, поэтому ознакомлюсь с алгоритмом только сейчас.
Сходу появляется вопрос, не является ли алгоритм на самом деле псевдополиномиальным.
По поводу пункта 3 в разделе «Что дальше»: важна не сводимость других задач к этой, а сводимость этой задачи к другим.
Сходу появляется вопрос, не является ли алгоритм на самом деле псевдополиномиальным.
По поводу пункта 3 в разделе «Что дальше»: важна не сводимость других задач к этой, а сводимость этой задачи к другим.
НЛО прилетело и опубликовало эту надпись здесь
Когда разговаривают две бабушки на завалинке, это правда. Но статья научная и поэтому надо пользоваться терминологией теории алгоритмов.
Это и есть научная терминология. Но даже если подумать, то ведь нужно уметь NP полные задачи сводить к этой, чтобы любая NP полная задача решалась за полином + время сведения. Зачем эту задачу сводить к другим? Ну сведем эту задачу к NP полной, а смысл? Получим что решив другую задачу сможем решить и эту. Но решение этой то нам уже известно (если предложеный алгоритм верен).
НЛО прилетело и опубликовало эту надпись здесь
У задачи 3-ВЫП не может существовать псевдополиномиального алгоритма ввиду отсутствия у нее числовых параметров.
Я думаю на вас очень быстро обратят внимание если вы взломаете RSA :) Оно основывается на разложении числа на множители, np-полной задаче, которая сводится как и все NP к задаче 3-ВЫП.
НЛО прилетело и опубликовало эту надпись здесь
Если не ошибаюсь, то принадлежность факторизации классу np-complete не доказана.
Впрочем, в NP эта задача все же лежит, т.к. проверить ее решение за полиномиальное время можно — проверяем, действительно ли произведение данного набора чисел есть исходное (очевидно, полином), и для каждого из сомножителей применяем тест AKS (тоже полином).
Впрочем, в NP эта задача все же лежит, т.к. проверить ее решение за полиномиальное время можно — проверяем, действительно ли произведение данного набора чисел есть исходное (очевидно, полином), и для каждого из сомножителей применяем тест AKS (тоже полином).
Вот-вот! И скорее всего задача разложения на множители как раз не полна в NP. Она (в версии проблемы разрешимости) лежит как в классе NP, так и в классе co-NP. Если она NP-сложна, то это означает, что NP=co-NP, а это в свою очередь будет весьма неожиданно. (Хотя исходная статья-то вообще доказывает, что P=NP :-)
Сводится-то она сводится. Только в классических способах сведения степень полинома, возникающего при сведении, редко бывает меньше 2^5. Соответственно, с учетом сложности алгоритма n^4 получаем сложность результативного решения >= n^128. Полином. Но бывают экспоненты лучше)
Если честно, я не понял откуда получилось n^128 :)
Если сведение имеет какую то сложность, пусть 2^5, то эта сложность аддитивная. В результате мы все-равно получаем задачу 3-ВЫП. Только вот количество переменных, то есть n, может сильно вырасти.
При сложности n^4 и значении n=1000 — это уже не мало. В реальных задачах (в частности ниже есть ссылка на sat competition) для 3-SAT самый большой пример имеет n = 18000. Это много :)
На тех же соревнованиях есть примеры с количеством переменных n = 4 000 000 и это k-SAT. При сведении к 3-SAT количество переменных может увеличиться в разы.
Кроме этого не нужно забывать, что у задачи есть еще один параметр — это количество скобок — m. Она тоже фигурирует в формуле сложности. И часто m > n. То есть в формуле n^4 можно смело прибавлять 1 в общем случае.
Это все-равно долго, но: 1) статья имеет теоретическую значимость 2) это алгоритм, на котором построено доказательство. У меня есть несколько идей, как его улучшить и снизить степень полинома.
Еще при первом прочтении никто не обращает внимание на ресурсы памяти. Задача на n=1000 в текущей реализации требует 13ГБ ОЗУ. Это можно поправить, оптимизировав структуры данных. По моим подсчетам это позволит сократить объем памяти в 40 раз. Но все-равно для больших задач одной «персоналки» будет не достаточно. Нужно строить вычислительный кластер/сеть.
Если сведение имеет какую то сложность, пусть 2^5, то эта сложность аддитивная. В результате мы все-равно получаем задачу 3-ВЫП. Только вот количество переменных, то есть n, может сильно вырасти.
При сложности n^4 и значении n=1000 — это уже не мало. В реальных задачах (в частности ниже есть ссылка на sat competition) для 3-SAT самый большой пример имеет n = 18000. Это много :)
На тех же соревнованиях есть примеры с количеством переменных n = 4 000 000 и это k-SAT. При сведении к 3-SAT количество переменных может увеличиться в разы.
Кроме этого не нужно забывать, что у задачи есть еще один параметр — это количество скобок — m. Она тоже фигурирует в формуле сложности. И часто m > n. То есть в формуле n^4 можно смело прибавлять 1 в общем случае.
Это все-равно долго, но: 1) статья имеет теоретическую значимость 2) это алгоритм, на котором построено доказательство. У меня есть несколько идей, как его улучшить и снизить степень полинома.
Еще при первом прочтении никто не обращает внимание на ресурсы памяти. Задача на n=1000 в текущей реализации требует 13ГБ ОЗУ. Это можно поправить, оптимизировав структуры данных. По моим подсчетам это позволит сократить объем памяти в 40 раз. Но все-равно для больших задач одной «персоналки» будет не достаточно. Нужно строить вычислительный кластер/сеть.
> И часто m > n.
ну вообще в худшем случае m = 2^n
но мы всегда можем взять за длину слова языка произведение len = n*m поэтому результирующая сложность все равно меньше O(len^4)
На счет сводимости задач… ну тут все сложнее (читай интересней):
Допустим у вас есть NP-полный (NPC) язык, в котором слово длины n сводится полиномиально к слову длины n^3 (полином? полином) в другом NPC языке, который, предположим, распознается за полиномиальное время (пусть те же len^4).
То мы получим результирующую сложность (n^3)^4 = n^12
и если n будет, скажем, =1000, то n^4 еще приемлемо, то n^12 равное в данном случае 10^36, а это уже совсем не приемлемо
ну вообще в худшем случае m = 2^n
но мы всегда можем взять за длину слова языка произведение len = n*m поэтому результирующая сложность все равно меньше O(len^4)
На счет сводимости задач… ну тут все сложнее (читай интересней):
Допустим у вас есть NP-полный (NPC) язык, в котором слово длины n сводится полиномиально к слову длины n^3 (полином? полином) в другом NPC языке, который, предположим, распознается за полиномиальное время (пусть те же len^4).
То мы получим результирующую сложность (n^3)^4 = n^12
и если n будет, скажем, =1000, то n^4 еще приемлемо, то n^12 равное в данном случае 10^36, а это уже совсем не приемлемо
n^128 получается так.
У нас есть задача о факторизации с длиной входа n. С помощью сведения мы получаем 3SAT с длиной входа n^32. С помощью этого алгоритма мы решаем 3SAT за (n^32)^4 = n^128.
Расход памяти для МТ всегда ограничен временем алгоритма сверху (и логарифмом от него — снизу, но это неважно).
Количество скобок увеличивает длину входа не более чем в константу раз. Так что ее можно не учитывать.
У нас есть задача о факторизации с длиной входа n. С помощью сведения мы получаем 3SAT с длиной входа n^32. С помощью этого алгоритма мы решаем 3SAT за (n^32)^4 = n^128.
Расход памяти для МТ всегда ограничен временем алгоритма сверху (и логарифмом от него — снизу, но это неважно).
Количество скобок увеличивает длину входа не более чем в константу раз. Так что ее можно не учитывать.
Советую проверить себя на задачках с www.satcompetition.org/. Если справитесь — будьте уверены, учёные на вас внимание обратят.
Мы использовали некоторые задачи оттуда в своих тестах.
Я уже писал выше о размерности задач и невозможности решать большие экземпляры на персоналках.
Еще мы решали задачи отсюда: www.cs.ubc.ca/~hoos/SATLIB/benchm.html
На этой реализации масштабный эксперимент мы не ставили, решили несколько тысяч задач с числом переменных n=20, 50, 75, 100, 125, 400
Первые решаются за несколько секунд, для задачи в 400 переменных ушло 14 часов. Сейчас может быть уже 7, я пока не пробовал, вчера только закомитил хорошую оптимизацию.
Если у кого-то есть свободные вычислительные ресурсы, чтобы запустить решение — напишите здесь.
Следует написать, наверное, что я все это делаю в свободное от работы время, поэтому времени немного не хватает :)
Я уже писал выше о размерности задач и невозможности решать большие экземпляры на персоналках.
Еще мы решали задачи отсюда: www.cs.ubc.ca/~hoos/SATLIB/benchm.html
На этой реализации масштабный эксперимент мы не ставили, решили несколько тысяч задач с числом переменных n=20, 50, 75, 100, 125, 400
Первые решаются за несколько секунд, для задачи в 400 переменных ушло 14 часов. Сейчас может быть уже 7, я пока не пробовал, вчера только закомитил хорошую оптимизацию.
Если у кого-то есть свободные вычислительные ресурсы, чтобы запустить решение — напишите здесь.
Следует написать, наверное, что я все это делаю в свободное от работы время, поэтому времени немного не хватает :)
Вычислительные ресурсы есть. Много. Давайте попробуем большие задачи.
Я знаком с людьми, которые занимались задачами с satcompetition. Они тоже всё решали на персоналках. Более того, большинство солверов на satcompetition — однопоточные.
400 переменных за 14 часов — это, по-моему, довольно слабо. Я в своё время по работе решал mixed-integer задачи линейного программирования (тоже NP-полная задача). Использовал свободный glpk и коммерческий cplex, и они работали на очень больших объёмах данных. Насколько я понимаю, они пользовались методом ветвей и границ.
Ещё я посмотрел вашу статью. Я до конца всё не стал проверять, но некоторые вопросы появились. Задам два мета-вопроса.
1. Первое что вы делаете — это разбиваете формулу на несколько формул с последовательными номерами переменных. Причём, я так понял, что конкретное количество таких формул, покуда оно полиномиально (а их не может быть больше чем n^3), не влияет на полиномиальность алгоритма. В таком случае, почему бы не брать в качестве таких подформул отдельные дизъюнкции? Вопрос о разрешимости и совместной разрешимости двух подформул сразу становится тривиальным.
2. Я не до конца разобрался в вашей гиперструктуре, но тем не менее. В ключевом месте алгоритма, когда вы проверяете существование удовлетворяющего набора для всех подформул одновременно заявлено, что вы одновременно проходите по k гиперструктурам. Вопрос: что вы делаете когда доходите до ветвления, то есть до ситуации когда есть два допустимых варианта дальнейшего продвижения по вашему графу?
400 переменных за 14 часов — это, по-моему, довольно слабо. Я в своё время по работе решал mixed-integer задачи линейного программирования (тоже NP-полная задача). Использовал свободный glpk и коммерческий cplex, и они работали на очень больших объёмах данных. Насколько я понимаю, они пользовались методом ветвей и границ.
Ещё я посмотрел вашу статью. Я до конца всё не стал проверять, но некоторые вопросы появились. Задам два мета-вопроса.
1. Первое что вы делаете — это разбиваете формулу на несколько формул с последовательными номерами переменных. Причём, я так понял, что конкретное количество таких формул, покуда оно полиномиально (а их не может быть больше чем n^3), не влияет на полиномиальность алгоритма. В таком случае, почему бы не брать в качестве таких подформул отдельные дизъюнкции? Вопрос о разрешимости и совместной разрешимости двух подформул сразу становится тривиальным.
2. Я не до конца разобрался в вашей гиперструктуре, но тем не менее. В ключевом месте алгоритма, когда вы проверяете существование удовлетворяющего набора для всех подформул одновременно заявлено, что вы одновременно проходите по k гиперструктурам. Вопрос: что вы делаете когда доходите до ветвления, то есть до ситуации когда есть два допустимых варианта дальнейшего продвижения по вашему графу?
satcompetition — это соревнования для алгоритмов, основанных на эвристиках. Они очень быстрые в большинстве случаев. Алгоритм Романова — это алгоритм общего назначения. Он работает всегда одинаково (O(n^4*m)) для всех случаев.
По вопросам.
1. Вы правильно поняли про CTF — это формулы с определенным порядком дизъюнктов. В дальнейшем же алгоритме участвуют их дополнения. Причем дополнения строятся так, что количество переменных в них все-равно равно n. Даже если в какой то CTF была одна тройка, то ее дополнение будет содержать n-2 уровня на каждом из которых по 8 троек, кроме одного уровня — на нем будет 7 троек.
2. В этом случае вершина продвигается (shift) по обоим ребрам. Причем она должна быть продвинута непусто во всех гиперструктурах. Если хотя бы в одной гиперструктуре она продвигается пустой, то считается, что во всех гиперструктурах она продвинулась пустой.
По вопросам.
1. Вы правильно поняли про CTF — это формулы с определенным порядком дизъюнктов. В дальнейшем же алгоритме участвуют их дополнения. Причем дополнения строятся так, что количество переменных в них все-равно равно n. Даже если в какой то CTF была одна тройка, то ее дополнение будет содержать n-2 уровня на каждом из которых по 8 троек, кроме одного уровня — на нем будет 7 троек.
2. В этом случае вершина продвигается (shift) по обоим ребрам. Причем она должна быть продвинута непусто во всех гиперструктурах. Если хотя бы в одной гиперструктуре она продвигается пустой, то считается, что во всех гиперструктурах она продвинулась пустой.
Окей, я решил честно почитать ваш текст и разобраться. По ходу дела ещё пара вопросов.
1. Следует ли из вашей работы, что множество удовлетворяющих наборов для любой 3-SAT задачи обязательно задаётся какой-нибудь CT-структурой? Кажется, что-то подобное подразумевается во втором абзаце раздела 4.
2. Верно ли я понимаю, что гиперструктура для двух наборов упорядоченных структур — это просто граф одной из структур, в вершинах которого стоят копии графа второй структуры, отфильтрованные в соответствии со значениями 3-х переменных, заданных в этой вершине?
3. Правильно ли я понимаю, что путь в гиперструктуре — это путь во внешнем графе такой что структуры стоящие в любых двух его _соседних_ вершинах совместны?
1. Следует ли из вашей работы, что множество удовлетворяющих наборов для любой 3-SAT задачи обязательно задаётся какой-нибудь CT-структурой? Кажется, что-то подобное подразумевается во втором абзаце раздела 4.
2. Верно ли я понимаю, что гиперструктура для двух наборов упорядоченных структур — это просто граф одной из структур, в вершинах которого стоят копии графа второй структуры, отфильтрованные в соответствии со значениями 3-х переменных, заданных в этой вершине?
3. Правильно ли я понимаю, что путь в гиперструктуре — это путь во внешнем графе такой что структуры стоящие в любых двух его _соседних_ вершинах совместны?
Попробую ответить на два вопроса (если отвечаю неправильно — сильно не бить).
1. Нет, не следует. Точнее, не следует явно (если мы верим что в работе есть ошибка — то из нее автоматически следует все что угодно). Второй абзац раздела 4 утверждает, что для пары СКТ S_1 и S_2 существует пара СКТ S_1^0 и S_2^0 со следующими свойствами:
S_1^0 \subseteq S_1, S_2^0 \subseteq S_2, и всякая строка из S_i^0 входит в какой-то набор, удовлетворяющий S_1 и S_2.
2. Там еще что-то с ребрами есть. Правда, я пока не очень понял, что именно.
3. Нет. Все вершины пути должны быть совместны в совокупности.
PS. Приношу свои извинения людям, не владеющим TeX'ом
1. Нет, не следует. Точнее, не следует явно (если мы верим что в работе есть ошибка — то из нее автоматически следует все что угодно). Второй абзац раздела 4 утверждает, что для пары СКТ S_1 и S_2 существует пара СКТ S_1^0 и S_2^0 со следующими свойствами:
S_1^0 \subseteq S_1, S_2^0 \subseteq S_2, и всякая строка из S_i^0 входит в какой-то набор, удовлетворяющий S_1 и S_2.
2. Там еще что-то с ребрами есть. Правда, я пока не очень понял, что именно.
3. Нет. Все вершины пути должны быть совместны в совокупности.
PS. Приношу свои извинения людям, не владеющим TeX'ом
1. То есть множества, задающиеся S_1^0 и S_2^0 являются подмножествами множества удовлетворяющих наборов, но могут не исчерпывать его, так? Формально говоря, придраться не к чему, но у меня есть ощущение, что в таком случае мы теряем какие-то решения и можем прийти в итоге к false negative.
3. В таком случае, по-моему, задача о нахождении такого пути сама по себе становится NP-полной. Нет?
3. В таком случае, по-моему, задача о нахождении такого пути сама по себе становится NP-полной. Нет?
1. Нет, наоборот — множество наборов, удовлетворяющих S_1 и S_2 есть подмножество наборов, удовлетворяющих S_i^0.
3. Ну, насчет NP-полноты надо подумать, но она действительно становится сложной. Но мы ищем такой путь не для произвольной гиперструктуры, а для некоторой специальной (полученной после эффективной процедуры).
3. Ну, насчет NP-полноты надо подумать, но она действительно становится сложной. Но мы ищем такой путь не для произвольной гиперструктуры, а для некоторой специальной (полученной после эффективной процедуры).
1. А Вы не могли бы дать ссылку на толкование в статье? В том абзаце просто написано «there exist two optimal CT structures», причём определения «optimal» я нигде не нашёл. Про них написано только что они «each formed as the union of JS sets», про какие именно множества идёт речь — не понятно.
3. Так а чем эта специальная гиперструктура отличается от общего случая-то? Как я понял из определения гиперструктуры, результат не должен зависеть от процедуры.
Да, кстати, я дошёл до теоремы 1, которая утверждает, что если нам удалось построить непустую гиперструктуру, то в ней обязательно найдётся путь. Сейчас прочитаю ещё раз, как строится гиперструктура и либо попробую придумать контрпример, либо почитаю доказательство.
3. Так а чем эта специальная гиперструктура отличается от общего случая-то? Как я понял из определения гиперструктуры, результат не должен зависеть от процедуры.
Да, кстати, я дошёл до теоремы 1, которая утверждает, что если нам удалось построить непустую гиперструктуру, то в ней обязательно найдётся путь. Сейчас прочитаю ещё раз, как строится гиперструктура и либо попробую придумать контрпример, либо почитаю доказательство.
1. Похоже, что русская и английская версии несколько отличаются. В русской явно выписано: «из S_1 и S_2 соответственно исключены все строки, не входящие в объединение элементарных СКТ, представляющих СВН в каждой из структур».
3. Утверждается, что каждая вершина j-го яруса специальной гиперструктуры есть объединение j-пересечений, т.е. эта вершина разбивается на (возможно, пересекающиеся) элементарные подструктуры X_i. Каждая X_i обладает следующим свойством:
существует вершина a_1 из 1го яруса, a_2 из 2го, ..., a_j из j-го такие, что X_i входит (как подструктура) в a_1, a_2, ...., a_j.
Тогда, поскольку пересечение вершины a_i и a_{i+1} пусто, если от a_i нет ребра к a_{i+1}, есть путь (a_1, a_2, ..., a_j) — такой, что пересечение подструтур, стоящих в его вершинах, непусто.
Подставив j=n-2, получим путь в гиперструктуре.
Пока что мне наиболее «подозрительным» кажется этап параллельного построения гиперструктур.
3. Утверждается, что каждая вершина j-го яруса специальной гиперструктуры есть объединение j-пересечений, т.е. эта вершина разбивается на (возможно, пересекающиеся) элементарные подструктуры X_i. Каждая X_i обладает следующим свойством:
существует вершина a_1 из 1го яруса, a_2 из 2го, ..., a_j из j-го такие, что X_i входит (как подструктура) в a_1, a_2, ...., a_j.
Тогда, поскольку пересечение вершины a_i и a_{i+1} пусто, если от a_i нет ребра к a_{i+1}, есть путь (a_1, a_2, ..., a_j) — такой, что пересечение подструтур, стоящих в его вершинах, непусто.
Подставив j=n-2, получим путь в гиперструктуре.
Пока что мне наиболее «подозрительным» кажется этап параллельного построения гиперструктур.
Я тоже сначала читал русский вариант, а потом нашёл по ссылке в этом посте более новый английский и шёл по нему.
Мне кажется, проблема уже в шаге для двух гиперструктур. См. habrahabr.ru/blogs/computer_science/112161/#comment_3589778
Мне кажется, проблема уже в шаге для двух гиперструктур. См. habrahabr.ru/blogs/computer_science/112161/#comment_3589778
О! Я, кажется, нашёл принципиальный вопрос.
Автор определяет объединение структур и, кажется, предполагает, что при этой операции множества, описываемые структурами также объединяются.
Это, конечно, не так. Рассмотрим структуры:
0 1 1 _
_ 1 1 0
и
1 1 1 _
_ 1 1 1
Первая из них описывает одно решение: 0110, вторая — тоже одно 1111. Однако если мы их механически объединим, то получится вот такая структура:
0 1 1 _
1 1 1 _
_ 1 1 0
_ 1 1 1
Этой структуре помимо 0110 и 1111 соответствуют и 0111 и 1110.
Встаёт вопрос, где автор на это полагается? А вот где. В доказательстве теоремы 1 он доказывает, что структура в каждой вершине будет объединением каких-то пересечений структур. Проблема в том, что не все наборы, описываемые такой структурой будут решениями. То есть из того, что в каждой вершине есть непустая структура, не следует, что там существует решение.
Прошу прощения, если я что-то понял не так.
Автор определяет объединение структур и, кажется, предполагает, что при этой операции множества, описываемые структурами также объединяются.
Это, конечно, не так. Рассмотрим структуры:
0 1 1 _
_ 1 1 0
и
1 1 1 _
_ 1 1 1
Первая из них описывает одно решение: 0110, вторая — тоже одно 1111. Однако если мы их механически объединим, то получится вот такая структура:
0 1 1 _
1 1 1 _
_ 1 1 0
_ 1 1 1
Этой структуре помимо 0110 и 1111 соответствуют и 0111 и 1110.
Встаёт вопрос, где автор на это полагается? А вот где. В доказательстве теоремы 1 он доказывает, что структура в каждой вершине будет объединением каких-то пересечений структур. Проблема в том, что не все наборы, описываемые такой структурой будут решениями. То есть из того, что в каждой вершине есть непустая структура, не следует, что там существует решение.
Прошу прощения, если я что-то понял не так.
Честно говоря, не нашел, где утверждается, что все такие наборы будут решениями.
Насколько я понимаю, утверждается, что подструктура в вершине может быть представлена как объединение решений.
Насколько я понимаю, утверждается, что подструктура в вершине может быть представлена как объединение решений.
Страница 4 последний абзац, там вводится понятие побочных (superfluous) подструктур. Это как раз 0111 и 1110. В оставшейся части статьи как раз и идет борьба с такими подструктурами, в частности процедурой фильтрации. Процедура фильтрации определяется как часть операции продвижения (shift). Она гарантирует, что каждая вершина не будет состоять только из побочных структур.
Не следует. Но если последний уровень системы гиперструктур построен не пустым, то значит в каждой вершине последнего уровня есть решение по построению. Как его найти — другой вопрос.
То есть из того, что в каждой вершине есть непустая структура, не следует, что там существует решение.
Не следует. Но если последний уровень системы гиперструктур построен не пустым, то значит в каждой вершине последнего уровня есть решение по построению. Как его найти — другой вопрос.
Окей. Мне кажется, мы так избавляемся от тривиальных связей типа 1-й бит равен 4-му, но не справимся с более сложными зависимостями.
Рассмотрим набор: 0xx1xx0, 1xx0xx0, 0xx0xx1, 1xx1xx1. «Проекция» ни с какого отдельного уровня не отсечёт у нас решения типа 0xx0xx0.
Рассмотрим набор: 0xx1xx0, 1xx0xx0, 0xx0xx1, 1xx1xx1. «Проекция» ни с какого отдельного уровня не отсечёт у нас решения типа 0xx0xx0.
Правда, я пока не уверен, что предложенный набор может получиться в какой-то вершине гиперструктуры…
Во время фильтрации очередная структура, которую мы двигаем по ребру вниз, сначала конкретизируется значениями переменных в целевой вершине (получаем промежуточную подструктуру), затем постепенно пересекается со всеми верхними уровнями по очереди, сохраняя и объединяя в себе все j-пересечения.
Если полученная (промежуточная) структура пересечется пусто хотя бы с одним уровнем — значит считаем, что продвижение в целевую вершину по данному ребру не удалось.
А если со всеми уровнями пересечение было не пустым, то в целевой вершине мы сохраняем хотя бы одно непустое j-пересечение.
Если полученная (промежуточная) структура пересечется пусто хотя бы с одним уровнем — значит считаем, что продвижение в целевую вершину по данному ребру не удалось.
А если со всеми уровнями пересечение было не пустым, то в целевой вершине мы сохраняем хотя бы одно непустое j-пересечение.
Мне всё ещё кажется, что ошибка есть уже для двух структур, но придумать контрпример не получается, так что задам вопрос про теорему 2.
Рассмотрим следующую конструкцию. Для простоты пуская первая структура будет соответствовать вообще всем наборам, а каждая из остальных — будет иметь дело только с одной тройкой переменных. Итак, пускай мы имеем следующие структуры (у каждой из них будет в точности один нетривиальный уровень, цифрами сверху обозначены номера переменных):
1 2 6
0 0 0
0 1 1
1 0 1
1 1 0
3 4 7
0 0 0
0 1 1
1 0 1
1 1 0
5 6 7
0 0 0
0 1 1
1 0 1
1 1 0
1 2 8
0 0 0
0 1 1
1 0 1
1 1 0
3 4 9
0 0 0
0 1 1
1 0 1
1 1 0
5 8 9
0 0 1
0 1 0
1 0 0
1 1 1
Объясню, что значат эти формулы (сложение — битовое, то бишь xor):
x6 = x1 + x2
x7 = x3 + x4
x5 + x6 + x7 = 0
x8 = x1 + x2
x9 = x3 + x4
x5 + x8 + x9 = 1
То бишь первые три в совокупности означают, что среди первых пяти битов есть чётное количество единиц, а оставшиеся три — что нечётное.
Несложно заметить, что все эти формулы в совокупности не совместны. При этом никакая из них не противоречит ни какой другой и любая комбинация значений любых двух битов оказывается допустима.
Собственно вопрос: в какой момент при фильтрации или унификации из этих структур пропадёт хоть одна строчка?
Рассмотрим следующую конструкцию. Для простоты пуская первая структура будет соответствовать вообще всем наборам, а каждая из остальных — будет иметь дело только с одной тройкой переменных. Итак, пускай мы имеем следующие структуры (у каждой из них будет в точности один нетривиальный уровень, цифрами сверху обозначены номера переменных):
1 2 6
0 0 0
0 1 1
1 0 1
1 1 0
3 4 7
0 0 0
0 1 1
1 0 1
1 1 0
5 6 7
0 0 0
0 1 1
1 0 1
1 1 0
1 2 8
0 0 0
0 1 1
1 0 1
1 1 0
3 4 9
0 0 0
0 1 1
1 0 1
1 1 0
5 8 9
0 0 1
0 1 0
1 0 0
1 1 1
Объясню, что значат эти формулы (сложение — битовое, то бишь xor):
x6 = x1 + x2
x7 = x3 + x4
x5 + x6 + x7 = 0
x8 = x1 + x2
x9 = x3 + x4
x5 + x8 + x9 = 1
То бишь первые три в совокупности означают, что среди первых пяти битов есть чётное количество единиц, а оставшиеся три — что нечётное.
Несложно заметить, что все эти формулы в совокупности не совместны. При этом никакая из них не противоречит ни какой другой и любая комбинация значений любых двух битов оказывается допустима.
Собственно вопрос: в какой момент при фильтрации или унификации из этих структур пропадёт хоть одна строчка?
Я не совсем понял постановку вопроса. Точнее эти структуры. Это одна формула разложенная на несколько CTF?
Чтобы убедиться, что мы говорим об одном и том же.
1) Процедура унификации — независимая операция, которая применяется не к CTF, а к CTS. У каждой CTS должен быть одинаковый набор переменных, но при этом разные перестановки.
2) Процедура фильтрации применяется для какой-либо подструктуры-вершины, которая находится в частично построенной гиперструктуре. И запускается входе алгоритма продвижения этой вершины по ребру на один уровень вниз.
Чтобы убедиться, что мы говорим об одном и том же.
1) Процедура унификации — независимая операция, которая применяется не к CTF, а к CTS. У каждой CTS должен быть одинаковый набор переменных, но при этом разные перестановки.
2) Процедура фильтрации применяется для какой-либо подструктуры-вершины, которая находится в частично построенной гиперструктуре. И запускается входе алгоритма продвижения этой вершины по ребру на один уровень вниз.
Это одна 3-SAT формула, разложенная в 7 CTF, первая из которых соответсвует тождественной истине и потому не приведена, а остальные 6 — те что перечислены.
Таблички, которые я выписал — это CTF и есть, с учётом того, что я не стал выписывать уровни, на которые в них нет никаких ограничений, и в которых, как следствие, присутствуют все возможные наборы из трёх битов. Перестановки переменных: 1 2 6 ..., 3 4 7 ..., 5 6 7 ..., 1 2 8 ..., 3 4 9 ..., 5 8 9… Вместо многоточий в каждой перестановке оставшиеся 6 переменных в произвольном порядке.
На всякий случай, чтобы в первой структуре значения переменных точно никак не влияли на соседние, можно ещё докинуть добавочных переменных, на которые нет никаких ограничений и расставить их в первой (базовой) CTF между значимыми переменными, так чтобы в любом уровне была максимум одна значимая переменная. Но кажется и без этого работает.
Таблички, которые я выписал — это CTF и есть, с учётом того, что я не стал выписывать уровни, на которые в них нет никаких ограничений, и в которых, как следствие, присутствуют все возможные наборы из трёх битов. Перестановки переменных: 1 2 6 ..., 3 4 7 ..., 5 6 7 ..., 1 2 8 ..., 3 4 9 ..., 5 8 9… Вместо многоточий в каждой перестановке оставшиеся 6 переменных в произвольном порядке.
На всякий случай, чтобы в первой структуре значения переменных точно никак не влияли на соседние, можно ещё докинуть добавочных переменных, на которые нет никаких ограничений и расставить их в первой (базовой) CTF между значимыми переменными, так чтобы в любом уровне была максимум одна значимая переменная. Но кажется и без этого работает.
Прошу прощения, таблички — CT-структуры, а не CTF.
Еще одно уточнение про первую структуру. Вы говорите что она соответствует тождественной истине. Это значит что в ней на всех ярусах по 8 строк? Если да, то такая формула не может быть выполнимой. Когда вы будете строить CTS — то есть дополнение к CTF — получите пустую структуру.
Или я опять неправильно понял?
Или я опять неправильно понял?
Про остальные 6 CTF я понял.
Секундочку. Если мы рассмотрим пустую 3-SAT формулу, она будет истинной для любого набора значений, так как пустая конъюнкция = истина. На каждом уровне у неё действительно будет по 8 строк.
В моём случае я в качестве внешней структуры взял тождественную истину, чтобы все существенные формулы находились в одинаковой ситуации и каждой формуле соответствовала ровно одна гиперструктура.
В моём случае я в качестве внешней структуры взял тождественную истину, чтобы все существенные формулы находились в одинаковой ситуации и каждой формуле соответствовала ровно одна гиперструктура.
Про фильтрацию и унификацию. В результате фильтрации, по-моему, тут вообще ничего не должно пропасть, так как каждая структура consistent.
В вершинах гиперструктуры, естественно, будут только те строчки, в которых на нужной позиции стоит нужный бит, но так как все рёбра у нас будут присутствовать (любая пара битов допустима), то дойдя до нижнего уровня в гиперструктуре, мы ничего не потеряем.
Как я понимаю унификацию: мы сравниваем соответсвующие вершины в гиперструктурах и смотрим на следующие ситуации:
а) в одной структуре в какой-то позиции всегда один и тот же бит,
б) два бита всегда ходят вместе.
Ни того, ни другого у нас, кажется, в данном примере не будет.
В вершинах гиперструктуры, естественно, будут только те строчки, в которых на нужной позиции стоит нужный бит, но так как все рёбра у нас будут присутствовать (любая пара битов допустима), то дойдя до нижнего уровня в гиперструктуре, мы ничего не потеряем.
Как я понимаю унификацию: мы сравниваем соответсвующие вершины в гиперструктурах и смотрим на следующие ситуации:
а) в одной структуре в какой-то позиции всегда один и тот же бит,
б) два бита всегда ходят вместе.
Ни того, ни другого у нас, кажется, в данном примере не будет.
Не понимаю что вы имеете ввиду, когда говорите, что каждая структура consistent. Такого определения структур в статье нет. Что вы имеете ввиду?
Фильтрация и унификация — никак не связаны. Это совершенно разные операции.
Такого не может быть по правилу построения CTS. CTS — это дополнение CTF. То что вы говорите может получиться, только если в CTF у нас нет ниодной скобки.
Унификация никак не связана с гиперструктурой. Унификация — это q-арная операция CTS с разными перестановками переменных (то есть несогласованных). Кстати, единственно-возможная операция для таких несогласованных структур.
Фильтрация и унификация — никак не связаны. Это совершенно разные операции.
но так как все рёбра у нас будут присутствовать
Такого не может быть по правилу построения CTS. CTS — это дополнение CTF. То что вы говорите может получиться, только если в CTF у нас нет ниодной скобки.
Унификация никак не связана с гиперструктурой. Унификация — это q-арная операция CTS с разными перестановками переменных (то есть несогласованных). Кстати, единственно-возможная операция для таких несогласованных структур.
А почему в CTF должна быть хотя бы одна скобка?
По определению :)
Она так строится. В CTF входят тройки из исходной формулы.
Она так строится. В CTF входят тройки из исходной формулы.
Да. Нигде не указано, что их должно быть не ноль.
Кроме того, здесь существенно не то, что базовая CTS полна, а то, что она не накладывает ограничения на переменные в остальных CTS. Этого добиться легко.
Кроме того, здесь существенно не то, что базовая CTS полна, а то, что она не накладывает ограничения на переменные в остальных CTS. Этого добиться легко.
Если у нас есть исходная формула F в CNF, то это:
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 будет пустым множеством, то мы должны определить дизъюнкцию как операцию над булевой переменной и пустым множеством. Как такое может быть?
Разве нет?
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 будет пустым множеством, то мы должны определить дизъюнкцию как операцию над булевой переменной и пустым множеством. Как такое может быть?
Разве нет?
Базовая CTS не обязана накладывать никаких ограничений на остальные CTS. Они могут и должны быть несогласованными (discordant). Отсюда и название статьи.
Я хотел сказать, что переменные, входящие в базовую CTS, не входят в остальные.
Как так? Обязятельно входят, также по построению.
Только в другом порядке (имеют другую перестановку).
Набор переменных в начальной формуле и в CTS — одни и те же. В CTF — может быть только подмножество, но при преобразовании CTF -> CTS, переменные, которых нет в CTF дописываются к перестановке CTS (например, справа).
Только в другом порядке (имеют другую перестановку).
Набор переменных в начальной формуле и в CTS — одни и те же. В CTF — может быть только подмножество, но при преобразовании CTF -> CTS, переменные, которых нет в CTF дописываются к перестановке CTS (например, справа).
Прошу прощения, я путаюсь в сокращениях. Я имел в виду, что в качестве первой структуры мы возьмём пустую (тожедественно истинную) формулу и, соответсвенно, полную структуру.
Если по каким-то причинам Вас смущает пустая формула, то можно добавить не связанных переменных и написать с ними какую-нибудь скобку. Это ни на что не повлияет.
Да, таблички, которые я перечислил — это структуры, а не формулы. То есть перечисления допустимых наборов битов.
Если по каким-то причинам Вас смущает пустая формула, то можно добавить не связанных переменных и написать с ними какую-нибудь скобку. Это ни на что не повлияет.
Да, таблички, которые я перечислил — это структуры, а не формулы. То есть перечисления допустимых наборов битов.
Насчет тождественной истины — да, меня это смущает :) Потому что в постановке 3-SAT участвуют скобки с тремя переменными. Я смогу объяснить как работает алгоритм, если вы добавите таких несвязанных литералов и покажете всю формулу целиком. Например в DIMACS CNF. Например, вот ваши 6 CTF уже в этом формате, сможете добавить остальные скобки?
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
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, а от этого зависит анализ того, как она работает.
Я бы хотел разобраться, как сработает последний шаг алгоритма (параллельное продвижение по гиперструктурам) в случае если формула разбита именно на такие 7 CT-структур, из которых, в свою очередь, получается 6 гиперструктур.
Если я просто сведу всё в одну формулу, то Ваша программа сама разобъёт формулу на несколько CTS, а от этого зависит анализ того, как она работает.
Я бы хотел разобраться, как сработает последний шаг алгоритма (параллельное продвижение по гиперструктурам) в случае если формула разбита именно на такие 7 CT-структур, из которых, в свою очередь, получается 6 гиперструктур.
Я это понял, но нельзя проверять алгоритм изменяя в нем первые шаги. Теоретически не может получиться CTS с количеством уровней 8. Все остальное — может быть. Может быть даже пустая CTS, что будет свидетельствовать о невыполнимости формулы.
Теоретически не может получиться CTS с количеством уровней 8.
Это уже я загавариваюсь.
Теоретически не может получиться CTS с колчеством строк равным 8 на <u<каждом уровне. Обязательно в одном будет максимум 7.
Давайте добавим еще одну переменную, которая будет входить только в базовую формулу. Базовая формула, соответственно, будет иметь, например, такое вид:
(y ∨ x1 ∨ x2).
(y ∨ x1 ∨ x2).
Базовая формула — это исходная? Первая скобка как вы написали, а остальные — как Олег написал?
Базовая формула — это часть исходной формулы, отвечающая базисной структуры.
Соответственно, исходная формула имеет вид (для «надежности» чуть-чуть поправлю базовую формулу):
(a ∨ b ∨ c) & (скобки, задающие структуры в #comment_3592699
Соответственно, исходная формула имеет вид (для «надежности» чуть-чуть поправлю базовую формулу):
(a ∨ b ∨ c) & (скобки, задающие структуры в #comment_3592699
Так, теперь понял. И что с этим делаем дальше? :)
Дальше строим базисный граф на основании (a ∨ b ∨ c), берем семь приведенных выше CTF, строим 7 гиперструктур и применяем алгоритм параллельного формирования гиперструктур.
(если я все правильно понял — конкретно в этот пример не вникал, сам я все еще не уверен в истинности теоремы 1)
(если я все правильно понял — конкретно в этот пример не вникал, сам я все еще не уверен в истинности теоремы 1)
Что приведено выше — это CTS, как мы разобрались здесь (comment_3592960)
То есть, в результате у нас множество 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 будет как там плюс одна 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, в качестве парной — соответственно одна из остальных.
Нужно ли пояснять, как делается унификация?
Простите, обсчитался.
Правильно ли я понимаю, что унификация этих 7 CTF их не изменит, т.к. каждая переменная бывает и нулем, и единицей в каждой из структур. А с помощью подходящей нумерации переменных в оставшихся структурах можно добиться того, что две переменные в разных структурах оказываются рядом только если ярусы, им соответствующие, заполнены полностью.
Правильно ли я понимаю, что унификация этих 7 CTF их не изменит, т.к. каждая переменная бывает и нулем, и единицей в каждой из структур. А с помощью подходящей нумерации переменных в оставшихся структурах можно добиться того, что две переменные в разных структурах оказываются рядом только если ярусы, им соответствующие, заполнены полностью.
Мало того, что в каждой позиции каждой структуры может встречаться и нолик и единица. В каждых двух позициях может находиться любая пара битов. Унификация ещё и на пары битов смотрит.
На счёт того, кто с кем находится рядом, я пока не понял, насколько это существенно. Если окажется что существенно, нужно во всех структурах между соседними переменными вставить дополнительные переменные на которые нет никаких ограничений.
На счёт того, кто с кем находится рядом, я пока не понял, насколько это существенно. Если окажется что существенно, нужно во всех структурах между соседними переменными вставить дополнительные переменные на которые нет никаких ограничений.
Кстати, блок-схему алгоритма в общем виде здесь можно найти, если это поможет:
github.com/anjlab/sat3/wiki/How-to-read-output-files
github.com/anjlab/sat3/wiki/How-to-read-output-files
Поправка. 6 гиперструктур. :)
Я тоже не уверен в истинности теоремы 1, но строго говоря, она не существенна, так как мы можем принять что каждая CTS соответствует ровно одной тройке, а не цепочке троек (что я собственно и сделал в своём примере) и тогда теорема 1 станет тривиальной.
Я тоже не уверен в истинности теоремы 1, но строго говоря, она не существенна, так как мы можем принять что каждая CTS соответствует ровно одной тройке, а не цепочке троек (что я собственно и сделал в своём примере) и тогда теорема 1 станет тривиальной.
Почему нельзя?
Доказательства теорем 1 и 2 никак не пользуются тем, что CTS, на которых они работают построены именно алгоритмом из раздела 3. Следовательно, последние шаги алгоритма должны работать на любых CTS, соответсвующих определению. Если Вас продолжает смущать наличие полной CTS, добавим три переменные x10, x11, x12 и пусть в нашей внешней CTS будет уровень
Доказательства теорем 1 и 2 никак не пользуются тем, что CTS, на которых они работают построены именно алгоритмом из раздела 3. Следовательно, последние шаги алгоритма должны работать на любых CTS, соответсвующих определению. Если Вас продолжает смущать наличие полной CTS, добавим три переменные x10, x11, x12 и пусть в нашей внешней CTS будет уровень
10 11 12 0 0 0
Any CTS is composed of the triplets that are absent in the corresponding CTF, at each tier respectively
Это нужно принимать во внимание в доказательствах. CTS в данном случае — это не любая произвольная структура. А только та, которая получена из CTF.
Можете написать исходную формулу целиком? Тогда я точно пойму.
Окей. Я буду пользоваться ^ в качестве xor.
not (x1 ^ x2 ^ x6) &
not (x3 ^ x4 ^ x7) & not (x5 ^ x6 ^ x7) &
not (x1 ^ x2 ^ x8) &
not (x3 ^ x4 ^ x9) &
(x5 ^ x8 ^ x9) &
(x10 | x11 | x12)
Последняя тройка — для внешней CTS. Если нужно, могу расписать в 3-SAT — каждая строчка кроме последней заменится на 4 дизъюнкции.
not (x1 ^ x2 ^ x6) &
not (x3 ^ x4 ^ x7) & not (x5 ^ x6 ^ x7) &
not (x1 ^ x2 ^ x8) &
not (x3 ^ x4 ^ x9) &
(x5 ^ x8 ^ x9) &
(x10 | x11 | x12)
Последняя тройка — для внешней CTS. Если нужно, могу расписать в 3-SAT — каждая строчка кроме последней заменится на 4 дизъюнкции.
Лучше распишите, я могу напутать с раскрытием скобок и это затянется еще :)
Пожалуйста. Надеюсь, я сам нигде не ошибся:
(x1 | x2 | !x6) & (x1 | !x2 | x6) & (!x1 | x2 | x6) & (!x1 | !x2 | !x6) &
(x3 | x4 | !x7) & (x3 | !x4 | x7) & (!x3 | x4 | x7) & (!x3 | !x4 | !x7) &
(x5 | x6 | !x7) & (x5 | !x6 | x7) & (!x5 | x6 | x7) & (!x5 | !x6 | !x7) &
(x1 | x2 | !x8) & (x1 | !x2 | x8) & (!x1 | x2 | x8) & (!x1 | !x2 | !x8) &
(x3 | x4 | !x9) & (x3 | !x4 | x9) & (!x3 | x4 | x9) & (!x3 | !x4 | !x9) &
(x5 | x8 | x9) & (x5 | !x8 | !x9) & (!x5 | x8 | !x9) & (!x5 | !x8 | x9) &
(x10 | x11 | x12)
(x1 | x2 | !x6) & (x1 | !x2 | x6) & (!x1 | x2 | x6) & (!x1 | !x2 | !x6) &
(x3 | x4 | !x7) & (x3 | !x4 | x7) & (!x3 | x4 | x7) & (!x3 | !x4 | !x7) &
(x5 | x6 | !x7) & (x5 | !x6 | x7) & (!x5 | x6 | x7) & (!x5 | !x6 | !x7) &
(x1 | x2 | !x8) & (x1 | !x2 | x8) & (!x1 | x2 | x8) & (!x1 | !x2 | !x8) &
(x3 | x4 | !x9) & (x3 | !x4 | x9) & (!x3 | x4 | x9) & (!x3 | !x4 | !x9) &
(x5 | x8 | x9) & (x5 | !x8 | !x9) & (!x5 | x8 | !x9) & (!x5 | !x8 | x9) &
(x10 | x11 | x12)
Олег, Михаил,
я предлагаю на сегодня закончить обсуждение. Если честно я уже просто физически устал — всю ночь фиксил баги :)
Обещаю завтра сделать новый топик (этот уже тяжелый), в котором мы разберем на примере этой формулы (она же исходная, да? :) все алгоритмы, включая унификацию и build HSS.
я предлагаю на сегодня закончить обсуждение. Если честно я уже просто физически устал — всю ночь фиксил баги :)
Обещаю завтра сделать новый топик (этот уже тяжелый), в котором мы разберем на примере этой формулы (она же исходная, да? :) все алгоритмы, включая унификацию и build HSS.
Да, спасибо. Мне тоже уже не очень удобно писать в маленьком квадратике. :)
Спасибо. Пока еще подумаю, если за сегодня/завтра ошибок не найду — попрошу посмотреть Александра Шеня.
Я тоже решил, что если сам ошибок не найду, пойду тормошить сотрудников лаборатории мат. логики ПОМИ.
Впрочем, сдаётся мне, они и так тут незримо присутствуют и наблюдают. :)
Впрочем, сдаётся мне, они и так тут незримо присутствуют и наблюдают. :)
Не факт. www.win.tue.nl/~gwoegi/P-versus-NP.htm — список из 67 (на настоящий момент) решений P = NP. Данное решение там 65е.
Продолжение здесь: habrahabr.ru/blogs/computer_science/112337/
Раскрывать скобки тут не надо:)
not(a^b^c) = (a | b | !c) & (a | !b | c) & (!a | b | c) & (!a | !b | !c)
not(a^b^c) = (a | b | !c) & (a | !b | c) & (!a | b | c) & (!a | !b | !c)
Да, таблички, которые я перечислил — это структуры, а не формулы. То есть перечисления допустимых наборов битов.
Я запутался :) То есть эти 6 структур — это CTS?
Да-да, прошу прощения, я вероятно неправильно написал. Это те CTS, которые фигурируют в последнем шаге алгоритма (раздел 5).
Мда… Математик из меня еще тот)
«Попробую ответить на два вопроса: 1<...> 2<...> 3<...>»
«Попробую ответить на два вопроса: 1<...> 2<...> 3<...>»
FYI: Вот тут развернулась небольшая дискуссия news.ycombinator.com/item?id=2121727
Полиномиальное решение для 3-SAT? Вы серьёзно?!
Глазам своим не верю! Если алгоритм действительно работает так, как заявлено, то вы перевернёте мир. 3-выполнимость — NP-полная задача, к которой сводятся все остальные задачи из класса NP. А это означает, что решится фундаментальнейшая проблема всей математики P? NP. Решится как P=NP. Криптографы, плачьте! Отныне любой шифр может быть сломан. Не помню, входит ли эта проблема в десятку величайших математических проблем современности, за решение которых дают миллион $. Должна входить.
В общем, с алгоритмом надо разобраться. Но, честно говоря, я в чудеса не верю.
Глазам своим не верю! Если алгоритм действительно работает так, как заявлено, то вы перевернёте мир. 3-выполнимость — NP-полная задача, к которой сводятся все остальные задачи из класса NP. А это означает, что решится фундаментальнейшая проблема всей математики P? NP. Решится как P=NP. Криптографы, плачьте! Отныне любой шифр может быть сломан. Не помню, входит ли эта проблема в десятку величайших математических проблем современности, за решение которых дают миллион $. Должна входить.
В общем, с алгоритмом надо разобраться. Но, честно говоря, я в чудеса не верю.
Входит.
Вы путаете теоретическую криптографию и практическую. В теоретической при P=NP теряется стойкость многих шифров, потому что там она оценивается относительно некоторого n. В практической криптографии n=const и ни о какой вычислительной стойкости в том понимании вообще речи не идёт. И здесь вполне может получиться так, что для некоторого n алгоритм со сложностью O(e^n) будет быстрее, чем O(n^8).
Ну я поставил решаться КНФ с 1258 переменными и 16648 скобками. Подожду недельку…
Увы, она уже выдала UNSAT. А формула точно SATisfiable.
Памяти не хватит скорее всего.
Ну вот вам пример выполнимой КНФ формулы, которую cryptominisat порвал за минуту, а ваша софтина (неоптимизированная) обьявила нерешаемой
narod.ru/disk/3936570001/11f5d019850183f02432a41a4551317c.7z.html
Решение, логи, все там есть.
narod.ru/disk/3936570001/11f5d019850183f02432a41a4551317c.7z.html
Решение, логи, все там есть.
Можете приложить лог нашей программы?
Она выдала сообщение: «One of the structures was built empty» или какое-то другое?
Она успела создать выходной файл с результатом?
Я попробовал запустить решение этой формулы на своем ноутбуке, в результате после преобразования в 3-SAT получилась формула:
VarCount: 131411; ClausesCount: 195216; TiersCount: 183716
Я даже недождался, когда она построит CTS. Это очень большая формула для этой реализации… и для ресурсов моего ноутбука. Для интереса, можете привести характеристики машины, на которой вы запускали задачу?
Она выдала сообщение: «One of the structures was built empty» или какое-то другое?
Она успела создать выходной файл с результатом?
Я попробовал запустить решение этой формулы на своем ноутбуке, в результате после преобразования в 3-SAT получилась формула:
VarCount: 131411; ClausesCount: 195216; TiersCount: 183716
Я даже недождался, когда она построит CTS. Это очень большая формула для этой реализации… и для ресурсов моего ноутбука. Для интереса, можете привести характеристики машины, на которой вы запускали задачу?
Пока писал пост программа выбросила ошибку:
18:40:31,019|22173 INFO [StopWatch] — Create CTF: 21233ms; overall: 22019ms
18:40:31,020|22174 INFO [Program] — CTF count: 58
18:48:03,983|475137 INFO [Helper] — **********************************************************************
18:48:03,983|475137 INFO [StopWatch] — Create CTS…
18:48:15,677|486831 INFO [StopWatch] — Create CTS: 11694ms; overall: 33713ms
18:48:15,706|486860 INFO [Program] — One of the structures was built empty
com.anjlab.sat3.EmptyStructureException
at com.anjlab.sat3.SimpleFormula.complete(SimpleFormula.java:224)
at com.anjlab.sat3.Helper.completeToCTS(Helper.java:762)
at com.anjlab.sat3.Program.main(Program.java:184)
18:48:15,708|486862 INFO [Helper] — **********************************************************************
18:48:15,708|486862 INFO [StopWatch] — Saving current statictics of calculations to ./examples/cnf.cnf-results.txt…
18:48:15,724|486878 INFO [StopWatch] — Saving current statictics of calculations to ./examples/cnf.cnf-results.txt: 16ms; overall: 33729ms
Это может быть из-за «плохих» данных, но я проверю еще раз.
18:40:31,020|22174 INFO [Program] — CTF count: 58
18:48:03,983|475137 INFO [Helper] — **********************************************************************
18:48:03,983|475137 INFO [StopWatch] — Create CTS…
18:48:15,677|486831 INFO [StopWatch] — Create CTS: 11694ms; overall: 33713ms
18:48:15,706|486860 INFO [Program] — One of the structures was built empty
com.anjlab.sat3.EmptyStructureException
at com.anjlab.sat3.SimpleFormula.complete(SimpleFormula.java:224)
at com.anjlab.sat3.Helper.completeToCTS(Helper.java:762)
at com.anjlab.sat3.Program.main(Program.java:184)
18:48:15,708|486862 INFO [Helper] — **********************************************************************
18:48:15,708|486862 INFO [StopWatch] — Saving current statictics of calculations to ./examples/cnf.cnf-results.txt…
18:48:15,724|486878 INFO [StopWatch] — Saving current statictics of calculations to ./examples/cnf.cnf-results.txt: 16ms; overall: 33729ms
Это может быть из-за «плохих» данных, но я проверю еще раз.
Ошибка была связана с OutOfMemoryError, которая маскировалась вот этим исключением: EmptyStructureException.
Собрали билд с исправлениями: github.com/downloads/anjlab/sat3/3-sat-experiment-2.0.0-PRE-bin.zip
Собрали билд с исправлениями: github.com/downloads/anjlab/sat3/3-sat-experiment-2.0.0-PRE-bin.zip
Машина 4GB, WinXP 32bit.
Могу помучить сейчас на Win7 с 6GB.
Мне только лень тыкаться и получать отлупы и эксепшны.
(пока я запускал на тех КНФ, на которых сryptominisat получал решение за секунду).
Могу помучить сейчас на Win7 с 6GB.
Мне только лень тыкаться и получать отлупы и эксепшны.
(пока я запускал на тех КНФ, на которых сryptominisat получал решение за секунду).
:) 6 ГБ не хватит точно для больших задач. 300-400 переменных — потянет.
Но я понял на чем у вас споткнулась реализация, так что спасибо!
Но я понял на чем у вас споткнулась реализация, так что спасибо!
300-400 переменных можно DPLL-лем на питоне брутфорсить не приходя в сознание, не интересно.
Какой у вас полином на потребление памяти?
Теоретически такой:
- Размер одной CTS: V(CTS) = 3*8*(n-2) // 3 переменные в ярусе, 8 строк в каждом ярусе, n-2 яруса всего
- Размер гиперструктуры HS: V(HS) = m_(CTS_1) * V(CTS_r) // m_(CTS_1) — это количество строк в CTS_1 (1 — потому что это базовая структура), V(CTS_r) — размер второй CTS в гиперструктуре — определено выше;
максимум m(CTS_r) = 8*(n-2) // 8 строк в n-2 ярусах
Размер системы гиперструктур HSS: V(HSS) = (k — 1)*V(HS) // k — количество CTS
То есть размер V(HSS) можно оценить так: V(HSS)=(k-1) * (8*(n-2)) * (3*8*(n-2)) = 192 * (k-1) * (n-2)^2 (откроется в WolframAlpha)
Число k зависит от структуры формулы… для формул размером n=100-300 => k=10-20, для n=1000 может быть 30-40. Здесь даже не столько влияет число n, сколько структура связей в формуле.
Но это в теории. На практике присутствуют накладные расходы на объекты и указатели. В текущей реализации память не оптимизировалась.
Вот маленькая КНФ,
narod.ru/disk/3937171001/62aedfdfef414e38dbe16145291424a1.7z.html
на которой у вас выпал
Exception in thread «main» java.lang.IllegalStateException: Tiers should be sorted
at com.anjlab.sat3.SimpleFormula.assertTiersSorted(SimpleFormula.java:488)
at com.anjlab.sat3.SimpleFormula.complete(SimpleFormula.java:208)
at com.anjlab.sat3.Helper.completeToCTS(Helper.java:783)
at com.anjlab.sat3.Program.main(Program.java:184)
narod.ru/disk/3937171001/62aedfdfef414e38dbe16145291424a1.7z.html
на которой у вас выпал
Exception in thread «main» java.lang.IllegalStateException: Tiers should be sorted
at com.anjlab.sat3.SimpleFormula.assertTiersSorted(SimpleFormula.java:488)
at com.anjlab.sat3.SimpleFormula.complete(SimpleFormula.java:208)
at com.anjlab.sat3.Helper.completeToCTS(Helper.java:783)
at com.anjlab.sat3.Program.main(Program.java:184)
Ошибка «Tiers should be sorted» — это результат внутренней проверки на правильность введенных данных.
Фактически это скорее всего вызвано тем, что нумерация переменных формуле (1..n) не совпадает с нумерацией 1, 2,… n. Например, вы могли ввести формулу с 5 переменными, но в ней переменные имеют имена 11, 12, 13, 20, 21 в место того, чтобы быть 1, 2, 3, 4, 5.
Я заметил, что многие задачи из sat competition оформлены подобным образом. По хорошему, конечно, при вводе данных нужно сделать преобразование по приведению имен переменных в нужный порядок, или хотя бы внятное сообщение об ошибке… Я думаю это будет одна из следующих фич, которые я реализую.
Ошибка «Can't get value of varName=4 because varName is not from the form» из сообщения ниже, скорее всего является следствием этого же. Просто несколько проверок самоконтроля приложение прошло успешно, а дальше свалилось. Это должно быть исправлено предыдущим фиксом.
Фактически это скорее всего вызвано тем, что нумерация переменных формуле (1..n) не совпадает с нумерацией 1, 2,… n. Например, вы могли ввести формулу с 5 переменными, но в ней переменные имеют имена 11, 12, 13, 20, 21 в место того, чтобы быть 1, 2, 3, 4, 5.
Я заметил, что многие задачи из sat competition оформлены подобным образом. По хорошему, конечно, при вводе данных нужно сделать преобразование по приведению имен переменных в нужный порядок, или хотя бы внятное сообщение об ошибке… Я думаю это будет одна из следующих фич, которые я реализую.
Ошибка «Can't get value of varName=4 because varName is not from the form» из сообщения ниже, скорее всего является следствием этого же. Просто несколько проверок самоконтроля приложение прошло успешно, а дальше свалилось. Это должно быть исправлено предыдущим фиксом.
Это DIMACS формат.
Все решатели его понимают, никто еще не жаловался.
Нумерация переменных — это личное дело того, кто кодирует КНФ (нумерация может нести семантику).
Когда исправите — могу еще погонять.
Все решатели его понимают, никто еще не жаловался.
Нумерация переменных — это личное дело того, кто кодирует КНФ (нумерация может нести семантику).
Когда исправите — могу еще погонять.
Согласен про семантику. Напишу здесь, когда реализую это исправление.
Поправили чтение таких файликов.
Собрали билд с исправлениями: github.com/downloads/anjlab/sat3/3-sat-experiment-2.0.0-PRE-bin.zip
Собрали билд с исправлениями: github.com/downloads/anjlab/sat3/3-sat-experiment-2.0.0-PRE-bin.zip
Еще одна микроформула
narod.ru/disk/3937596001/a5da0d18696f4902149f1c2c6cbf6109.7z.html
на которой у вас
Program completed
Exception in thread «main» java.lang.IllegalArgumentException: Can't get value of varName=4 because varName is not from the form
ula's permutation
at com.anjlab.sat3.SimpleFormula.valueOf(SimpleFormula.java:737)
at com.anjlab.sat3.Helper.unify(Helper.java:537)
at com.anjlab.sat3.Helper.unify(Helper.java:445)
at com.anjlab.sat3.Program.main(Program.java:203)
Все, играть кончаю, пора на работу.
А вас советую потестировать серьезней, перед публикацией статей (не читал) и кода (не смотрел).
narod.ru/disk/3937596001/a5da0d18696f4902149f1c2c6cbf6109.7z.html
на которой у вас
Program completed
Exception in thread «main» java.lang.IllegalArgumentException: Can't get value of varName=4 because varName is not from the form
ula's permutation
at com.anjlab.sat3.SimpleFormula.valueOf(SimpleFormula.java:737)
at com.anjlab.sat3.Helper.unify(Helper.java:537)
at com.anjlab.sat3.Helper.unify(Helper.java:445)
at com.anjlab.sat3.Program.main(Program.java:203)
Все, играть кончаю, пора на работу.
А вас советую потестировать серьезней, перед публикацией статей (не читал) и кода (не смотрел).
Я ответил на ошибку в комментарии выше: habrahabr.ru/blogs/computer_science/112161/#comment_3590126
Согласен, защиту от неверных данных нужно было сделать впервую очередь. Это получилось даже не потому, что формат DIMACS все понимают по разному (кто-то может в одном файле закодировать сразу несколько формул, кто-то в одну скобку может поместить переменную с одним именем два раза), а в том, что большинство формул, на которых проводились тесты (http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html), были оформлены «правильно».
Будем постепенно адаптироваться.
Согласен, защиту от неверных данных нужно было сделать впервую очередь. Это получилось даже не потому, что формат DIMACS все понимают по разному (кто-то может в одном файле закодировать сразу несколько формул, кто-то в одну скобку может поместить переменную с одним именем два раза), а в том, что большинство формул, на которых проводились тесты (http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html), были оформлены «правильно».
Будем постепенно адаптироваться.
Спасибо за интерес и потраченное время!
НЛО прилетело и опубликовало эту надпись здесь
Вопрос
Русская версия, страница 14, 3й абзац.
Что такое «t-пересечение со значением x_{t+3} = b»?
Русская версия, страница 14, 3й абзац.
Что такое «t-пересечение со значением x_{t+3} = b»?
Пусть первые три яруса гиперструктуры выглядят так:
Тогда \pi_3(0) и \pi_3(1) не есть 3-пересечения.
000 000 001 | 000 000 001 | 000 000 001
Тогда \pi_3(0) и \pi_3(1) не есть 3-пересечения.
Это значит пересечение с первого уровня до уровня t, причем значение переменной x_{t+3} в этой подструктуре равно b.
Пересечение подструктуры из некой вершины уровня один, подструктуры из некой вершины уровня два, ..., подструктуры из некой вершины уровня t. Так?
В какой — «этой»?
В какой — «этой»?
j-пересечение вводится на странице 10 в третьем абзаце:
вместо j в термине «j-пересечение» можно поставить любую букву или цифру, например, 5-пересечение, или t-пересечение. Эта цифра влияет только на диапазон 1, 2,..., j (1 ≤ j < n−3). Значение из этого диапазона обозначает уровень (tier) в графе. То есть мы получаем подструктуры с каждого уровня и их объединяем — получаем j-пересечение. Там же говорится, что по-построению j-пересечение будет непустым, только если между вершинами на соседних ярусах есть ребро.
A substructure that is formed by means of intersection of j substructures located respectively at the tiers 1, 2,..., j (1 ≤ j < n−3), is said to be a j-intersection of substructures in HS.
вместо j в термине «j-пересечение» можно поставить любую букву или цифру, например, 5-пересечение, или t-пересечение. Эта цифра влияет только на диапазон 1, 2,..., j (1 ≤ j < n−3). Значение из этого диапазона обозначает уровень (tier) в графе. То есть мы получаем подструктуры с каждого уровня и их объединяем — получаем j-пересечение. Там же говорится, что по-построению j-пересечение будет непустым, только если между вершинами на соседних ярусах есть ребро.
Так, j-пересечение — это пересечение специальным образом выбранных j структур.
Да, с каждого уровня от 1 до j берется одна любая вершина.
Что такое «j-пересечение со значением x_{j+3} = b»?
Это значит, что результат j-пересечения конкретизирован: (x_{j+3} -> b)
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Открытое письмо ученым и эталонная реализация алгоритма Романова для NP-полной задачи 3-ВЫП