| 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 |
|---|