Knowledge Compilation for Quantification and Synthesis
summary
Claims that a much weaker compiled form than OBDDs/DNNFs suffices to do existential quantification and Boolean functional synthesis in polytime: the synthesis negation normal form (SynNNF) enforces a limited “y and ȳ unrealizability” that lets sequential quantifier elimination avoid exponential blowup. Implements two compilers, C2Syn (CNF-based) and DeConflict (counterexample-guided), and shows SynNNF is exponentially more succinct than input-first ROBDDs and often smaller than d-DNNF, while compilation still can be worst-case exponential.
AI-written summary · about
chapters (9)
- 0:00Knowledge compilation intro
- 0:44Boolean synthesis problem
- 12:21Skolem function synthesis
- 16:27Synthesis complexity impact
- 26:22Simplified synthesis view
- 33:46Efficient synthesis via compilation
- 44:25Introducing synthesis negation normal form
- 56:10Future research
- 1:01:20Q&A on synthesis
related talks
49mCompiling FO Sentences to Circuits: Upper Bounds and Lower Bounds on the Size of the Circuit
31mLetting users do the undecidable: lessons from program synthesis
14mLOUD: Synthesizing Strongest and Weakest Specifications
30mA Novel EGs-Based Framework for Systematic Propositional-Formula Simplification
30mSemantics-Guided Synthesis
30mRelatively Complete Verification of Probabilistic Programs
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
20mOptimal Program Synthesis via Abstract Interpretation