×

A SAT-based decision procedure for the Boolean combination of difference constraints. (English) Zbl 1122.68583

Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 16-29 (2005).
Summary: The problem of deciding satisfiability of Boolean combinations of difference constraints is at the core of many important techniques such as planning, scheduling and bounded 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 system implementing a SAT-based decision procedure for this problem, and the techniques implemented in it; in particular, TSAT++ takes full advantage of recent SAT techniques. Comparative experimental results indicate that TSAT++ outperforms its competitors both on randomly generated, hand-made and real world problems.
For the entire collection see [Zbl 1075.68002].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

Chaff
PDFBibTeX XMLCite
Full Text: DOI