Логическая выполнимость
В статье про разложение на заблокированные ограничения (РЗО) упоминается забавный приём под названием SAT sweeping - переведём его, как "чистку схемы" (ЧС).
Состоит он в присваивании входам схемы случайных значений и прогону значений по схеме (распространение констант). Те переменные ("провода" ), что принимают одинаковые значения, могут быть равными. Те переменные, что всегда принимают значения 0 или 1, могут быть точно равны 0 или 1.
Прогон можно выполнять сразу над многими значениями, представленными массивами битов.
В случае КНФ у нас нет схемы, как таковой. РЗО позволяет восстановить её в каком-то виде, после алгоритма разложения у нас есть пары литерал ← ограничение, и если ограничение не удовлетворено, то надо изменить значение переменной литерала на обратное.
Первое, что необходимо отметить, что РЗО работает с легко разрешимым подмножеством исходной формулы. То есть, не только это подмножество имеет решение, так его ещё и легко найти, за линейное время. Второе - каждое ограничение работает не более одного раза. Поскольку РЗО разделяет ограничения на две части - побольше и поменьше, - и после мы работаем только с одной частью, некоторые ограничения вообще не будут использованы. Третье, и это относится к ЧС в целом, у нас нет выбора направления прохода. В случае ЧС исходной схемы нет сведений об использовании обратного прохода, от выходов ко входам, в случае ЧС частей формулы после РЗО так же нет направления.
(про направление в КНФ говорить бессмысленно, ибо там всё может быть перемешано; но если не перемешано, то почему бы не использовать?)
Что можно сделать.
Первое, это использовать всю формулу. После РЗО использовать все полученные части с вычисленными блокирующими литералами, перемешав их случайно или использовать порядок РЗО. Как ни странно, даже взятие случайного литерала из ограничения и взятие ограничений в случайном порядке работает вполне неплохо.
Второе, это использование всех ограничений, как-то касающихся переменной. Если у нас есть ограничение x1+x2+x3 (xi - литерал переменной vi), то оно должно быть использовано и при вычислении значения v1, и при вычислении значения v2 и при вычислении значения v3.
Третье, мы можем попробовать восстановить или как-то задать направление вычислений. В соображении выше мы можем упорядочивать работу с ограничениями по рассматриваемой переменной, в порядке возрастания или убывания. Мы, также, можем ограничить ограничения, что будут использованы при вычислении значения переменной - содержащими только переменные меньшие или равные вычисляемой, тогда у нас "проход по схеме в направлении выхода," или ограничения должны содержать переменные большие или равные вычисляемой, тогда у нас получится "проход по схеме от выхода ко входу."
Переменные КНФ (схемы вообще) можно разделить на "хребет" и остальные. Переменные "хребта" имеют одно и то же значение при всех удовлетворяющих присваиваниях. Остальные переменные могут принадлежать какому-то классу (не)равенства - где при всех удовлетворяющих присваиваниях они обязательно (не) равны друг другу. Типичная задача разложения на множители для N=PQ, где P и Q простые, содержит довольно много переменных хребта и один класс (не)равенства - переменные, не принадлежащие хребту, в одном из двух решений либо 0, либо 1. Ну, так уж получилось, что класс там один, может быть больше, да ещё и условных (если P или Q составные). В статье выше переменные разделяются по классам равенства, то есть, в любом истинном присваивании они равны между собой. Я считаю, что соединять можно и по равенству, и по неравенству.
Так вот.
Если в результате прогона какая-то переменная получила значение "все 0" или "все 1," то можно (осторожно) считать, что её значение таковым и является. Чем длиннее массив битов, представляющий значение переменной, тем выше вероятность, что так и есть.
Если в результате прогона какие-то две переменных получили значения равные друг другу, ровно с той же осторожностью можно считать их равными. Если значение одной равно дополненному до 2 значению другой, то столь же осторожно можно считать переменные строго неравными друг другу.
Равенства и неравенства можно объединять через классы равенств. v1=v2 и v2=v3 можно перевести в v1=v2 и v1=v3, и тогда упрощение формулы становится проще выполнить.
В завершение скажу, что все алгоритмы выше приводят к некоторому насыщению - из КНФ мы можем извлечь N констант и M (не)равенств, после чего они перестают работать. Тем не менее, некоторое упрощение вполне можно получить, уменьшив количество переменных и ограничений в КНФ раза в полтора, если повезёт.
Состоит он в присваивании входам схемы случайных значений и прогону значений по схеме (распространение констант). Те переменные ("провода" ), что принимают одинаковые значения, могут быть равными. Те переменные, что всегда принимают значения 0 или 1, могут быть точно равны 0 или 1.
Прогон можно выполнять сразу над многими значениями, представленными массивами битов.
В случае КНФ у нас нет схемы, как таковой. РЗО позволяет восстановить её в каком-то виде, после алгоритма разложения у нас есть пары литерал ← ограничение, и если ограничение не удовлетворено, то надо изменить значение переменной литерала на обратное.
Первое, что необходимо отметить, что РЗО работает с легко разрешимым подмножеством исходной формулы. То есть, не только это подмножество имеет решение, так его ещё и легко найти, за линейное время. Второе - каждое ограничение работает не более одного раза. Поскольку РЗО разделяет ограничения на две части - побольше и поменьше, - и после мы работаем только с одной частью, некоторые ограничения вообще не будут использованы. Третье, и это относится к ЧС в целом, у нас нет выбора направления прохода. В случае ЧС исходной схемы нет сведений об использовании обратного прохода, от выходов ко входам, в случае ЧС частей формулы после РЗО так же нет направления.
(про направление в КНФ говорить бессмысленно, ибо там всё может быть перемешано; но если не перемешано, то почему бы не использовать?)
Что можно сделать.
Первое, это использовать всю формулу. После РЗО использовать все полученные части с вычисленными блокирующими литералами, перемешав их случайно или использовать порядок РЗО. Как ни странно, даже взятие случайного литерала из ограничения и взятие ограничений в случайном порядке работает вполне неплохо.
Второе, это использование всех ограничений, как-то касающихся переменной. Если у нас есть ограничение x1+x2+x3 (xi - литерал переменной vi), то оно должно быть использовано и при вычислении значения v1, и при вычислении значения v2 и при вычислении значения v3.
Третье, мы можем попробовать восстановить или как-то задать направление вычислений. В соображении выше мы можем упорядочивать работу с ограничениями по рассматриваемой переменной, в порядке возрастания или убывания. Мы, также, можем ограничить ограничения, что будут использованы при вычислении значения переменной - содержащими только переменные меньшие или равные вычисляемой, тогда у нас "проход по схеме в направлении выхода," или ограничения должны содержать переменные большие или равные вычисляемой, тогда у нас получится "проход по схеме от выхода ко входу."
Переменные КНФ (схемы вообще) можно разделить на "хребет" и остальные. Переменные "хребта" имеют одно и то же значение при всех удовлетворяющих присваиваниях. Остальные переменные могут принадлежать какому-то классу (не)равенства - где при всех удовлетворяющих присваиваниях они обязательно (не) равны друг другу. Типичная задача разложения на множители для N=PQ, где P и Q простые, содержит довольно много переменных хребта и один класс (не)равенства - переменные, не принадлежащие хребту, в одном из двух решений либо 0, либо 1. Ну, так уж получилось, что класс там один, может быть больше, да ещё и условных (если P или Q составные). В статье выше переменные разделяются по классам равенства, то есть, в любом истинном присваивании они равны между собой. Я считаю, что соединять можно и по равенству, и по неравенству.
Так вот.
Если в результате прогона какая-то переменная получила значение "все 0" или "все 1," то можно (осторожно) считать, что её значение таковым и является. Чем длиннее массив битов, представляющий значение переменной, тем выше вероятность, что так и есть.
Если в результате прогона какие-то две переменных получили значения равные друг другу, ровно с той же осторожностью можно считать их равными. Если значение одной равно дополненному до 2 значению другой, то столь же осторожно можно считать переменные строго неравными друг другу.
Равенства и неравенства можно объединять через классы равенств. v1=v2 и v2=v3 можно перевести в v1=v2 и v1=v3, и тогда упрощение формулы становится проще выполнить.
В завершение скажу, что все алгоритмы выше приводят к некоторому насыщению - из КНФ мы можем извлечь N констант и M (не)равенств, после чего они перестают работать. Тем не менее, некоторое упрощение вполне можно получить, уменьшив количество переменных и ограничений в КНФ раза в полтора, если повезёт.