##
Satisfiability and the Computation of Combinatorial Numbers

Victor W. Marek

Department of Computer Science

University of Kentucky

Lexington, KY 40506-0046

marek@cs.uky.edu
(Joint work with M. R. Dransfield)

### ABSTRACT

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.