Linear Sat Unsat vs Linear Unsat Sat

Question

I know both the above algorithm come under iterative solutions to find an optimum for MAXSAT problems but I was wondering why is it that starting from the Satisfiable side while finding a solution for MAXSAT better than searching for it from the Unsatisfiable side?

Also here Satisfiable side means relaxing all possible soft clauses until we hit UNSAT and Unsatisfiability side means starting with no clauses relaxed to increasing the number until we hit SAT

Answer 1

MAX-SAT problems are generally concerned with unsatisfiable formulas. Unsatisfiability proofs are, in the average case, harder to write than satisfiability proofs. Unsatisfiability proofs also tend to get harder as you remove constraints from an instance, overconstraint being the primary reason some unsatisfiable instances are easy.

So with one method you're starting with easy instances that gradually get harder to write SAT/UNSAT proofs for, versus the other method that starts out trying to write hard proofs and is rewarded by having to write an even harder one the next iteration.