A Novel EGs-Based Framework for Systematic Propositional-Formula Simplification
summary
A framework implements existential graphs plus binary implication graph analysis as a directed cyclic hypergraph to simplify arbitrary propositional formulas without CNF flattening. It guarantees equivalence, monotonic size reduction, termination, and finds unit clauses and equivalences for propagation; implemented prototype handles industrial benchmarks with millions of clauses and hundreds of thousands of variables and yields extra reductions (up to 11% more reduction after Minisat preprocessing) while slowing runtime versus highly tuned preprocessors.
AI-written summary · about
chapters (11)
- 0:00Simplify propositional formulas
- 2:56Limitations of simplification
- 4:22Pierce existential graphs
- 7:17Binary implication graphs
- 10:49Properties of new approach
- 12:33Advanced rules and implementation
- 15:00Proofs and theorem discovery
- 18:32Comparison with DPLL
- 20:59Impact on model counting
- 23:27Conclusion and future work
- 25:33Q&A
related talks
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
47mLogic Programming à la Carte
01h 04mKnowledge Compilation for Quantification and Synthesis
14mPredicate E-Graphs with Symbolic Conditional Rewriting
30mSemantics-Guided Synthesis
19mAutomated Verification of Fundamental Algebraic Laws
24mSimplifying Multiple-Statement Reductions with the Polyhedral Model
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...