Search results for "satisfiability"
showing 10 items of 34 documents
Efficient CNF Encoding of Boolean Cardinality Constraints
2003
In this paper, we address the encoding into CNF clauses of Boolean cardinality constraints that arise in many practical applications. The proposed encoding is efficient with respect to unit propagation, which is implemented in almost all complete CNF satisfiability solvers. We prove the practical efficiency of this encoding on some problems arising in discrete tomography that involve many cardinality constraints. This encoding is also used together with a trivial variable elimination in order to re-encode parity learning benchmarks so that a simple Davis and Putnam procedure can solve them.
On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards
2007
The guarded fragment of first-order logic, GF, enjoys the finite model property, so the satisfiability and the finite satisfiability problems coincide. We are concerned with two extensions of the two-variable guarded fragment that do not possess the finite model property, namely, GF2 with equivalence and GF2 with transitive guards. We prove that in both cases every finitely satisfiable formula has a model of at most double exponential size w.r.t. its length. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NEXPTIME-upper bound on the complexity of the fini…
Topological Logics with Connectedness over Euclidean Spaces
2013
We consider the quantifier-free languages, Bc and Bc °, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of R n ( n ≥ 2) and, additionally, over the regular closed semilinear sets of R n . The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric Qualitative Spatial Reasoning. We prove that the satisfiability problem for Bc is undecidable over the regular closed semilinear sets in all dimensions greater than 1,…
Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting
2017
The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.
The fluted fragment with transitive relations
2022
Abstract The fluted fragment is a fragment of first-order logic (without equality) in which, roughly speaking, the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that this fragment has the finite model property. We consider extensions of the fluted fragment with various numbers of transitive relations, as well as the equality predicate. In the presence of one transitive relation (together with equality), the finite model property is lost; nevertheless, we show that the satisfiability and finite satisfiability problems for this extension remain decidable. We also show that the corresponding problems in the…
Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants
2018
We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NExpTime-upper bou…
The Fluted Fragment with Transitivity
2019
We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.
Exact quantum algorithms have advantage for almost all Boolean functions
2014
It has been proved that almost all $n$-bit Boolean functions have exact classical query complexity $n$. However, the situation seemed to be very different when we deal with exact quantum query complexity. In this paper, we prove that almost all $n$-bit Boolean functions can be computed by an exact quantum algorithm with less than $n$ queries. More exactly, we prove that ${AND}_n$ is the only $n$-bit Boolean function, up to isomorphism, that requires $n$ queries.
Classical and Quantum Annealing in the Median of Three Satisfiability
2011
We determine the classical and quantum complexities of a specific ensemble of three-satisfiability problems with a unique satisfying assignment for up to N = 100 and 80 variables, respectively. In the classical limit, we employ generalized ensemble techniques and measure the time that a Markovian Monte Carlo process spends in searching classical ground states. In the quantum limit, we determine the maximum finite correlation length along a quantum adiabatic trajectory determined by the linear sweep of the adiabatic control parameter in the Hamiltonian composed of the problem Hamiltonian and the constant transverse field Hamiltonian. In the median of our ensemble, both complexities diverge e…
Decidability Frontier for Fragments of First-Order Logic with Transitivity
2018
Several decidable fragments of first-order logic have been identified in the past as a generalisation of the standard translation of modal logic. These include: the fluted fragment, the two-variable frag- ment, the guarded fragment and the unary negation fragment; some of them have been recently generalised or combined to yield even more expressive decidable logics (guarded negation fragment or uniform one- dimensional fragment). None of the fragments allows one to express tran- sitivity of a binary relation or related properties like being an equivalence, a linear or a partial order, that naturally appear in specifications or in verification. The question therefore arises what is the impac…