Isomorph-Free Generation Of Combinatorial Objects With Sat Modulo Symmetries
summary
SMS claims a practical, certifying way to generate combinatorial objects without isomorphic duplicates by integrating a CDCL SAT solver with dynamic symmetry-breaking and a MinCheck propagator that reasons on partially defined graphs via ordered partitions. Implementation in C++ (with CaDiCaL/IPASIR and a Python wrapper) produces DRAT-checkable proofs, enumerates diameter-2-critical graphs up to 13 vertices and proves nonexistence up to 19 in some bounds, adds a Kuratowski planarity propagator for planar Turán and narrows cases in the Earth–Moon problem.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:57Generation of Combinatorial Objects
- 2:42Isomorph-Free Generation
- 4:49Example: connected graphs
- 5:23Generate & Test
- 6:36Static SAT approach
- 9:19Dynamic SAT approach
- 11:15Dynamic Symmetry Breaking with SMS
- 13:20Natural partial order
- 14:13Canonicity of partially defined graphs
- 22:59Iterative Ordered Partition Refinement
- 23:47Propagation
- 27:35Obstruction
- 30:37Implementation
- 36:07Generating Planar Graphs with SMS
- 39:17Earth-Moon problem: background
- 41:45Summary
related talks
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
01h 04mExplicit SoS Lower Bounds from (Small-Set) High Dimensional Expanders
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
23mVerified Code Generation for the Polyhedral Model
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
27mProducing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver