Perfect Matching in Random Graphs is as Hard as Tseitin [PDF]
We study the complexity of proving that a sparse random regular graph on an odd number of vertices does not have a perfect matching, and related problems involving each vertex being matched some pre-specified number of times.
Per Austrin, Kilian Risse
doaj +1 more source
Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy [PDF]
We introduce a generalization of the bisimulation game that finds distinguishing Hennessy-Milner logic formulas from every finitary, subformula-closed language in van Glabbeek's linear-time--branching-time spectrum between two finite-state processes.
Benjamin Bisping +2 more
doaj +1 more source
Small Promise CSPs that reduce to large CSPs [PDF]
For relational structures A, B of the same signature, the Promise Constraint Satisfaction Problem PCSP(A,B) asks whether a given input structure maps homomorphically to A or does not even map to B.
Alexandr Kazda, Peter Mayr, Dmitriy Zhuk
doaj +1 more source
Tractable Combinations of Temporal CSPs [PDF]
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.
Manuel Bodirsky +2 more
doaj +1 more source
Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity [PDF]
This paper settles the computational complexity of model checking of several extensions of the monadic second order (MSO) logic on two classes of graphs: graphs of bounded treewidth and graphs of bounded neighborhood diversity.
Dušan Knop +3 more
doaj +1 more source
Complexity classifications for different equivalence and audit problems for Boolean circuits [PDF]
We study Boolean circuits as a representation of Boolean functions and consider different equivalence, audit, and enumeration problems. For a number of restricted sets of gate types (bases) we obtain efficient algorithms, while for all other gate types ...
Elmar Böhler +5 more
doaj +1 more source
The Complexity of Combinations of Qualitative Constraint Satisfaction Problems [PDF]
The CSP of a first-order theory $T$ is the problem of deciding for a given finite set $S$ of atomic formulas whether $T \cup S$ is satisfiable. Let $T_1$ and $T_2$ be two theories with countably infinite models and disjoint signatures.
Manuel Bodirsky, Johannes Greiner
doaj +1 more source
On the Monadic Second-Order Transduction Hierarchy [PDF]
We compare classes of finite relational structures via monadic second-order transductions. More precisely, we study the preorder where we set C \subseteq K if, and only if, there exists a transduction {\tau} such that C\subseteq{\tau}(K).
Achim Blumensath, Bruno Courcelle
doaj +1 more source
Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds [PDF]
Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path checking can be
Lars Kuhtz, Bernd Finkbeiner
doaj +1 more source
The complexity of linear-time temporal logic over the class of ordinals [PDF]
We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem.
Stephane Demri, Alexander Rabinovich
doaj +1 more source

