A Two Stage Approach to Solve Constraint Satisfaction Problem.pdfVIP

A Two Stage Approach to Solve Constraint Satisfaction Problem Satish Chandra Gupta (scgupta@cs.uwm.edu) Project for CS710: Artificial Intelligence University of Wisconsin - Milwaukee May 2001 Abstract This study investigates solving a CSP by first independently solving each constraint and generating SAT encoding for all possible nogood for the constraint. And then solving SAT using a SAT solver. CSP solution is reconstructed from SAT solution. Experiments are performed on ILP problems. 1 Introduction CSP can be reduced to SAT and vice versa. Walsh[1] shows two ways to reduce a CSP problem to a SAT. This work is an attempt to solve CSP by first converting a CSP to SAT, then utilizing a SAT solver to solve the generated SAT, and then reconstructing CSP solution from SAT solution. A CSP is specified by specifying number of variables, their domains and the constraints. For example, a simple CSP, with 3 variables and 4 constraints, can be defined as following: # Number of variables 3 ; ; # Domains X(0) IN [2, 8] ; X(1) IN [-5, 10]; X(2) IN [-7, -3]; ; # Constraints 2 * X(1) - 2 * X(0) 5 ; -2 * X(0) + 3 * X(2) = -10 ; 5 * X(1) = 34 ; 3 * X(1) + 7 * X(2) 0 ; # End of CSP We will use this example to explain different steps in the process. In first phase of SAT encoding generation, constraints are used to refine the domains of variables. In second phase SAT is generated using Log Encoding for each nogood. 2 Domain Refinement A constraint can be represented by 
    , where  is one of the operators  . If ! #$ % ( *) , the maximum value of a term  + in the constraints can be defined as following: ,.-       /  10 32   54   0 % 27698;: =9 @? And the minimum value can be defined as: , # A *+  /   0 % 2   54   0  2B698;: = C? Then, , #
 D E 
F , # A DE# , and ,G- 
HI A  
F ,.-  A EC For less than constraint,
FI E   , for any J , A +9