LIVIVO - The Search Portal for Life Sciences

zur deutschen Oberfläche wechseln
Advanced search

Search results

Result 1 - 10 of total 11

Search options

  1. Article ; Online: Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing

    Slivovsky, Friedrich

    Computer Aided Verification

    Abstract: We present a new semantic gate extraction technique for propositional formulas based on interpolation. While known gate detection methods are incomplete and rely on pattern matching or simple semantic conditions, this approach can detect any definition ... ...

    Abstract We present a new semantic gate extraction technique for propositional formulas based on interpolation. While known gate detection methods are incomplete and rely on pattern matching or simple semantic conditions, this approach can detect any definition entailed by an input formula. As an application, we consider the problem of computing unique strategy functions from Quantified Boolean Formulas (QBFs) and Dependency Quantified Boolean Formulas (DQBFs). Experiments with a prototype implementation demonstrate that functions can be efficiently extracted from formulas in standard benchmark sets, and that many of these definitions remain undetected by syntactic gate detection. We turn this into a preprocessing technique by substituting unique strategy functions for input variables and test solver performance on the resulting instances. Compared to syntactic gate detection, we see a significant increase in the number of solved QBF instances, as well as a modest increase for DQBF instances.
    Keywords covid19
    Publisher PMC
    Document type Article ; Online
    DOI 10.1007/978-3-030-53288-8_24
    Database COVID19

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  2. Book ; Online: Towards Uniform Certification in QBF

    Chew, Leroy / Slivovsky, Friedrich

    2022  

    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- ... ...

    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 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.
    Keywords Computer Science - Logic in Computer Science ; Computer Science - Computational Complexity
    Publishing date 2022-10-13
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  3. Book ; Online: Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

    Chew, Leroy / de Colnet, Alexis / Slivovsky, Friedrich / Szeider, Stefan

    2024  

    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 ... ...

    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 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.
    Keywords Computer Science - Computational Complexity
    Subject code 004
    Publishing date 2024-02-01
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  4. Book ; Online: Proof Complexity of Symbolic QBF Reasoning

    Mengel, Stefan / Slivovsky, Friedrich

    2021  

    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 ... ...

    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 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.
    Keywords Computer Science - Computational Complexity ; Computer Science - Artificial Intelligence ; Computer Science - Logic in Computer Science
    Publishing date 2021-04-06
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  5. Article ; Online: A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth

    Slivovsky, Friedrich / Szeider, Stefan

    Theory and Applications of Satisfiability Testing - SAT 2020

    Abstract: The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the ... ...

    Abstract The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the exponential factor of [Formula: see text]. We improve this factor to [Formula: see text] by utilizing fast algorithms for computing the zeta transform and covering product of functions representing partial model counts, thereby achieving the same running time as FPT algorithms that are parameterized by the less general treewidth of the primal graph. Our new algorithm is asymptotically optimal unless the Strong Exponential Time Hypothesis (SETH) fails.
    Keywords covid19
    Publisher PMC
    Document type Article ; Online
    DOI 10.1007/978-3-030-51825-7_19
    Database COVID19

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  6. Book ; Online: Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF

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

    2023  

    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 ... ...

    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 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.
    Keywords Computer Science - Logic in Computer Science ; Computer Science - Computational Complexity ; Computer Science - Data Structures and Algorithms ; Mathematics - Logic
    Subject code 511
    Publishing date 2023-04-26
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  7. Article: On Compiling Structured CNFs to OBDDs.

    Bova, Simone / Slivovsky, Friedrich

    Theory of computing systems

    2016  Volume 61, Issue 2, Page(s) 637–655

    Abstract: We present new results on the size of OBDD representations of structurally characterized classes of CNF formulas. First, we prove ... ...

    Abstract We present new results on the size of OBDD representations of structurally characterized classes of CNF formulas. First, we prove that
    Language English
    Publishing date 2016-10-26
    Publishing country United States
    Document type Journal Article
    ZDB-ID 1463181-7
    ISSN 1433-0490 ; 1432-4350
    ISSN (online) 1433-0490
    ISSN 1432-4350
    DOI 10.1007/s00224-016-9715-z
    Database MEDical Literature Analysis and Retrieval System OnLINE

    Full text online

    More links

    Kategorien

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

  8. Article ; Online: Long-Distance Q-Resolution with Dependency Schemes.

    Peitl, Tomáš / Slivovsky, Friedrich / Szeider, Stefan

    Journal of automated reasoning

    2018  Volume 63, Issue 1, Page(s) 127–155

    Abstract: Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers that use these systems to generate proofs. We study a combination of two proof systems ... ...

    Abstract Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers that use these systems to generate proofs. We study a combination of two proof systems supported by the solver DepQBF: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system-which we call long-distance Q(D)-resolution-is sound for the reflexive resolution-path dependency scheme. In fact, we prove that it admits strategy extraction in polynomial time. This comes as an application of a general result, by which we identify a whole class of dependency schemes for which long-distance Q(D)-resolution admits polynomial-time strategy extraction. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q(D)-resolution with the standard dependency scheme. We further show that search-based QBF solvers using a dependency scheme D and learning with long-distance Q-resolution generate long-distance Q(D)-resolution proofs. The above soundness results thus translate to partial soundness results for such solvers: they declare an input QBF to be false only if it is indeed false. Finally, we report on experiments with a configuration of DepQBF that uses the standard dependency scheme and learning based on long-distance Q-resolution.
    Language English
    Publishing date 2018-06-09
    Publishing country Netherlands
    Document type Journal Article
    ZDB-ID 1479376-3
    ISSN 1573-0670 ; 0168-7433
    ISSN (online) 1573-0670
    ISSN 0168-7433
    DOI 10.1007/s10817-018-9467-3
    Database MEDical Literature Analysis and Retrieval System OnLINE

    Full text online

    More links

    Kategorien

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

  9. Article ; Online: Short Q-Resolution Proofs with Homomorphisms

    Shukla, Ankit / Slivovsky, Friedrich / Szeider, Stefan

    Theory and Applications of Satisfiability Testing - SAT 2020

    Abstract: We introduce new proof systems for quantified Boolean formulas (QBFs) by enhancing Q-resolution systems with rules which exploit local and global symmetries. The rules are based on homomorphisms that admit non-injective mappings between literals. This ... ...

    Abstract We introduce new proof systems for quantified Boolean formulas (QBFs) by enhancing Q-resolution systems with rules which exploit local and global symmetries. The rules are based on homomorphisms that admit non-injective mappings between literals. This results in systems that are stronger than Q-resolution with (injective) symmetry rules. We further strengthen the systems by utilizing a dependency system D in a way that surpasses Q(D)-resolution in relative strength.
    Keywords covid19
    Publisher PMC
    Document type Article ; Online
    DOI 10.1007/978-3-030-51825-7_29
    Database COVID19

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  10. Article ; Online: Multi-linear Strategy Extraction for QBF Expansion Proofs via Local Soundness

    Schlaipfer, Matthias / Slivovsky, Friedrich / Weissenbacher, Georg / Zuleger, Florian

    Theory and Applications of Satisfiability Testing - SAT 2020

    Abstract: In applications, QBF solvers are expected to not only decide whether a given formula is true or false but also return a solution in the form of a strategy. Determining whether strategies can be efficiently extracted from proof traces generated by QBF ... ...

    Abstract In applications, QBF solvers are expected to not only decide whether a given formula is true or false but also return a solution in the form of a strategy. Determining whether strategies can be efficiently extracted from proof traces generated by QBF solvers is a fundamental research task. Most resolution-based proof systems are known to implicitly support polynomial-time strategy extraction through a simulation of the evaluation game associated with an input formula, but this approach introduces large constant factors and results in unwieldy circuit representations. In this work, we present an explicit polynomial-time strategy extraction algorithm for the [Formula: see text] proof system. This system is used by expansion-based solvers that implement counterexample-guided abstraction refinement (CEGAR), currently one of the most effective QBF solving paradigms. Our argument relies on a Curry-Howard style correspondence between strategies and [Formula: see text] derivations, where each strategy realizes an invariant obtained from an annotated clause derived in the proof system.
    Keywords covid19
    Publisher PMC
    Document type Article ; Online
    DOI 10.1007/978-3-030-51825-7_30
    Database COVID19

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

To top