On the Propagation Strength of SAT Encodings for Qualitative Temporal Reasoning

Several studies in Qualitative Spatial and Temporal Reasoningdiscuss translations of the satisfiability problem on qualitativeconstraint languages into propositional SAT. Most of these encodings focus on compactness, while propagation strength is seldom discussed. In this work, we focus on temporal reasoning with the Point Algebra and Allen's Interval Algebra. We understand all encodings as a combination of propagation andsearch. We first give a systematic analysis of existing propagation approachesfor these constraint languages. They are studied and ordered with respect to their propagation strengthand refutation completeness for classes of input instances. Secondly, we discuss how existing encodings can be derived fromsuch propagation approaches. We conclude our work with an empirical evaluation which shows that theolder ORD-encoding by Nebel and Bürckert performs better than more recently suggested encodings.