Solving Temporal CSPs via Enumeration and SAT Compilation
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 satisf...
Main Author: | |
---|---|
Format: | Others |
Language: | English |
Published: |
Linköpings universitet, Institutionen för datavetenskap
2019
|
Subjects: | |
Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-162482 |
id |
ndltd-UPSALLA1-oai-DiVA.org-liu-162482 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-UPSALLA1-oai-DiVA.org-liu-1624822019-12-11T15:42:34ZSolving Temporal CSPs via Enumeration and SAT CompilationengEriksson, LeifLinköpings universitet, Institutionen för datavetenskap2019CSPAlgorithmsComputer SciencesDatavetenskap (datalogi)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. Student thesisinfo:eu-repo/semantics/bachelorThesistexthttp://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-162482application/pdfinfo:eu-repo/semantics/openAccess |
collection |
NDLTD |
language |
English |
format |
Others
|
sources |
NDLTD |
topic |
CSP Algorithms Computer Sciences Datavetenskap (datalogi) |
spellingShingle |
CSP Algorithms Computer Sciences Datavetenskap (datalogi) Eriksson, Leif Solving Temporal CSPs via Enumeration and SAT Compilation |
description |
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. |
author |
Eriksson, Leif |
author_facet |
Eriksson, Leif |
author_sort |
Eriksson, Leif |
title |
Solving Temporal CSPs via Enumeration and SAT Compilation |
title_short |
Solving Temporal CSPs via Enumeration and SAT Compilation |
title_full |
Solving Temporal CSPs via Enumeration and SAT Compilation |
title_fullStr |
Solving Temporal CSPs via Enumeration and SAT Compilation |
title_full_unstemmed |
Solving Temporal CSPs via Enumeration and SAT Compilation |
title_sort |
solving temporal csps via enumeration and sat compilation |
publisher |
Linköpings universitet, Institutionen för datavetenskap |
publishDate |
2019 |
url |
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-162482 |
work_keys_str_mv |
AT erikssonleif solvingtemporalcspsviaenumerationandsatcompilation |
_version_ |
1719302728165883904 |