Table Constraints in Clause Learning CSP Solvers
Erdem, Ozan, George Katsirelos, Fahiem Bacchus · HAL (Le Centre pour la Communication Scientifique Directe) · 2013
We investigate alternative methods for implementing table constraints in clause learning CSP solvers (CL solvers). CL solvers have been an important development in CP solving as they can provide important performance improvements on some problems. Furthermore, table constraints remain an important and useful modeling tool in CP. Hence, it is important to be able to utilize table constraints in CL solvers effectively. Here we compare different ways of achieving GAC propagation over table constraints in a CL solver. These methods require different representations of the constraint. First we utilize a CNF encoding of the table constraint which has the property that unit propagation achieves GAC. We compare this with the use of a traditional GAC propagation algorithm for tables, Simple Tabular Reduction (STR). To utilize STR in a CL solver we also develop a method for extracting clausal explanations for pruned values from it. We also develop and test a negative version of STR which more compactly represents tables that have fewer falsifying than satisfying tuples, which also generates clausal explanations. We implement these different methods in the CL solver minicsp, and analyze their performance empirically.