Solving Temporal CSPs via Enumeration and SAT Compilation
Leif E. B. Eriksson · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2019
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;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.