Источник удивления
https://cca.informatik.uni-freiburg.de/papers/BalyoFrohlichHeuleBiere-SAT14.pdf и ещё статья про blocked clause decomposition https://www.cs.cmu.edu/~mheule/publications/bcd.pdf
Ограничение C может быть заблокировано переменной x (литерал x или !x входит в ограничение C), если любое разрешение (resolution) по x приводит к тавтологии. Такое ограничение можно исключить из формулы и решать её без неё. После обнаружения решения, если C не удовлетворено, надо изменить решение, заменив литерал переменной x на его отрицание (если x=1, то надо принять x=0 и наоборот).
Устранение заблокированных ограничений обладает свойством сходимости - с какого ограничения не начни, придёшь к тому же набору. Если у вас КНФ получена преобразованиями Цейтина из логической формулы, то у неё есть тривиальное разбиение - на разрешаемое через устранение заблокированных ограничений множество ограничений КНФ без ограничений на входы и выходы (L) и ограничения на входы и выходы (R, обычно это логические константы).
Однако, господа, что писали статьи выше, сосредоточились на разбиении КНФ формулы F на подформулы L и R, что могут быть решены с помощью устранения заблокированных ограничений. При этом большая часть полезных результатов получается при максимальном разбиении, когда L (large или left, большая часть разбиения) много больше R, но R вовсе не используется.
Вопрос, а почему R должен быть разрешаем с помощью устранения заблокированных ограничений, если R не используется, а почти всё извлекается только из L (SAT sweeping), оставлен без ответа. Вопрос, а не можем ли мы получить больший (и более выгодный) L, если R не может быть разрешён через устранение заблокированных ограничений, также оставлен без ответа - хотя важен. Вопрос, можем ли мы R, неразрешимый с помощью устранения заблокированных ограничений, снова разбить на разрешимые подмножества (см. алгоритм PureDecompose, он с этим справится), конечно же, оставлен без ответа. Как и то, что из этого следует.
Удивительно, почему им никто эти вопросы не задал.
Я наткнулся на статью китайца по следам статей выше, так он тоже не задаёт эти неудобные вопросы.
Ну-с, теперь вы будете спать так же плохо, как и я. ;)
Ограничение C может быть заблокировано переменной x (литерал x или !x входит в ограничение C), если любое разрешение (resolution) по x приводит к тавтологии. Такое ограничение можно исключить из формулы и решать её без неё. После обнаружения решения, если C не удовлетворено, надо изменить решение, заменив литерал переменной x на его отрицание (если x=1, то надо принять x=0 и наоборот).
Устранение заблокированных ограничений обладает свойством сходимости - с какого ограничения не начни, придёшь к тому же набору. Если у вас КНФ получена преобразованиями Цейтина из логической формулы, то у неё есть тривиальное разбиение - на разрешаемое через устранение заблокированных ограничений множество ограничений КНФ без ограничений на входы и выходы (L) и ограничения на входы и выходы (R, обычно это логические константы).
Однако, господа, что писали статьи выше, сосредоточились на разбиении КНФ формулы F на подформулы L и R, что могут быть решены с помощью устранения заблокированных ограничений. При этом большая часть полезных результатов получается при максимальном разбиении, когда L (large или left, большая часть разбиения) много больше R, но R вовсе не используется.
Вопрос, а почему R должен быть разрешаем с помощью устранения заблокированных ограничений, если R не используется, а почти всё извлекается только из L (SAT sweeping), оставлен без ответа. Вопрос, а не можем ли мы получить больший (и более выгодный) L, если R не может быть разрешён через устранение заблокированных ограничений, также оставлен без ответа - хотя важен. Вопрос, можем ли мы R, неразрешимый с помощью устранения заблокированных ограничений, снова разбить на разрешимые подмножества (см. алгоритм PureDecompose, он с этим справится), конечно же, оставлен без ответа. Как и то, что из этого следует.
Удивительно, почему им никто эти вопросы не задал.
Я наткнулся на статью китайца по следам статей выше, так он тоже не задаёт эти неудобные вопросы.
Ну-с, теперь вы будете спать так же плохо, как и я. ;)