WIDER RESEARCH CONTEXT
Propositional satisfiability (SAT) is the canonical NP-complete problem, with applications across computer science and beyond. In this proposal, we want to study the applications of SAT to combinatorial search. In a combinatorial search problem, we are asked to find a combinatorial structure with a prescribed property. An example would be finding a smallest triangle-free graph with a given chromatic number (vertices properly colorable with k but no fewer colors).
OBJECTIVES
Some combinatorial search problems are amenable to a polysize SAT encoding. Still, others are not, including the example above: one can express succinctly that a graph should be triangle-free, but not that it should not be k-1-colorable. The latter requires a universal quantifier to say that no coloring is proper. We call such problems alternating search problems after the quantifier alternation pattern.
In this proposal, we want to solve alternating search with SAT technology.
APPROACH
Combinatorial and alternating search problems are often abundant in symmetries. When searching exhaustively, it is wasteful to test symmetric copies, and solvers that can detect them gain an advantage. Such search tactics are known as symmetry breaking.
Symmetry breaking is most often performed statically: before solving, add a symmetry-breaking constraint to the formula to select just one canonical object in each symmetry class. Static symmetry breaking has many strengths and one fatal weakness: the constraint can easily get exponentially large.
To avoid huge static symmetry-breaking constraints, we recently proposed a new method called Satisfiability Modulo Symmetries (SMS). In SMS, instead of breaking symmetries statically upfront, the SAT solver is endowed with a symmetry propagator, which is called dynamically and checks whether partial assignments are canonical.
INNOVATION
SMS currently only works for SAT, and alternating search problems do not admit polysize SAT encodings. We will explore several options of lifting SMS to alternating search: using pure SAT, quantified Boolean formulas (QBF), and symmetry-reasoning packages such as Nauty. Additionally, we expect to encounter and tackle theoretical questions about the complexity of SMS and symmetry breaking.
Our main goal is to advance SAT-based and symmetry-breaking methods, and alternating search serves mainly as a benchmarking domain. However, we also include a catalog of open alternating search problems, and we expect to make progress on several of them. This includes graph and hypergraph search problems, problems in matroid theory, and even SAT theory itself.
