Alternating Symmetry-Breaking Combinatorial Search with SAT

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.