Не понимаю что вы имеете ввиду, когда говорите, что каждая структура consistent. Такого определения структур в статье нет. Что вы имеете ввиду?
Фильтрация и унификация — никак не связаны. Это совершенно разные операции.
но так как все рёбра у нас будут присутствовать
Такого не может быть по правилу построения CTS. CTS — это дополнение CTF. То что вы говорите может получиться, только если в CTF у нас нет ниодной скобки.
Унификация никак не связана с гиперструктурой. Унификация — это q-арная операция CTS с разными перестановками переменных (то есть несогласованных). Кстати, единственно-возможная операция для таких несогласованных структур.
Еще одно уточнение про первую структуру. Вы говорите что она соответствует тождественной истине. Это значит что в ней на всех ярусах по 8 строк? Если да, то такая формула не может быть выполнимой. Когда вы будете строить CTS — то есть дополнение к CTF — получите пустую структуру.
Или я опять неправильно понял?
Размер одной 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, сколько структура связей в формуле.
Но это в теории. На практике присутствуют накладные расходы на объекты и указатели. В текущей реализации память не оптимизировалась.
Я не совсем понял постановку вопроса. Точнее эти структуры. Это одна формула разложенная на несколько CTF?
Чтобы убедиться, что мы говорим об одном и том же.
1) Процедура унификации — независимая операция, которая применяется не к CTF, а к CTS. У каждой CTS должен быть одинаковый набор переменных, но при этом разные перестановки.
2) Процедура фильтрации применяется для какой-либо подструктуры-вершины, которая находится в частично построенной гиперструктуре. И запускается входе алгоритма продвижения этой вершины по ребру на один уровень вниз.
j-пересечение вводится на странице 10 в третьем абзаце:
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-пересечение.
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
Это может быть из-за «плохих» данных, но я проверю еще раз.
Согласен, защиту от неверных данных нужно было сделать впервую очередь. Это получилось даже не потому, что формат DIMACS все понимают по разному (кто-то может в одном файле закодировать сразу несколько формул, кто-то в одну скобку может поместить переменную с одним именем два раза), а в том, что большинство формул, на которых проводились тесты (http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html), были оформлены «правильно».
Ошибка «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» из сообщения ниже, скорее всего является следствием этого же. Просто несколько проверок самоконтроля приложение прошло успешно, а дальше свалилось. Это должно быть исправлено предыдущим фиксом.
Она выдала сообщение: «One of the structures was built empty» или какое-то другое?
Она успела создать выходной файл с результатом?
Я попробовал запустить решение этой формулы на своем ноутбуке, в результате после преобразования в 3-SAT получилась формула:
VarCount: 131411; ClausesCount: 195216; TiersCount: 183716
Я даже недождался, когда она построит CTS. Это очень большая формула для этой реализации… и для ресурсов моего ноутбука. Для интереса, можете привести характеристики машины, на которой вы запускали задачу?
Фильтрация и унификация — никак не связаны. Это совершенно разные операции.
Такого не может быть по правилу построения CTS. CTS — это дополнение CTF. То что вы говорите может получиться, только если в CTF у нас нет ниодной скобки.
Унификация никак не связана с гиперструктурой. Унификация — это q-арная операция 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, сколько структура связей в формуле.
Но это в теории. На практике присутствуют накладные расходы на объекты и указатели. В текущей реализации память не оптимизировалась.
Чтобы убедиться, что мы говорим об одном и том же.
1) Процедура унификации — независимая операция, которая применяется не к CTF, а к CTS. У каждой CTS должен быть одинаковый набор переменных, но при этом разные перестановки.
2) Процедура фильтрации применяется для какой-либо подструктуры-вершины, которая находится в частично построенной гиперструктуре. И запускается входе алгоритма продвижения этой вершины по ребру на один уровень вниз.
Да, с каждого уровня от 1 до j берется одна любая вершина.
Это значит, что результат j-пересечения конкретизирован: (x_{j+3} -> b)
вместо j в термине «j-пересечение» можно поставить любую букву или цифру, например, 5-пересечение, или t-пересечение. Эта цифра влияет только на диапазон 1, 2,..., j (1 ≤ j < n−3). Значение из этого диапазона обозначает уровень (tier) в графе. То есть мы получаем подструктуры с каждого уровня и их объединяем — получаем j-пересечение. Там же говорится, что по-построению j-пересечение будет непустым, только если между вершинами на соседних ярусах есть ребро.
Собрали билд с исправлениями: 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
Если полученная (промежуточная) структура пересечется пусто хотя бы с одним уровнем — значит считаем, что продвижение в целевую вершину по данному ребру не удалось.
А если со всеми уровнями пересечение было не пустым, то в целевой вершине мы сохраняем хотя бы одно непустое j-пересечение.
Но я понял на чем у вас споткнулась реализация, так что спасибо!
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
Это может быть из-за «плохих» данных, но я проверю еще раз.
Согласен, защиту от неверных данных нужно было сделать впервую очередь. Это получилось даже не потому, что формат DIMACS все понимают по разному (кто-то может в одном файле закодировать сразу несколько формул, кто-то в одну скобку может поместить переменную с одним именем два раза), а в том, что большинство формул, на которых проводились тесты (http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html), были оформлены «правильно».
Будем постепенно адаптироваться.
Фактически это скорее всего вызвано тем, что нумерация переменных формуле (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» из сообщения ниже, скорее всего является следствием этого же. Просто несколько проверок самоконтроля приложение прошло успешно, а дальше свалилось. Это должно быть исправлено предыдущим фиксом.
Она выдала сообщение: «One of the structures was built empty» или какое-то другое?
Она успела создать выходной файл с результатом?
Я попробовал запустить решение этой формулы на своем ноутбуке, в результате после преобразования в 3-SAT получилась формула:
VarCount: 131411; ClausesCount: 195216; TiersCount: 183716
Я даже недождался, когда она построит CTS. Это очень большая формула для этой реализации… и для ресурсов моего ноутбука. Для интереса, можете привести характеристики машины, на которой вы запускали задачу?