We focus on incremental compilation-to-SAT procedures (iCTS), a promising way to push the standard CTS approaches beyond their limits. We propose the first comprehensive framework...
Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translating to CNF. The best known example of this feature is probably pro...
Kolaitis and Vardi pointed out that constraint satisfaction and conjunctive query containment are essentially the same problem. We study the Boolean conjunctive queries under a mor...
Michael Bauland, Philippe Chapdelaine, Nadia Creig...
Abstract. Many problems are naturally expressed using CNF clauses and boolean cardinality constraints. It is generally believed that solving such problems through pure CNF encoding...
The problem of solving boolean combinations of difference constraints is at the core of many important techniques such as planning, scheduling, and model-checking of real-time syst...
Abstract. During the recent years, the development of tools for deciding Quantified Boolean Formulas (QBFs) has been accompanied by a steady supply of real-world instances, i.e., ...
We define a collection of mappings that transform many-valued clausal forms into satisfiability equivalent Boolean clausal forms, analyze their complexity and evaluate them empir...
We study the parameterized complexity of detecting backdoor sets for instances of the propositional satisfiability problem (SAT) with respect to the polynomially solvable classes ...