Document

**Published in:** LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

A backdoor in a finite-domain CSP instance is a set of variables where each possible instantiation moves the instance into a polynomial-time solvable class. Backdoors have found many applications in artificial intelligence and elsewhere, and the algorithmic problem of finding such backdoors has consequently been intensively studied. Sioutis and Janhunen (KI, 2019) have proposed a generalised backdoor concept suitable for infinite-domain CSP instances over binary constraints. We generalise their concept into a large class of CSPs that allow for higher-arity constraints. We show that this kind of infinite-domain backdoors have many of the positive computational properties that finite-domain backdoors have: the associated computational problems are fixed-parameter tractable whenever the underlying constraint language is finite. On the other hand, we show that infinite languages make the problems considerably harder.

Peter Jonsson, Victor Lagerkvist, and Sebastian Ordyniak. Reasoning Short Cuts in Infinite Domain Constraint Satisfaction: Algorithms and Lower Bounds for Backdoors. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.CP.2021.32, author = {Jonsson, Peter and Lagerkvist, Victor and Ordyniak, Sebastian}, title = {{Reasoning Short Cuts in Infinite Domain Constraint Satisfaction: Algorithms and Lower Bounds for Backdoors}}, booktitle = {27th International Conference on Principles and Practice of Constraint Programming (CP 2021)}, pages = {32:1--32:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-211-2}, ISSN = {1868-8969}, year = {2021}, volume = {210}, editor = {Michel, Laurent D.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.32}, URN = {urn:nbn:de:0030-drops-153238}, doi = {10.4230/LIPIcs.CP.2021.32}, annote = {Keywords: Constraint Satisfaction Problems, Parameterised Complexity, Backdoors} }

Document

**Published in:** LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Uniqueness quantification (Exists!) is a quantifier in first-order logic where one requires that exactly one element exists satisfying a given property. In this paper we investigate the strength of uniqueness quantification when it is used in place of existential quantification in conjunctive formulas over a given set of relations Gamma, so-called primitive positive definitions (pp-definitions). We fully classify the Boolean sets of relations where uniqueness quantification has the same strength as existential quantification in pp-definitions and give several results valid for arbitrary finite domains. We also consider applications of Exists!-quantified pp-definitions in computer science, which can be used to study the computational complexity of problems where the number of solutions is important. Using our classification we give a new and simplified proof of the trichotomy theorem for the unique satisfiability problem, and prove a general result for the unique constraint satisfaction problem. Studying these problems in a more rigorous framework also turns out to be advantageous in the context of lower bounds, and we relate the complexity of these problems to the exponential-time hypothesis.

Victor Lagerkvist and Gustav Nordh. On the Strength of Uniqueness Quantification in Primitive Positive Formulas. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lagerkvist_et_al:LIPIcs.MFCS.2019.36, author = {Lagerkvist, Victor and Nordh, Gustav}, title = {{On the Strength of Uniqueness Quantification in Primitive Positive Formulas}}, booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)}, pages = {36:1--36:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-117-7}, ISSN = {1868-8969}, year = {2019}, volume = {138}, editor = {Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.36}, URN = {urn:nbn:de:0030-drops-109808}, doi = {10.4230/LIPIcs.MFCS.2019.36}, annote = {Keywords: Primitive positive definitions, clone theory, constraint satisfaction problems} }

Document

**Published in:** LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Many computational problems arising in, for instance, artificial intelligence can be realized as infinite-domain constraint satisfaction problems (CSPs) based on partition schemes: a set of pairwise disjoint binary relations (containing the equality relation) whose union spans the underlying domain and which is closed under converse. We first consider partition schemes that contain a strict partial order and where the constraint language contains all unions of the basic relations; such CSPs are frequently occurring in e.g. temporal and spatial reasoning. We identify three properties of such orders which, when combined, are sufficient to establish NP-hardness of the CSP. This result explains, in a uniform way, many existing hardness results from the literature. More importantly, this result enables us to prove that CSPs of this kind are not solvable in subexponential time unless the exponential-time hypothesis (ETH) fails. We continue by studying constraint languages based on partition schemes but where relations are built using disjunctions instead of unions; such CSPs appear naturally when analysing first-order definable constraint languages. We prove that such CSPs are NP-hard even in very restricted settings and that they are not solvable in subexponential time under the randomised ETH. In certain cases, we can additionally show that they cannot be solved in O(c^n) time for any c >= 0.

