Function synthesis for maximizing model counting
summary
Defines DQMax#SAT as a strict generalization of Max#SAT that subsumes DQBF and DSSAT and proves NEXPTIME-completeness, gives a concrete reduction to Max#SAT by encoding each maximizing variable as selectors over its minterms (introducing an exponential number of minterms), and builds an incremental reduction to Max#SAT that refines dependency sets to produce anytime lower bounds. Implements a prototype solver in Verimag that uses MaxSAT oracles (probabilistic MaxHS/D4 variants), reports the running example yields a 3/4 optimum, and shows dependency set size drives exponential blowup and memory blowups on hard benchmarks.
AI-written summary · about
chapters (11)
- 0:00Function synthesis for model counting
- 2:49Attacker strategy synthesis challenges
- 3:54Problem specification and example
- 6:04Related problems and generalizations
- 7:51Reduction to MaxSAT solving
- 9:59Incremental dependency handling
- 13:10Local simplification procedures
- 14:53Implementation and solver details
- 15:35Experimental results and applications
- 15:56Conclusion and future work
- 16:38Q&A
related talks
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
10mSATisfying answers to difficult questions!
18mSAT Beyond Boolean Interpretations
17mAlgebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
29mLet our optima combine!
52mCounting Solutions to Random Constraint Satisfaction Problems
14mGeneralizable Synthesis Through Unification
32mExplaining SAT Solving Using Causal Reasoning