Solving Temporal CSPs via Enumeration and SAT Compilation

Abstract: The constraint satisfaction problem (CSP) is a powerful framework used in theoretical computer science for formulating a  multitude of problems. The CSP over a constraint language Γ (CSP(Γ)) is the decision problem of verifying whether a set of constraints based on the relations in Γ admits a satisfying assignment or not. Temporal CSPs are a special subclass of CSPs frequently encountered in AI. Here, the relations are first-order definable in the structure (Q;<), i.e the rationals with the usual order. These problems have previously often been solved by either enumeration or SAT compilation. We study a restriction of temporal CSPs where the constraint language is limited to logical disjunctions of <-, =-, ≠- and ≤-relations, and were each constraint contains at most k such basic relations (CSP({<,=,≠,≤}∨k)).   Every temporal CSP with a finite constraint language Γ is polynomial-time reducible to CSP({<,=,≠,≤}∨k) where k is only dependent on Γ. As this reduction does not increase the number of variables, the time complexity of CSP(Γ) is never worse than that of CSP({<,=,≠,≤}∨k). This makes the complexity of CSP({<,=,≠,≤}∨k) interesting to study.   We develop algorithms combining enumeration and SAT compilation to solve CSP({<,=,≠,≤}∨k), and study the asymptotic behaviour of these algorithms for different classes. Our results show that all finite constraint languages Γ first order definable over (Q;<) are solvable in O'(((1/(eln(2))-ϵk)n)^n) time for some ϵk>0 dependent on Γ. This is strictly better than O'((n/(eln(2)))^n), i.e. O'((0.5307n)^n), achieved by enumeration algorithms. Some examples of upper bounds on time complexity achieved in the thesis are CSP({<}∨2) in O'((0.1839n)^n) time, CSP({<,=,≤}∨2) in O'((0.2654n)^n) time, CSP({<,=,≠}∨3) in O'((0.4725n)^n) time and CSP({<,=,≠,≤}∨3) in O'((0.5067n)^n) time. For CSP({<}∨2) this should be compared to the bound O'((0.3679n)^n), from previously known enumeration algorithms.