ASK-SAT: Alternating Symmetry-Breaking Combinatorial Search with SAT

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

• Stefan Szeider (PI)
• Markus Kirchweger
• Tomas Peitl
• Florentina Voboril

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.