Showing 1–11 of 11 results for author: Slivovsky, F

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

Authors: Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider

Abstract: Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable orde… ▽ More Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable order is chosen at random. We obtain this result by proving that these formulas, which are known to be Tseitin formulas, have Tseitin graphs of linear treewidth with high probability. Since such Tseitin formulas require exponential resolution proofs, our result follows. We generalize this argument to a new class of formulas that capture a basic form of parity reasoning involving a sum of two random parity constraints with random orders. Even when the variable order for the sum is chosen favorably, these formulas remain hard for resolution. In contrast, we prove that they have short DRAT refutations. We show experimentally that the running time of CDCL SAT solvers on both classes of formulas grows exponentially with their treewidth. △ Less

Submitted 1 February, 2024; originally announced February 2024.

Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF

Authors: Johannes K. Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak

Abstract: The QSAT problem, which asks to evaluate a quantified Boolean formula (QBF), is of fundamental interest in approximation, counting, decision, and probabilistic complexity and is also considered the prototypical PSPACEcomplete problem. As such, it has previously been studied under various structural restrictions (parameters), most notably parameterizations of the primal graph representation of inst… ▽ More The QSAT problem, which asks to evaluate a quantified Boolean formula (QBF), is of fundamental interest in approximation, counting, decision, and probabilistic complexity and is also considered the prototypical PSPACEcomplete problem. As such, it has previously been studied under various structural restrictions (parameters), most notably parameterizations of the primal graph representation of instances. Indeed, it is known that QSAT remains PSPACE-complete even when restricted to instances with constant treewidth of the primal graph, but the problem admits a double-exponential fixed-parameter algorithm parameterized by the vertex cover number (primal graph). However, prior works have left a gap in our understanding of the complexity of QSAT when viewed from the perspective of other natural representations of instances, most notably via incidence graphs. In this paper, we develop structure-aware reductions which allow us to obtain essentially tight lower bounds for highly restricted instances of QSAT, including instances whose incidence graphs have bounded treedepth or feedback vertex number. We complement these lower bounds with novel algorithms for QSAT which establish a nearly-complete picture of the problem's complexity under standard graph-theoretic parameterizations. We also show implications for other natural graph representations, and obtain novel upper as well as lower bounds for QSAT under more fine-grained parameterizations of the primal graph. △ Less

Submitted 26 April, 2023; originally announced April 2023.

Towards Uniform Certification in QBF

Authors: Leroy Chew, Friedrich Slivovsky

Abstract: We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction i… ▽ More We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction into simulation and combining it with new local strategy extraction arguments. This approach leads to simulations that are carried out mainly in propositional logic, with minimal use of the QBF rules. Our proofs therefore provide a new, largely propositional interpretation of the simulated systems. We argue that these results strengthen the case for uniform certification in QBF solving, since many QBF proof systems now fall into place underneath extended QBF Frege. △ Less

Submitted 12 February, 2024; v1 submitted 13 October, 2022; originally announced October 2022.

Journal ref: Logical Methods in Computer Science (February 13, 2024) lmcs:10146

Engineering an Efficient Boolean Functional Synthesis Engine

Authors: Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel

Abstract: Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state-of-the-art approach combines machine learning and automated reas… ▽ More Given a Boolean specification between a set of inputs and outputs, the problem of Boolean functional synthesis is to synthesise each output as a function of inputs such that the specification is met. Although the past few years have witnessed intense algorithmic development, accomplishing scalability remains the holy grail. The state-of-the-art approach combines machine learning and automated reasoning to efficiently synthesise Boolean functions. In this paper, we propose four algorithmic improvements for a data-driven framework for functional synthesis: using a dependency-driven multi-classifier to learn candidate function, extracting uniquely defined functions by interpolation, variables retention, and using lexicographic MaxSAT to repair candidates. We implement these improvements in the state-of-the-art framework, called Manthan. The proposed framework is called Manthan2. Manthan2 shows significantly improved runtime performance compared to Manthan. In an extensive experimental evaluation on 609 benchmarks, Manthan2 is able to synthesise a Boolean function vector for 509 instances compared to 356 instances solved by Manthan--- an increment of 153 instances over the state-of-the-art. To put this into perspective, Manthan improved on the prior state-of-the-art by only 76 instances. △ Less

Submitted 12 August, 2021; originally announced August 2021.

Comments: To be published in 40th International Conference On Computer Aided Design (ICCAD-2021)

Certified DQBF Solving by Definition Extraction

