Oliver Kullmann — Page 2

arXiv2011

Constraint satisfaction problems in clausal form

This is the report-version of a mini-series of two articles on the foundations of satisfiability of conjunctive normal forms with non-boolean variables, to appear in Fundamenta Informaticae, 2011. These two parts are here bundled in one report, each part yielding a chapter. Generalised conjunctive normal forms are considered, allowing literals of the form "variable not-equal value". The first part sets the foundations for the theory of autarkies, with emphasise on matching autarkies. Main results concern various polynomial time results in dependency on the deficiency. The second part considers translations to boolean clause-sets and irredundancy as well as minimal unsatisfiability. Main results concern classification of minimally unsatisfiable clause-sets and the relations to the hermitian rank of graphs. Both parts contain also discussions of many open problems.

cs.DM↗

arXiv2010

Exact Ramsey Theory: Green-Tao numbers and SAT

We consider the links between Ramsey theory in the integers, based on van der Waerden's theorem, and (boolean, CNF) SAT solving. We aim at using the problems from exact Ramsey theory, concerned with computing Ramsey-type numbers, as a rich source of test problems, where especially methods for solving hard problems can be developed. In order to control the growth of the problem instances, we introduce "transversal extensions" as a natural way of constructing mixed parameter tuples (k_1, ..., k_m) for van-der-Waerden-like numbers N(k_1, ..., k_m), such that the growth of these numbers is guaranteed to be linear. Based on Green-Tao's theorem we introduce the "Green-Tao numbers" grt(k_1, ..., k_m), which in a sense combine the strict structure of van der Waerden problems with the (pseudo-)randomness of the distribution of prime numbers. Using standard SAT solvers (look-ahead, conflict-driven, and local search) we determine the basic values. It turns out that already for this single form of Ramsey-type problems, when considering the best-performing solvers a wide variety of solver types is covered. For m > 2 the problems are non-boolean, and we introduce the "generic translation scheme", which offers an infinite variety of translations ("encodings") and covers the known methods. In most cases the special instance called "nested translation" proved to be far superior.

cs.DM↗