A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints

The problem of solving boolean combinations of difference constraints is at the core of many important techniques such as planning, scheduling, and model-checking of real-time systems. Efficient decision procedures for this class of formulas are, therefore, strongly needed. In this paper we present TSAT++, a SAT-based open reasoning platform able to decide boolean combinations of difference constraints. Experimental results indicate that TSAT++ outperforms its competitors both on randomly-generated, hand-made and real world problems.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, Marco Maratea
• Keywords: Boolean Combinations, Difference Constraints, SAT 2004, SAT-based Open Reasoning