Authors: Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider

Abstract: We propose a new decision procedure for dependency quantified Boolean formulas (DQBF) that uses interpolation-based definition extraction to compute Skolem functions in a counter-example guided inductive synthesis (CEGIS) loop. In each iteration, a family of candidate Skolem functions is tested for correctness using a SAT solver, which either determines that a model has been found, or returns an a… ▽ More We propose a new decision procedure for dependency quantified Boolean formulas (DQBF) that uses interpolation-based definition extraction to compute Skolem functions in a counter-example guided inductive synthesis (CEGIS) loop. In each iteration, a family of candidate Skolem functions is tested for correctness using a SAT solver, which either determines that a model has been found, or returns an assignment of the universal variables as a counterexample. Fixing a counterexample generally involves changing candidates of multiple existential variables with incomparable dependency sets. Our procedure introduces auxiliary variables -- which we call arbiter variables -- that each represent the value of an existential variable for a particular assignment of its dependency set. Possible repairs are expressed as clauses on these variables, and a SAT solver is invoked to find an assignment that deals with all previously seen counterexamples. Adding arbiter variables defines the values of Skolem functions for assignments where they were previously undefined, and may lead to the detection of Skolem functions by definition extraction in subsequent iterations. A key feature of the proposed procedure is that it is certifying by design: for true DQBF, models can be returned at minimal overhead. Towards certification of false formulas, we prove that clauses can be derived in an expansion-based proof system for DQBF. In an experimental evaluation on standard benchmark sets, an implementation was able to match (and in some cases, surpass) the performance of state-of-the-art DQBF solvers. Moreover, models could be generated and validated for all true instances that were solved. △ Less

Submitted 4 June, 2021; originally announced June 2021.

Proof Complexity of Symbolic QBF Reasoning

Authors: Stefan Mengel, Friedrich Slivovsky

Abstract: We introduce and investigate symbolic proof systems for Quantified Boolean Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These systems capture QBF solvers that perform symbolic quantifier elimination, and as such admit short proofs of formulas of bounded path-width and quantifier complexity. As a consequence, we obtain exponential separations from standard clausal proof sys… ▽ More We introduce and investigate symbolic proof systems for Quantified Boolean Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These systems capture QBF solvers that perform symbolic quantifier elimination, and as such admit short proofs of formulas of bounded path-width and quantifier complexity. As a consequence, we obtain exponential separations from standard clausal proof systems, specifically (long-distance) QU-Resolution and IR-Calc. We further develop a lower bound technique for symbolic QBF proof systems based on strategy extraction that lifts known lower bounds from communication complexity. This allows us to derive strong lower bounds against symbolic QBF proof systems that are independent of the variable ordering of the underlying OBDDs, and that hold even if the proof system is allowed access to an NP-oracle. △ Less

Submitted 6 April, 2021; originally announced April 2021.

On Compiling Structured CNFs to OBDDs

Authors: Simone Bova, Friedrich Slivovsky

Abstract: We present new results on the size of OBDD representations of structurally characterized classes of CNF formulas. First, we identify a natural sufficient condition, which we call the few subterms property, for a class of CNFs to have polynomial OBDD size; we then prove that CNFs whose incidence graphs are variable convex have few subterms (and hence have polynomial OBDD size), and observe that the… ▽ More We present new results on the size of OBDD representations of structurally characterized classes of CNF formulas. First, we identify a natural sufficient condition, which we call the few subterms property, for a class of CNFs to have polynomial OBDD size; we then prove that CNFs whose incidence graphs are variable convex have few subterms (and hence have polynomial OBDD size), and observe that the few subterms property also explains the known fact that classes of CNFs of bounded treewidth have polynomial OBDD size. Second, we prove an exponential lower bound on the OBDD size of a family of CNF classes with incidence graphs of bounded degree, exploiting the combinatorial properties of expander graphs. △ Less

Submitted 20 November, 2014; originally announced November 2014.

A Strongly Exponential Separation of DNNFs from CNF Formulas

Authors: Simone Bova, Florent Capelli, Stefan Mengel, Friedrich Slivovsky

