Constraint satisfaction problems in clausal form

TL;DR

This paper explores the foundations of satisfiability for generalized conjunctive normal forms with non-boolean variables, focusing on autarkies, translations to boolean clause-sets, and properties of minimally unsatisfiable clause-sets.

Contribution

It introduces a theoretical framework for non-boolean SAT problems, including polynomial time results, classifications of minimally unsatisfiable clause-sets, and connections to graph hermitian rank.

Findings

Polynomial time results related to deficiency

Classification of minimally unsatisfiable clause-sets

Relations between clause-sets and graph hermitian rank

Abstract

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.