Peter Jonsson and Victor Lagerkvist. Why are CSPs Based on Partition Schemes Computationally Hard?. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 43:1-43:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.MFCS.2018.43, author = {Jonsson, Peter and Lagerkvist, Victor}, title = {{Why are CSPs Based on Partition Schemes Computationally Hard?}}, booktitle = {43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)}, pages = {43:1--43:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-086-6}, ISSN = {1868-8969}, year = {2018}, volume = {117}, editor = {Potapov, Igor and Spirakis, Paul and Worrell, James}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.43}, URN = {urn:nbn:de:0030-drops-96257}, doi = {10.4230/LIPIcs.MFCS.2018.43}, annote = {Keywords: Constraint satisfaction problems, infinite domains, partition schemes, lower bounds} }

Document

**Published in:** LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

The inverse satisfiability problem over a set of Boolean relations Gamma (Inv-SAT(Gamma)) is the computational decision problem of, given a set of models R, deciding whether there exists a SAT(Gamma) instance with R as its set of models. This problem is co-NP-complete in general and a dichotomy theorem for finite Γ containing the constant Boolean relations was obtained by Kavvadias and Sideri. In this paper we remove the latter condition and prove that Inv-SAT(Gamma) is always either tractable or co-NP-complete for all finite sets of relations Gamma, thus solving a problem open since 1998. Very little of the techniques used by Kavvadias and Sideri are applicable and we have to turn to more recently developed algebraic approaches based on partial polymorphisms. We also consider the case when Γ is infinite, where the situation differs markedly from the case of SAT. More precisely, we show that there exists infinite Gamma such that Inv-SAT(Gamma) is tractable even though there exists finite Delta is subset of Gamma such that Inv-SAT(Delta) is co-NP-complete.

Victor Lagerkvist and Biman Roy. A Dichotomy Theorem for the Inverse Satisfiability Problem. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 39:1-39:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lagerkvist_et_al:LIPIcs.FSTTCS.2017.39, author = {Lagerkvist, Victor and Roy, Biman}, title = {{A Dichotomy Theorem for the Inverse Satisfiability Problem}}, booktitle = {37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)}, pages = {39:1--39:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-055-2}, ISSN = {1868-8969}, year = {2018}, volume = {93}, editor = {Lokam, Satya and Ramanujam, R.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.39}, URN = {urn:nbn:de:0030-drops-83745}, doi = {10.4230/LIPIcs.FSTTCS.2017.39}, annote = {Keywords: Complexity Theory, Inverse Satisfiability, Clone Theory} }

Document

**Published in:** LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

