Title :
SAT with Global Constraints
Author :
Chowdhury, Md Syeed ; Jia-Huai You
Author_Institution :
Dept. of Comput. Sci., Univ. of Alberta, Edmonton, AB, Canada
Abstract :
We present a tight integration of SAT with CP, called SAT(gc), which embeds global constraints into SAT. A prototype is implemented by integrating the state of the art SAT solver ZCHAFF and the generic constraint solver GECODE. Experiments are carried out for benchmarks from puzzle domains and planning domains to reveal insights in compact representation, solving effectiveness, and novel usability of the new framework.
Keywords :
computability; constraint handling; GECODE constraint solver; SAT(gc); ZCHAFF SAT solver; global constraint; planning domain; puzzle domain; satisfiability; Algorithm design and analysis; Artificial intelligence; Educational institutions; Electronic mail; Planning; Prototypes; Standards; Boolean Satisfiability; CP; Constraint Programming; Cross fertilization of SAT and CP; Integration of SAT and CP; SAT;
Conference_Titel :
Tools with Artificial Intelligence (ICTAI), 2012 IEEE 24th International Conference on
Conference_Location :
Athens
Print_ISBN :
978-1-4799-0227-9
DOI :
10.1109/ICTAI.2012.19