Abstract: Decomposable Negation Normal Forms (DNNFs) are Boolean circuits in negation normal form where the subcircuits leading into each AND gate are defined on disjoint sets of variables. We prove a strongly exponential lower bound on the size of DNNFs for a class of CNF formulas built from expander graphs. As a corollary, we obtain a strongly exponential separation between DNNFs and CNF formulas in prime… ▽ More Decomposable Negation Normal Forms (DNNFs) are Boolean circuits in negation normal form where the subcircuits leading into each AND gate are defined on disjoint sets of variables. We prove a strongly exponential lower bound on the size of DNNFs for a class of CNF formulas built from expander graphs. As a corollary, we obtain a strongly exponential separation between DNNFs and CNF formulas in prime implicates form. This settles an open problem in the area of knowledge compilation (Darwiche and Marquis, 2002). △ Less

Submitted 19 February, 2015; v1 submitted 7 November, 2014; originally announced November 2014.

Model Counting for Formulas of Bounded Clique-Width

Authors: Friedrich Slivovsky, Stefan Szeider

Abstract: We show that #SAT is polynomial-time tractable for classes of CNF formulas whose incidence graphs have bounded symmetric clique-width (or bounded clique-width, or bounded rank-width). This result strictly generalizes polynomial-time tractability results for classes of formulas with signed incidence graphs of bounded clique-width and classes of formulas with incidence graphs of bounded modular tree… ▽ More We show that #SAT is polynomial-time tractable for classes of CNF formulas whose incidence graphs have bounded symmetric clique-width (or bounded clique-width, or bounded rank-width). This result strictly generalizes polynomial-time tractability results for classes of formulas with signed incidence graphs of bounded clique-width and classes of formulas with incidence graphs of bounded modular treewidth, which were the most general results of this kind known so far. △ Less

Submitted 30 September, 2014; originally announced September 2014.

Comments: Extended version of a paper published at ISAAC 2013

Journal ref: Proceedings of ISAAC 2013. Lecture Notes in Computer Science, vol. 8283, pp. 677-687, Springer, 2013

Meta-Kernelization with Structural Parameters

Authors: Robert Ganian, Friedrich Slivovsky, Stefan Szeider

Abstract: Meta-kernelization theorems are general results that provide polynomial kernels for large classes of parameterized problems. The known meta-kernelization theorems, in particular the results of Bodlaender et al. (FOCS'09) and of Fomin et al. (FOCS'10), apply to optimization problems parameterized by solution size. We present the first meta-kernelization theorems that use a structural parameters of… ▽ More Meta-kernelization theorems are general results that provide polynomial kernels for large classes of parameterized problems. The known meta-kernelization theorems, in particular the results of Bodlaender et al. (FOCS'09) and of Fomin et al. (FOCS'10), apply to optimization problems parameterized by solution size. We present the first meta-kernelization theorems that use a structural parameters of the input and not the solution size. Let C be a graph class. We define the C-cover number of a graph to be a the smallest number of modules the vertex set can be partitioned into, such that each module induces a subgraph that belongs to the class C. We show that each graph problem that can be expressed in Monadic Second Order (MSO) logic has a polynomial kernel with a linear number of vertices when parameterized by the C-cover number for any fixed class C of bounded rank-width (or equivalently, of bounded clique-width, or bounded Boolean width). Many graph problems such as Independent Dominating Set, c-Coloring, and c-Domatic Number are covered by this meta-kernelization result. Our second result applies to MSO expressible optimization problems, such as Minimum Vertex Cover, Minimum Dominating Set, and Maximum Clique. We show that these problems admit a polynomial annotated kernel with a linear number of vertices. △ Less

Submitted 19 April, 2013; v1 submitted 7 March, 2013; originally announced March 2013.

Computing Resolution-Path Dependencies in Linear Time

Authors: Friedrich Slivovsky, Stefan Szeider

Abstract: The alternation of existential and universal quantifiers in a quantified boolean formula (QBF) generates dependencies among variables that must be respected when evaluating the formula. Dependency schemes provide a general framework for representing such dependencies. Since it is generally intractable to determine dependencies exactly, a set of potential dependencies is computed instead, which may… ▽ More The alternation of existential and universal quantifiers in a quantified boolean formula (QBF) generates dependencies among variables that must be respected when evaluating the formula. Dependency schemes provide a general framework for representing such dependencies. Since it is generally intractable to determine dependencies exactly, a set of potential dependencies is computed instead, which may include false positives. Among the schemes proposed so far, resolution-path dependencies introduce the fewest spurious dependencies. In this work, we describe an algorithm that detects resolution-path dependencies in linear time, resolving a problem posed by Van Gelder (CP 2011). △ Less

Submitted 5 May, 2012; v1 submitted 14 February, 2012; originally announced February 2012.

Comments: 14 pages, SAT 2012