SAT Beyond Boolean Interpretations
summary
Given a CNF formula, the goal is to maximize its value under interpretations over a semiring K rather than Boolean truth; for the Viterbi semiring (values in [0,1], AND = multiplication, OR = max, negation ≈ 1−x) this yields the decision/search problem OptSemVal. The problem reduces from MaxSAT via a gadget that forces the optimum to be 1/4^{m−r} where r is the max satisfiable clauses, and lies in FP^{NP[log]} using number-rationality bounds tied to Farey sequences. Approximation thresholds 0.716^m (algorithm) and hardness beyond 0.845 (inapproximability) are proved.
AI-written summary · about
chapters (10)
- 0:00Start
- 2:20Beyond Boolean Interpretations
- 4:14Interpretation of Negation
- 4:50Useful Semirings
- 6:40Computational Problem OptSemVal
- 7:48Viterbi Interpretations
- 8:42Hardness for Viterbi
- 11:49Upperbound - Overview
- 13:38Approximation of OptSemVal over Viterbi
- 14:14Future Work
related talks
10mSATisfying answers to difficult questions!
20mFunction synthesis for maximizing model counting
41mCounting Solutions to Random CNF Formulas
44mCombinatorial Characterizations in Semidefinite Programming Duality: ...
29mLet our optima combine!
43mCapacity Analysis of Vector Symbolic Architectures
01h 04mLP/SDP Hierarchies and Sum of Squares Proofs 2
57mIt ain't over till it's over