Solving Constraint Satisfaction Problems with NB-Resolution

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

Ämnesord

NATURVETENSKAP  -- Matematik -- Beräkningsmatematik (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Computational Mathematics (hsv//eng)

Publikations- och innehållstyp

vet (ämneskategori)

rap (ämneskategori)