Comments 24
По вашей ссылке — «Gist has been deleted»
Если я правильно понимаю, на строках 857-932 выведена базисная структура.
Изначально в качестве базисной структуры предлагалась последняя из СКТ (строки 547-626).
Изначально в качестве базисной структуры предлагалась последняя из СКТ (строки 547-626).
Да, базисная структура там другая получилась.
Алгоритм выбирает базисную структуру по простому правилу — где меньше строк.
Если это принципиально (это сказывается только на потреблении памяти).
Я могу переписать тест, чтобы можно было явно базисную структуру задавать.
Как решим?
Алгоритм выбирает базисную структуру по простому правилу — где меньше строк.
Если это принципиально (это сказывается только на потреблении памяти).
Я могу переписать тест, чтобы можно было явно базисную структуру задавать.
Как решим?
Просто результаты получаются большими, так их наверное проще будет анализировать.
Кстати, можно ли отказаться от процедуры унификации для троек переменных вообще, и для пар переменных кроме x1 и x2 в первой и четвертой структурах, а также x3 и x4 во второй и пятой? Поскольку остальные пары переменных вместе в ограничениях встречаются не более одного раза, то добавлением достаточного числа фиктивных переменных можно добиться того, что никакие другие пары переменных не будут оказываться рядом более одного раза.
Кстати, можно ли отказаться от процедуры унификации для троек переменных вообще, и для пар переменных кроме x1 и x2 в первой и четвертой структурах, а также x3 и x4 во второй и пятой? Поскольку остальные пары переменных вместе в ограничениях встречаются не более одного раза, то добавлением достаточного числа фиктивных переменных можно добиться того, что никакие другие пары переменных не будут оказываться рядом более одного раза.
«проще анализировать» — потому что базисная структура не будет оказывать никакого влияния на происходящее, вопрос будет исключительно в согласовании.
Не уверен, что понял вопрос про унификацию.
Унификация не имеет дело с тройками — только с парами переменных и с переменными, которые тождественно 1 или 0.
Если переменные x1 и x2 встречаются в пределах одной тройки в двух и более структурах — значит при унификации нужно учитывать эту пару.
Не понял про фиктивные переменные, зачем их добавлять? В любом случае, если вы добавляете «фиктивные» переменные, то они также участвуют в процедурах очищения и унификации.
Унификация не имеет дело с тройками — только с парами переменных и с переменными, которые тождественно 1 или 0.
Если переменные x1 и x2 встречаются в пределах одной тройки в двух и более структурах — значит при унификации нужно учитывать эту пару.
Не понял про фиктивные переменные, зачем их добавлять? В любом случае, если вы добавляете «фиктивные» переменные, то они также участвуют в процедурах очищения и унификации.
Фиктивная переменная — это переменная, не стоящая ни в одной скобке.
Если две переменных в одной скобке вместе стоят только в одной скобке, то, за счет подходящей нумерации переменных при достаточно большом количестве фиктивных, можно добиться, чтобы они стояли рядом только в одной из СКТ.
Фиктивные переменные на процедуры очищения и унификации существенного влияния не оказывают, так как все структуры выдерживают замену нулей фиктивной переменной единицами, а единиц — нулями.
Тем самым для данного примера можно в процедуре унификации исключить унификацию по тройкам, а парную унификацию проводить только по парам (x1, x2) и (x3, x4).
Если две переменных в одной скобке вместе стоят только в одной скобке, то, за счет подходящей нумерации переменных при достаточно большом количестве фиктивных, можно добиться, чтобы они стояли рядом только в одной из СКТ.
Фиктивные переменные на процедуры очищения и унификации существенного влияния не оказывают, так как все структуры выдерживают замену нулей фиктивной переменной единицами, а единиц — нулями.
Тем самым для данного примера можно в процедуре унификации исключить унификацию по тройкам, а парную унификацию проводить только по парам (x1, x2) и (x3, x4).
Я вижу вы здесь знаете больше меня. :)
Простите, не очень понял.
С каким-то из утверждений Вы несогласны? Тогда я попробую его расписать и доказать (просто это выглядит чисто технической работой).
Для простоты явно выпишу основные пункты:
1. При достаточно большом числе фиктивных переменных можно добиться того, что пара переменных стоит рядом в двух разных СКТ только в том случае, если эта пара переменных входит в две различные скобки (в том числе, каждая пара фиктивных переменных, а также каждая пара фиктивная+существенная переменная стоят рядом не более чем в одной скобке).
2. Если структуры из обсуждаемого примера преобразованы путем добавления/перестановки переменных, указанной в предыдущем пункте, то:
2а. Процедура унификации по тройкам в алгоритме не будет использована ни разу.
2б. Процедура унификации по парам будет использована только для пар (x1, x2) и (x3, x4) для СКТ (1,4) и (2, 5) соответственно.
С каким-то из утверждений Вы несогласны? Тогда я попробую его расписать и доказать (просто это выглядит чисто технической работой).
Для простоты явно выпишу основные пункты:
1. При достаточно большом числе фиктивных переменных можно добиться того, что пара переменных стоит рядом в двух разных СКТ только в том случае, если эта пара переменных входит в две различные скобки (в том числе, каждая пара фиктивных переменных, а также каждая пара фиктивная+существенная переменная стоят рядом не более чем в одной скобке).
2. Если структуры из обсуждаемого примера преобразованы путем добавления/перестановки переменных, указанной в предыдущем пункте, то:
2а. Процедура унификации по тройкам в алгоритме не будет использована ни разу.
2б. Процедура унификации по парам будет использована только для пар (x1, x2) и (x3, x4) для СКТ (1,4) и (2, 5) соответственно.
С каким-то из утверждений Вы несогласны?
Нет, наверное все так. Я просто не понимаю к чему это… :\
Просто мне кажется, что чем меньше всего будет делать алгоритм, тем проще будет проверять.
В данном случае — унификацию можно сильно ограничить.
В данном случае — унификацию можно сильно ограничить.
Очень может быть. Вообще, Романов сам постоянно говорит, что наверняка все можно сделать проще, найти какие-то свойства структур и алгоритмов, которые позволят сделать его эффективнее. Но для доказательства уже достаточно того, что есть сейчас. В статье про унификацию вообще приводятся только основные правила, суть которых показать какой должен быть результат. Как это будет реализовано — другой вопрос. Только я переписывал процедуру унификации несколько раз. Правда со стороны, которую предлагаете вы, я на эту проблему не смотрел. Интересно.
Если базисная структура — та где меньше строк, можно последнюю формулу с (x10 | x11 | x12) поменять на (x10 & x11 & x12), так чтобы там была ровно одна строка.
У меня есть ощущение, что вы в качестве базовой структуры взяли нетривиальную, ту которая x1 + x2 = x6. А я бы хотел посмотреть на это дело с (x10 | x11 | x12) в качестве базовой структуры.
А чем вы программу собираете? В основном git-репозитории ведь этого юнит-теста нету ещё? Я бы хотел сам собрать, чтобы подабавлять отладочного вывода.
А чем вы программу собираете? В основном git-репозитории ведь этого юнит-теста нету ещё? Я бы хотел сам собрать, чтобы подабавлять отладочного вывода.
Я переделал тест, теперь там явно указывается базисная структура, та которая (x10 | x11 | x12). Обновил лог и тест по ссылке.
Тест был у меня в рабочей копии, сейчас я его закомитил: github.com/anjlab/sat3/commit/27e75ae4527f15ae0d6e3dedb98dccc948f1cc74
Программа собирается maven3 (но я думаю можно и maven2), я запускаю тест из eclipse.
Чтобы загрузить проект в эклипс делаете checkout, потом в этой папке запускаете (maven2/3 должен быть в переменной PATH):
Все тесты должны пройти. После этого можно загрузить проект в IDE, чтобы загрузить в eclipse я делаю так:
1)
2) В eclipse делаю File -> Import -> Existing projects into workspace… -> Выбираю оба проекта 3-sat-core и 3-sat-experiment
3) Дальше нужно будет добавить переменную билда M2_REPO. Для этого на проекте нужно щелкнуть правой кнопкой -> Properties -> Java Build Path -> На вкладке Libraries нажать кнопку Add Variable… -> Configure Variables… -> New… -> В качестве имени M2_REPO, значение — путь к папке с репозиторем maven2, по умолчанию он в <user-dir>/m2/repository (например, c:\Users\dmitrygusev\.m2\repository) -> Дальше везде Ok
Тест был у меня в рабочей копии, сейчас я его закомитил: github.com/anjlab/sat3/commit/27e75ae4527f15ae0d6e3dedb98dccc948f1cc74
Программа собирается maven3 (но я думаю можно и maven2), я запускаю тест из eclipse.
Чтобы загрузить проект в эклипс делаете checkout, потом в этой папке запускаете (maven2/3 должен быть в переменной PATH):
mvn clean test
Все тесты должны пройти. После этого можно загрузить проект в IDE, чтобы загрузить в eclipse я делаю так:
1)
mvn eclipse:eclipse
2) В eclipse делаю File -> Import -> Existing projects into workspace… -> Выбираю оба проекта 3-sat-core и 3-sat-experiment
3) Дальше нужно будет добавить переменную билда M2_REPO. Для этого на проекте нужно щелкнуть правой кнопкой -> Properties -> Java Build Path -> На вкладке Libraries нажать кнопку Add Variable… -> Configure Variables… -> New… -> В качестве имени M2_REPO, значение — путь к папке с репозиторем maven2, по умолчанию он в <user-dir>/m2/repository (например, c:\Users\dmitrygusev\.m2\repository) -> Дальше везде Ok
Дмитрий, может стоит собрать некоторый минимальный набор тестовых файлов в одном месте?
Входной формат известен, для каждого файла заготовить эталонный вывод: разрешима ли задачи и само решение (+ остальная информация в комментариях).
Для начала хватит 6 файлов: простой набор который легко проверить руками, средний набор который включает граничные условия, большой набор для проверки скорости. В каждом наборе по одной разрешимой и неразрешимой задаче.
P.S. сейчас разбираюсь в алгоритме, попробую реализовать его на C#
Входной формат известен, для каждого файла заготовить эталонный вывод: разрешима ли задачи и само решение (+ остальная информация в комментариях).
Для начала хватит 6 файлов: простой набор который легко проверить руками, средний набор который включает граничные условия, большой набор для проверки скорости. В каждом наборе по одной разрешимой и неразрешимой задаче.
P.S. сейчас разбираюсь в алгоритме, попробую реализовать его на C#
Минимальный набор сложно подобрать, наверное. Но какие-то тесты уже есть в проекте: github.com/anjlab/sat3/tree/master/3-sat-core/src/test/resources
Конечно, там есть и большие формулы — они использовались в основном в начале разработки для тестирования алгоритма декомпозиции формулы. Но есть экземпляры и поменьше, например, article-example.cnf — это формула из статьи, cnf-v112-c418-100-sat.cnf — формула, которая нашим алгоритмом декомпозируется на 2 ФКТ, так что получается одна гиперструктура, и т.д. Большинство формул для тестов были взяты отсюда: www.cs.ubc.ca/~hoos/SATLIB/benchm.html
Я не запускал регрессионные тесты на всех формулах, потому что есть набор unit-тестов, которые тестируют разные алгоритмы по-отдельности.
Насчет решения — их обычно быть много, можно конечно привести одно, но зачем? Если вы получите свое — можете легко его проверить, подставив значения в формулу.
Конечно, там есть и большие формулы — они использовались в основном в начале разработки для тестирования алгоритма декомпозиции формулы. Но есть экземпляры и поменьше, например, article-example.cnf — это формула из статьи, cnf-v112-c418-100-sat.cnf — формула, которая нашим алгоритмом декомпозируется на 2 ФКТ, так что получается одна гиперструктура, и т.д. Большинство формул для тестов были взяты отсюда: www.cs.ubc.ca/~hoos/SATLIB/benchm.html
Я не запускал регрессионные тесты на всех формулах, потому что есть набор unit-тестов, которые тестируют разные алгоритмы по-отдельности.
Насчет решения — их обычно быть много, можно конечно привести одно, но зачем? Если вы получите свое — можете легко его проверить, подставив значения в формулу.
Я тут пока играю с солвером на примерах разной сложности. Пока он считает (кстати, долговато что-то, 5+ часов на 250 переменных), задам вопрос по доказательству.
Где в доказательстве теоремы 2 используется 2-й пункт унификации? В котором мы проверяем какие значения могут быть у пары битов. И почему нам хватает только проверок пар битов, и не нужно проверять, скажем, значения троек битов?
Где в доказательстве теоремы 2 используется 2-й пункт унификации? В котором мы проверяем какие значения могут быть у пары битов. И почему нам хватает только проверок пар битов, и не нужно проверять, скажем, значения троек битов?
Насчет скорости: помимо n и m на время работы алгоритма влияет еще структура формулы. Некоторые формулы можно декомпозировать на 2 ФКТ, другие — на 10, третьи — на сотни. Время работы алгоритма будет также зависеть от числа k — количества ФКТ. Это число неявно присутствует в оценке сложности в качестве m: O(m * n^4). Соответственно, чем больше k, чем больше в базисной СКТ строк — тем дольше будет работать алгоритм.
Еще один момент: в приложении реализованы два алгоритма, которые запускаются последовательно. Первый — построение системы гиперструктур. Если результатом его работы является напустая HSS, то формула считается выполнимой по теореме 1.
Второй алгоритм — поиск выполняющего набора в HSS. Вообще говоря в статье этот алгоритм не рассматривается. Сейчас в реализации он работает так: в HSS последовательно из каждого уровня базисного графа отбрасываются все вершины кроме одной начиная с первого уровня и так далее вниз. Оставляется только одна вершина (любая), подструктура которой имеет непустое пересечение с любой подструктурой вершины последнего уровня. Строится новая система гиперструктур. Дальше со второго уровня выбрасываются все вершины, кроме смежных с вершиной первого уровня. Их максимум две. Какую оставить решает такое правило: оставляем первую вершину и строим систему HSS, если она построена — значит мы выбрали правильную вершину, если нет — значит оставляем вторую вершину. И так далее, пока HSS не станет элементарной, то есть будет содержать только одно j-пересечение.
К чему я это, к тому, что при запуске алгоритма HSS может строиться несколько раз — что приводит к еще более длительному времени работы программы. Почему может — потому что сейчас не обязательно HSS сводить к элементарной для поиска выполняющего набора, так как там есть вспомогательный алгоритм (quickFindHSSRoute), который умеет находить выполняющий набор в системе гиперструктур. Не буду вдаваться в подробности этого алгоритма, можно считать сейчас, что это эвристика.
Насчет второго вопроса, я уточню у Владимира Федоровича. Но вроде бы так:
Еще один момент: в приложении реализованы два алгоритма, которые запускаются последовательно. Первый — построение системы гиперструктур. Если результатом его работы является напустая HSS, то формула считается выполнимой по теореме 1.
Второй алгоритм — поиск выполняющего набора в HSS. Вообще говоря в статье этот алгоритм не рассматривается. Сейчас в реализации он работает так: в HSS последовательно из каждого уровня базисного графа отбрасываются все вершины кроме одной начиная с первого уровня и так далее вниз. Оставляется только одна вершина (любая), подструктура которой имеет непустое пересечение с любой подструктурой вершины последнего уровня. Строится новая система гиперструктур. Дальше со второго уровня выбрасываются все вершины, кроме смежных с вершиной первого уровня. Их максимум две. Какую оставить решает такое правило: оставляем первую вершину и строим систему HSS, если она построена — значит мы выбрали правильную вершину, если нет — значит оставляем вторую вершину. И так далее, пока HSS не станет элементарной, то есть будет содержать только одно j-пересечение.
К чему я это, к тому, что при запуске алгоритма HSS может строиться несколько раз — что приводит к еще более длительному времени работы программы. Почему может — потому что сейчас не обязательно HSS сводить к элементарной для поиска выполняющего набора, так как там есть вспомогательный алгоритм (quickFindHSSRoute), который умеет находить выполняющий набор в системе гиперструктур. Не буду вдаваться в подробности этого алгоритма, можно считать сейчас, что это эвристика.
Насчет второго вопроса, я уточню у Владимира Федоровича. Но вроде бы так:
- второе доказательство строится на одноименных j-пересечениях; унификация, как она определена, должна приводить к тому, чтобы в двух CTS убирались строки, которые не образуют совместного выполняющего набора.
В алгоритме SEP пункт A concordance rules на стр. 15 говорит о том, что все одноименные подструктуры должны быть унифицированы в ходе построения HSS. Это приводит к тому, что все одноименные j-пересечения будут в себе заключать все совместные выполняющие наборы.
- тройки битов не проверяются, потому что подразумевается, что три переменных в одной тройке могут быть только в одной СКТ.
Я переговорил с Владимиром Федоровичем. По первому вопросу все так: если две переменные будут иметь разные значения — это приведет к противоречию и совместного выполняющего набора для них быть не может по построению. По второму — тройки переменных отдельно не нужно проверять, потому что такая проверка покрываются проверкой пар значений переменных. Если в двух тройках любая пара совпадает, значит и тройки тоже совпадают.
> По первому вопросу все так: если две переменные будут иметь разные значения — это приведет к противоречию и совместного выполняющего набора для них быть не может по построению.
Это доказательство того, что если выполняющий набор есть, то такая проверка ничего не испортит. Меня интересует, где тот факт что мы проверяем пары переменных, используется в доказательстве в другую сторону. Проверка пар — это ключевая часть унификации, тот факт что мы её делаем должен явно использоваться в доказательстве. Вопрос: где?
(Вполне возможно, что я не заметил это место, так что заранее извиняюсь.)
Это доказательство того, что если выполняющий набор есть, то такая проверка ничего не испортит. Меня интересует, где тот факт что мы проверяем пары переменных, используется в доказательстве в другую сторону. Проверка пар — это ключевая часть унификации, тот факт что мы её делаем должен явно использоваться в доказательстве. Вопрос: где?
(Вполне возможно, что я не заметил это место, так что заранее извиняюсь.)
Чем закончилось?
Sign up to leave a comment.
Обсуждение работы алгоритма Романова на примере