The exponential-time hypothesis (ETH) states that 3-SAT is not solvable in subexponential time, i.e. not solvable in O(c^n) time for arbitrary c > 1, where n denotes the number of variables. Problems like k-SAT can be viewed as special cases of the constraint satisfaction problem (CSP), which is the problem of determining whether a set of constraints is satisfiable. In this paper we study the worst-case time complexity of NP-complete CSPs. Our main interest is in the CSP problem parameterized by a constraint language Gamma (CSP(Gamma)), and how the choice of Gamma affects the time complexity. It is believed that CSP(Gamma) is either tractable or NP-complete, and the algebraic CSP dichotomy conjecture gives a sharp delineation of these two classes based on algebraic properties of constraint languages. Under this conjecture and the ETH, we first rule out the existence of subexponential algorithms for finite domain NP-complete CSP(Gamma) problems. This result also extends to certain infinite-domain CSPs and structurally restricted CSP(Gamma) problems. We then begin a study of the complexity of NP-complete CSPs where one is allowed to arbitrarily restrict the values of individual variables, which is a very well-studied subclass of CSPs. For such CSPs with finite domain D, we identify a relation SD such that (1) CSP({SD}) is NP-complete and (2) if CSP(Gamma) over D is NP-complete and solvable in O(c^n) time, then CSP({SD}) is solvable in O(c^n) time, too. Hence, the time complexity of CSP({SD}) is a lower bound for all CSPs of this particular kind. We also prove that the complexity of CSP({SD}) is decreasing when |D| increases, unless the ETH is false. This implies, for instance, that for every c>1 there exists a finite-domain Gamma such that CSP(Gamma) is NP complete and solvable in O(c^n) time.

Peter Jonsson, Victor Lagerkvist, and Biman Roy. Time Complexity of Constraint Satisfaction via Universal Algebra. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.MFCS.2017.17, author = {Jonsson, Peter and Lagerkvist, Victor and Roy, Biman}, title = {{Time Complexity of Constraint Satisfaction via Universal Algebra}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {17:1--17:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.17}, URN = {urn:nbn:de:0030-drops-80710}, doi = {10.4230/LIPIcs.MFCS.2017.17}, annote = {Keywords: Clone Theory, Universal Algebra, Constraint Satisfaction Problems} }

Document

**Published in:** LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

The parameterized satisfiability problem over a set of Boolean
relations Gamma (SAT(Gamma)) is the problem of determining
whether a conjunctive formula over Gamma has at least one
model. Due to Schaefer's dichotomy theorem the computational
complexity of SAT(Gamma), modulo polynomial-time reductions, has
been completely determined: SAT(Gamma) is always either tractable
or NP-complete. More recently, the problem of studying the
relationship between the complexity of the NP-complete cases of
SAT(Gamma) with restricted notions of reductions has attracted
attention. For example, Impagliazzo et al. studied the complexity of
k-SAT and proved that the worst-case time complexity increases
infinitely often for larger values of k, unless 3-SAT is solvable in
subexponential time. In a similar line of research Jonsson et al.
studied the complexity of SAT(Gamma) with algebraic tools borrowed
from clone theory and proved that there exists an NP-complete problem
SAT(R^{neq,neq,neq,01}_{1/3}) such that there cannot exist any NP-complete SAT(Gamma) problem with strictly lower worst-case time complexity: the easiest NP-complete SAT(Gamma) problem. In this paper
we are interested in classifying the NP-complete SAT(Gamma)
problems whose worst-case time complexity is lower than 1-in-3-SAT but
higher than the easiest problem SAT(R^{neq,neq,neq,01}_{1/3}). Recently it was conjectured that there only exists three satisfiability problems of this form. We prove that this conjecture does not hold and that there is an infinite number of such SAT(Gamma) problems. In the process we determine several algebraic properties of 1-in-3-SAT and related problems, which could be of independent interest for constructing exponential-time algorithms.

Victor Lagerkvist and Biman Roy. A Preliminary Investigation of Satisfiability Problems Not Harder than 1-in-3-SAT. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 64:1-64:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{lagerkvist_et_al:LIPIcs.MFCS.2016.64, author = {Lagerkvist, Victor and Roy, Biman}, title = {{A Preliminary Investigation of Satisfiability Problems Not Harder than 1-in-3-SAT}}, booktitle = {41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)}, pages = {64:1--64:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-016-3}, ISSN = {1868-8969}, year = {2016}, volume = {58}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.64}, URN = {urn:nbn:de:0030-drops-64769}, doi = {10.4230/LIPIcs.MFCS.2016.64}, annote = {Keywords: clone theory, universal algebra, satisfiability problems} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail