Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTractable Combinations of Temporal CSPs
159
0
0.0
(
0
)
Added by
Johannes Greiner
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The constraint satisfaction problem (CSP) of a first-order theory $T$ is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of $T$. We study the computational complexity of $mathrm{CSP}(T_1 cup T_2)$ where $T_1$ and $T_2$ are theories with disjoint finite relational signatures. We prove that if $T_1$ and $T_2$ are the theories of temporal structures, i.e., structures where all relations have a first-order definition in $(mathbb{Q};<)$, then $mathrm{CSP}(T_1 cup T_2)$ is in P or NP-complete. To this end we prove a purely algebraic statement about the structure of the lattice of locally closed clones over the domain ${mathbb Q}$ that contain $mathrm{Aut}(mathbb{Q};<)$.
rate research
Read More
For a first-order theory $T$, the Constraint Satisfaction Problem of $T$ is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of $T$. In this article we develop sufficient conditions for polynomial-time tractability of the constraint satisfaction problem for the union of two theories with disjoint relational signatures. To this end, we introduce the concept of sampling for theories and show that samplings can be applied to examples which are not covered by the seminal result of Nelson and Oppen.
In the field of constraint satisfaction problems (CSP), promise CSPs are an exciting new direction of study. In a promise CSP, each constraint comes in two forms: strict and weak, and in the associated decision problem one must distinguish between being able to satisfy all the strict constraints versus not being able to satisfy all the weak constraints. The most commonly cited example of a promise CSP is the approximate graph coloring problem--which has recently seen exciting progress [BKO19, WZ20] benefiting from a systematic algebraic approach to promise CSPs based on polymorphisms, operations that map tuples in the strict form of each constraint to tuples in the corresponding weak form. In this work, we present a simple algorithm which in polynomial time solves the decision problem for all promise CSPs that admit infinitely many symmetric polymorphisms, which are invariant under arbitrary coordinate permutations. This generalizes previous work of the first two authors [BG19]. We also extend this algorithm to a more general class of block-symmetric polymorphisms. As a corollary, this single algorithm solves all polynomial-time tractable Boolean CSPs simultaneously. These results give a new perspective on Schaefers classic dichotomy theorem and shed further light on how symmetries of polymorphisms enable algorithms. Finally, we show that block symmetric polymorphisms are not only sufficient but also necessary for this algorithm to work, thus establishing its precise power
For formulas F of propositional calculus I introduce a metavariable MF and show how it can be used to define an algorithm for testing satisfiability. MF is a formula which is true/false under all possible truth assignments iff F is satisfiable/unsatisfiable. In this sense MF is a metavariable with the meaning F is SAT. For constructing MF a group of transformations of the basic variables ai is used which corresponds to flipping literals to their negation. The whole procedure corresponds to branching algorithms where a formula is split with respect to the truth values of its variables, one by one. Each branching step corresponds to an approximation to the metatheorem which doubles the chance to find a satisfying truth assignment but also doubles the length of the formulas to be tested, in principle. Simplifications arise by additional length reductions. I also discuss the notion of logical primes and show that each formula can be written as a uniquely defined product of such prime factors. Satisfying truth assignments can be found by determining the missing primes in the factorization of a formula.
This note introduces a generalization to the setting of infinite-time computation of the busy beaver problem from classical computability theory, and proves some results concerning the growth rate of an associated function. In our view, these results indicate that the generalization is both natural and promising.
Robin Hirsch posed in 1996 the Really Big Complexity Problem: classify the computational complexity of the network satisfaction problem for all finite relation algebras $bf A$. We provide a complete classification for the case that $bf A$ is symmetric and has a flexible atom; the problem is in this case NP-complete or in P. If a finite integral relation algebra has a flexible atom, then it has a normal representation $mathfrak{B}$. We can then study the computational complexity of the network satisfaction problem of ${bf A}$ using the universal-algebraic approach, via an analysis of the polymorphisms of $mathfrak{B}$. We also use a Ramsey-type result of Nev{s}etv{r}il and Rodl and a complexity dichotomy result of Bulatov for conservative finite-domain constraint satisfaction problems.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
