Линейный сб Unsat против линейного Unsat сб

Question

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

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

Answer 1

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

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