SAT-Based Procedures for Temporal Reasoning

In this paper we study the consistency problem for a set of disjunctive temporal constraints [Stergiou and Koubarakis, 1998]. We propose two SAT-based procedures, and show that—on sets of binary randomly generated disjunctive constraints—they perform up to 2 orders of magnitude less consistency checks than the best procedure presented in [Stergiou and Koubarakis, 1998]. On these tests, our experimental analysis confirms Stergiou and Koubarakis’s result about the existence of an easy-hard-easy pattern whose peak corresponds to a value in between 6 and 7 of the ratio of clauses to variables.

• Type: Conference
• Year: 1999
• Where: ECP
• Authors: Alessandro Armando, Claudio Castellini, Enrico Giunchiglia
• Keywords: Consistency Problem, Disjunctive Constraints—they, Disjunctive Temporal Constraints, ECP 1999, Robotics