Title: Solving Constraint Satisfaction Problems with NB-Resolution
Authors: Alan M. Frisch
Series: Linkping Electronic Articles in Computer and Information Science
ISSN 1401-9841
Issue: Vol. 4 (1999), No. 037
URL: http://www.ep.liu.se/ea/cis/1999/037/

Abstract: Though resolution and constraint satisfaction problems are two of the most developed areas in artificial intelligence, little has been done to explore the relationship between the two. This paper explores the relationship using the key observation that semantic trees, used in the study of resolution, and backtrack search spaces, used in the study of constraint satisfaction, are the same objects. The exploration results in the development of the NB-resolution rule of inference, a generalisation of ordinary resolution that can be used to solve constraint satisfaction problems. This paper proves that a clausal-form constraint satisfaction problem is backtrack-free if its constraints are closed under NB-resolution. This generalises the usual completeness result for resolution by telling us not only what happens when an unsatisfiable set of clauses is closed under resolution but also what happens when a satisfiable set of clauses is closed under resolution. The paper also presents a refinement of NB-resolution based on the order in which variables are considered in the search procedure.

Original publication 1999-12-30 Postscript part I -- Checksum
Checksum
(old) Information about recalculation of checksum
Postscript part II -- Checksum II
Checksum II (old) Information about recalculation of checksum