Alternating Symmetry-Breaking Combinatorial Search with SAT (Research Project)
Project Acronym: ASK-SAT (Alternating Symmetry-Breaking Combinatorial Search with SAT)
Funding organization: Austrian Science Fund (FWF)
Project number: P 36688
Grant DOI: 10.55776/P36688
Project Team
Topic
Many unsolved problems in discrete mathematics and extremal combinatorics can be stated as whether a combinatorial object with a particular property and size exists.
The project focuses on developing novel methods for answering such questions using the innovative Satisfiability Modulo Symmetries (SMS) technique. This approach departs from traditional exhaustive search strategies by dynamically identifying and excluding redundant sub-configurations, thus streamlining the search process while utilizing the power of solvers for the propositional satisfiability problem (SAT).
The project aims to extend the capabilities of SMS to effectively tackle the existence of objects whose defining property requires alternating quantifiers, which present unique challenges beyond the scope of conventional SAT methods. This involves integrating advanced computational tools, including quantified Boolean formulas and symmetry-reasoning technologies.
Through this research, the project aspires to advance the fields of automated reasoning and discrete mathematics.
Software
The software tool developed through the project is available via GitHub, the documentation via Read the Docs.
Publications
20 results| 2026 | |
| [20] | A General Theoretical Framework for Learning Smallest Interpretable Models Artificial Intelligence, volume 350, pages 104441, 2026. |
| [19] | Backdoors to Satisfaction Continued Computer Science Review, volume 60, pages 100868, 2026. |
| [18] | OBDDs, SDDs, and Circuits of Bounded Width: Completeness Matters Artificial Intelligence, volume 351, pages 104458, 2026. |
| [17] | ASP-Bench: From Natural Language to Logic Programs Proceedings of the 2nd IEEE/ACM International Workshop on Neuro-Symbolic Software Engineering (NSE '26), 2026, Assoc. Comput. Mach., New York. Note: To appear; preprint: CoRR abs/2602.01171, https://arxiv.org/abs/2602.01171 |
| [16] | ContReAct: A Feedback-Based Architecture for Continuous Agentic Operation Proceedings of the 2026 International Workshop on Agentic Engineering (AGENT '26), 2026, Assoc. Comput. Mach., New York. Note: To appear |
| [15] | Smart Cubing for Graph Search: A Comparative Study 32nd International Conference on Principles and Practice of Constraint Programming, CP 2026, July 20–23, 2026, Lisbon, Portugal, 2026, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Note: To appear; preprint: CoRR abs/2501.17201, https://arxiv.org/abs/2501.17201 |
| [14] | Graph Choosability via SAT: Beyond the Nullstellensatz The 40th Annual AAAI Conference on Artificial Intelligence, AAAI-2026, pages 14269–14277, 2026. |
| 2025 | |
| [13] | Generating Streamlining Constraints with Large Language Models Journal of Artificial Intelligence Research, volume 84, pages 16:1–16:19, 2025. Note: Abstract reprint in AAAI 2026, page 39900 |
| [12] | StreamLLM: Enhancing Constraint Programming with Large Language Model-Generated Streamliners 2025 IEEE/ACM 1st International Workshop on Neuro-Symbolic Software Engineering (NSE), pages 17-22, 5 2025, IEEE Computer Soc.. |
| [11] | The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, August 10-15, 2025, Glasgow, Scotland (Maria Garcia de la Banda, ed.), volume 340 of LIPIcs, pages 39:1–39:19, 2025, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
| [10] | SAT Modulo Symmetries: A Survey Satisfiability Checking and Symbolic Computation, 10th International Workshop, SC-Square 2025, Stuttgart, Germany, August 2, 2025, co-located with CADE 2025, volume 4116 of CEUR Workshop Proceedings, pages 1–11, 2025, CEUR-WS.org. |
| [9] | Breaking Symmetries in Quantified Graph Search: A Comparative Study AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA (Toby Walsh, Julie Shah, Zico Kolter, eds.), pages 11246–11254, 2025, AAAI Press. |
| 2024 | |
| [8] | SAT Modulo Symmetries for Graph Generation and Enumeration ACM Transactions on Computational Logic, volume 25, number 3, 2024. |
| [7] | SAT backdoors: Depth beats size Journal of Computer and System Sciences, volume 142, pages 103520, 2024. |
| [6] | Revisiting Causal Discovery from a Complexity-Theoretic Perspective Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24 (Kate Larson, ed.), pages 3377–3385, 8 2024, International Joint Conferences on Artificial Intelligence Organization. Note: Main Track |
| [5] | Compilation and Fast Model Counting beyond CNF Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24 (Kate Larson, ed.), pages 3315–3323, 8 2024, International Joint Conferences on Artificial Intelligence Organization. Note: Main Track |
| [4] | SAT-Based Tree Decomposition with Iterative Cascading Policy Selection AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 8191–8199, 2024, AAAI Press. |
| [3] | A General Theoretical Framework for Learning Smallest Interpretable Models AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 10662–10669, 2024, AAAI Press. |
| [2] | Computing small Rainbow Cycle Numbers with SAT modulo Symmetries The 30th International Conference on Principles and Practice of Constraint Programming, CP 2024 (Paul Shaw, ed.), 2024, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
| [1] | Learning Small Decision Trees for Data of Low Rank-Width AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 10476–10483, 2024, AAAI Press. |
