Linear Sat Unsat vs Linear Unsat Sat

Я знаю, что оба приведенных выше алгоритма подходят для итеративных решений, чтобы найти оптимум для проблем MAXSAT, но мне было интересно, почему это, начиная с удовлетворительной стороны, при поиске решения для MAXSAT лучше, чем искать его с неудовлетворительной стороны?

Также здесь «Удовлетворительная сторона» означает ослабление всех возможных мягких предложений до тех пор, пока мы не дойдем до UNSAT, а сторона «Неудовлетворительность» означает, что начало без предложений ослаблено до увеличения числа до тех пор, пока мы не дойдем до SAT.


constraint-programming constraint-satisfaction sat sat-solvers satisfiability
person lava_07    schedule 04.05.2020    source источник
comment
Определите лучше. Это разные подходы, и теория и практика могут сильно отличаться. Существуют также гибриды или подходы, такие как алгоритмы на основе неподатливого ядра, которые я не мог легко сопоставить с вашим разделением подходов. Теоретически есть рассуждения о NP (проверка выполнимости: сверху) и coNP (доказательство невозможности: снизу). Эмпирически для большинства алгоритмов вы обнаружите, что последние итерации, коснувшиеся границы SAT / UNSAT, будут самый сложный / самый медленный. Это, вероятно, связано с эмпирическими вещами, такими как эвристика, но также и с теорией доказательств (см. pigeonhole sat).   -  person sascha    schedule 04.05.2020

Ответы (1)


arrow_upward
1
arrow_downward

Задачи MAX-SAT обычно связаны с неудовлетворительными формулами. Доказательства невыполнимости в среднем сложнее написать, чем доказательства выполнимости. Доказательства неудовлетворенности также имеют тенденцию усложняться по мере того, как вы удаляете ограничения из экземпляра, причем чрезмерное ограничение является основной причиной того, что некоторые неудовлетворительные экземпляры являются легкими.

Итак, с помощью одного метода вы начинаете с простых экземпляров, для которых постепенно становится все труднее писать доказательства SAT / UNSAT, по сравнению с другим методом, который начинает с попытки написать жесткие доказательства и вознаграждается тем, что на следующей итерации приходится писать еще более сложный.

person Kyle Jones    schedule 04.05.2020