Research map / Graph learning / Graph algorithms and clustering
Breaking Symmetries in Quantified Graph Search: A Comparative Study
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Extends SAT Modulo Symmetries to quantified Boolean formulas, comparing a static QBF canonicity encoding (Q-static) and dynamic SMS integration into QBF solvers (Q-SMS, including a new 2-QBF solver 2Qiss) against co-certificate learning on quantified graph search problems.
Problem
Generating and enumerating graphs up to isomorphism when properties are coNP-complete (quantified constraints), where SAT Modulo Symmetries cannot directly handle quantifiers and redundant isomorphic graphs slow search.
Approach
Encode graph canonicity with universal variables for permutations (Q-static) or integrate an SMS minimality check as a propagator inside circuit-based QBF solvers (Qfun, CQesto, Qute) and a new CEGAR 2-QBF solver 2Qiss, yielding a uniform, proof-producing alternative to custom co-certificate learning.
Key results
- CCL is typically 2-3x faster than 2Qiss on the same instances (e.g., 6, 63, 34 minutes vs 18, 122, 58 minutes).
- Q-static scales poorly: solves at most 14 vertices on snarks and none on Kochen-Specker instances.
- 2Qiss solved 110 instances, the most among QBF solvers (Qfun 104, CQesto 90, Qute 72); Qute produced 1874 verified proofs for 70 instances.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use Q-SMS instead of Q-static | Quantified graph search · Domination conjectures (i), (ii), and (iii) | largest solved n: 12 -> 28; 12 -> 34; 12 -> 30 | Helped |
| Use Q-SMS instead of Q-static | Quantified graph search · Folkman (3,3;4), Folkman (3,3;5), and snarks, girth 5 | largest solved n: 11 -> 15; 10 -> 12; 14 -> 20 | Helped |
| Use Q-SMS instead of Q-static | Quantified graph search · Treewidth 4 and Treewidth 5 | largest solved n: 9 -> 9; 9 -> 9 | No clear effect |
| Use Q-SMS instead of Q-static | Quantified graph search · Triangle-free non-3-colorable | largest solved n: 13 -> 15 | Helped |
| Use Q-SMS instead of Q-static | Quantified graph search · Maximal triangle-free non-4-colorable | largest solved n: 12 -> 20 | Helped |
| Use Q-SMS instead of CCL | Quantified graph search · Triangle-free non-3-colorable, maximal triangle-free non-4-colorable, and Kochen-Specker candidates | largest solved n: 15 -> 15; 20 -> 20; 20 -> 20 | No clear effect |
| Use Q-SMS instead of CCL | Quantified graph search · Applicable problems | runtime: 2--3 times faster | Hurt |
| Use 2Qiss instead of the other evaluated QBF solvers | QBF solving · Graph benchmark instances | instances solved: 110 vs 104; 90; 72; 57; 55 | Helped |
| Use the static QBF minimality encoding | Quantified graph search · Graph benchmark instances | instances solved: 57; 55 | Hurt |
| Use Qute with proof logging | Qute · Solved graph instances | proofs produced: 1874 proofs | Helped |
Surprising findings
- The new simple 2-QBF solver 2Qiss outperformed established QBF solvers, contrary to expectation.
- The static QBF minimality encoding (Q-static) performs poorly on almost all instances regardless of vertex ordering.
Limitations
- CCL remains about 2-3 times faster than the best QBF-based method (2Qiss) on the same instances.
- Qute's proof logging is limited to 30-minute runs because proofs grow too large; the circuit-to-CNF translation is not certified.
Experimental setup
Datasets: quantified graph search benchmark instances (triangle-free non-k-colorable, Folkman, domination conjecture, treewidth, s
Benchmarks: triangle-free non-3-colorable max triangle-free non-4-colorable Kochen-Specker domination conjecture Folkman (3,3;4) and (3,3;5) treewidth 4 and 5 snarks girth 5
Metrics: largest solvable number of vertices within 4 hours CPU number of solved instances
Baselines: CCL (co-certificate learning) Q-static (minqbf) Qfun CQesto Qute
Builds on: SAT Modulo Symmetries co-certificate learning RAReQS Qute CaDiCaL
Closest papers by meaning
- Computationally Hard Problems Are Hard for QBF Proof Systems Too (AAAI 2025 · similarity 0.87)
- Using Symmetries to Lift Satisfiability Checking (AAAI 2024 · similarity 0.85)
- Exploiting Symmetries in MUS Computation (AAAI 2025 · similarity 0.85)
- SAT-Based Algorithms for Regular Graph Pattern Matching (AAAI 2024 · similarity 0.84)
- Complete Symmetry Breaking for Finite Models (AAAI 2025 · similarity 0.84)
- Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.