SAT for Optimization
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
SAT for optimization frames optimization as repeated SAT decision queries (encode feasibility plus objective ≤ Q) and shows MaxSAT as the practical formalism: hard clauses plus weighted soft clauses. Modern solvers use cores returned under assumptions to build small cardinality encodings rather than huge global encodings (cardinality encodings blow up quadratically, so 100k inputs are impractical). An alternate implicit hitting/hidden-set approach computes lower bounds via minimal hitting sets; exchangeable soft-clause sets can force exponentially many cores, so abstracting by sums (as in recent MaxHS work) compresses many cores and yields state‑of‑the‑art performance.
AI-written summary · about