Satisfiability and the Computation of Combinatorial Numbers

Victor W. Marek
Department of Computer Science
University of Kentucky
Lexington, KY 40506-0046

(Joint work with M. R. Dransfield)


Numerous theorems in Combinatorics follow this schema: "For every natural number k, l, m, ... there exists n such that no ``configuration'' (depending on k, l, m, n) exists. The most celebrated examples of such results are Schur theorem on sum-free sets, van der Waerden theorem on monochromatic arithmetic progressions, Ramsey theorem on monochromatic cliques and Hales-Jewett theorem on the generalized tic-tac-toe game. All these theorems can be reformulated in such a way that the existence of a desired ``configuration'' is equivalent to satisfiability of an appropriate chosen propositional formula.

The significant progress in software tools called SAT-solvers (which find if an input propositional formula has a satisfying assignment, and if so, exhibit one), indicates that some classical computational combinatorial problems may be solved with this software.

While it would be naive to think that SAT-solvers can compete with specialized software devoted to combinatorial numbers computation, it turns out that for some of the problems the results one obtains are comparable to such specialized software.

At this stage, SAT solvers are not able to rediscover the most spectacular results in the area (e.g. McKay and Radziszowski's result on R(4,5)). But the progress in the area is fast, and it is likely that this and other subtle results will soon be reproved using SAT-solvers.

Colloquia Series page.