Overview
- 45 archival publications between 2008 and 2023, among them two book chapters and 43 peer-reviewed publications:
- 32 papers in conference proceedings
- 8 journal papers
- 3 papers in workshop proceedings
- 20+ papers published in the proceedings of top tier conferences (CORE ranking A* or A).
- 13 papers published between 2008 and 2019 in the proceedings of the Conference on Theory and Applications of Satisfiability Solving (SAT), the primary venue for satisfiability-related research.
- Google Scholar profile
- DBLP listing
2023
Chattopadhyay, Saranyu; Devarajegowda, Keerthikumara; Zhao, Bihan; Lonsing, Florian; D'Agostino, Brandon A.; Vavelidou, Ioanna; Bhatt, Vijay Deep; Prebeck, Sebastian; Ecker, Wolfgang; Trippel, Caroline; Barrett, Clark W.; Mitra, Subhasish
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators Proceedings Article
In: 60th ACM/IEEE Design Automation Conference, DAC 2023, San Francisco, CA, USA, July 9-13, 2023, pp. 1–6, IEEE, 2023.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/dac/ChattopadhyayDZLDVBPETBM23,
title = {G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators},
author = {Saranyu Chattopadhyay and Keerthikumara Devarajegowda and Bihan Zhao and Florian Lonsing and Brandon A. D'Agostino and Ioanna Vavelidou and Vijay Deep Bhatt and Sebastian Prebeck and Wolfgang Ecker and Caroline Trippel and Clark W. Barrett and Subhasish Mitra},
url = {https://doi.org/10.1109/DAC56929.2023.10247903},
doi = {10.1109/DAC56929.2023.10247903},
year = {2023},
date = {2023-01-01},
urldate = {2023-01-01},
booktitle = {60th ACM/IEEE Design Automation Conference, DAC 2023, San Francisco,
CA, USA, July 9-13, 2023},
pages = {1–6},
publisher = {IEEE},
abstract = {Hardware accelerators (HAs) underpin high-performance and energy-efficient digital systems. Correctness of these systems thus depends on the correctness of constituent HAs. Self-consistency-based pre-silicon verification techniques, like A-QED (Accelerator Quick Error Detection), provide a quick and provably thorough HA verification framework that does not require extensive design-specific properties or a full functional specification. However, A-QED is limited to verifying HAs which are non-interfering – i.e., they produce the same result for a given input independent of its context within a sequence of inputs. We present a new technique called G-QED (Generalized QED) which goes beyond non-interfering HAs while retaining A-QED’s benefits. Our extensive results as well as a detailed industrial case study show that: G-QED is highly thorough in detecting critical bugs in well-verified designs that otherwise escape traditional verification flows while simultaneously improving verification productivity 18-fold (from 370 person days to 21 person days). These results are backed by theoretical guarantees of soundness and completeness.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Hardware accelerators (HAs) underpin high-performance and energy-efficient digital systems. Correctness of these systems thus depends on the correctness of constituent HAs. Self-consistency-based pre-silicon verification techniques, like A-QED (Accelerator Quick Error Detection), provide a quick and provably thorough HA verification framework that does not require extensive design-specific properties or a full functional specification. However, A-QED is limited to verifying HAs which are non-interfering – i.e., they produce the same result for a given input independent of its context within a sequence of inputs. We present a new technique called G-QED (Generalized QED) which goes beyond non-interfering HAs while retaining A-QED’s benefits. Our extensive results as well as a detailed industrial case study show that: G-QED is highly thorough in detecting critical bugs in well-verified designs that otherwise escape traditional verification flows while simultaneously improving verification productivity 18-fold (from 370 person days to 21 person days). These results are backed by theoretical guarantees of soundness and completeness.
Wu, Haoze; Hahn, Christopher; Lonsing, Florian; Mann, Makai; Ramanujan, Raghuram; Barrett, Clark W.
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning Proceedings Article
In: Nadel, Alexander; Rozier, Kristin Yvonne (Ed.): Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, pp. 1–11, IEEE, 2023.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/fmcad/WuHLMRB23,
title = {Lightweight Online Learning for Sets of Related Problems in Automated Reasoning},
author = {Haoze Wu and Christopher Hahn and Florian Lonsing and Makai Mann and Raghuram Ramanujan and Clark W. Barrett},
editor = {Alexander Nadel and Kristin Yvonne Rozier},
url = {https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_10
https://arxiv.org/abs/2305.11087},
doi = {10.34727/2023/ISBN.978-3-85448-060-0_10},
year = {2023},
date = {2023-01-01},
urldate = {2023-01-01},
booktitle = {Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA,
October 24-27, 2023},
pages = {1–11},
publisher = {IEEE},
abstract = {We present Self-Driven Strategy Learning (SDSL), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. SDSL does not require offline training, but instead automatically constructs a dataset while solving earlier problems. It fits a machine learning model to this data which is then used to adjust the solving strategy for later problems. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the SDSL calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the KISSAT solver and show that the combination of KISSAT+SDSL certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present Self-Driven Strategy Learning (SDSL), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. SDSL does not require offline training, but instead automatically constructs a dataset while solving earlier problems. It fits a machine learning model to this data which is then used to adjust the solving strategy for later problems. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the SDSL calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the KISSAT solver and show that the combination of KISSAT+SDSL certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.
2021
Beyersdorff, Olaf; Janota, Mikolás; Lonsing, Florian; Seidl, Martina
Quantified Boolean Formulas Book Section
In: Handbook of Satisfiability, IOS Press, 2021.
Abstract | Links | BibTeX | Tags:
@incollection{SATBookChapterQBFProofs,
title = {Quantified Boolean Formulas},
author = {Olaf Beyersdorff and Mikolás Janota and Florian Lonsing and Martina Seidl},
url = {https://www.ti1.uni-jena.de/ti1media/publications/qbf-proofs.pdf
https://ebooks.iospress.nl/doi/10.3233/FAIA201015},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Handbook of Satisfiability},
publisher = {IOS Press},
edition = {2nd},
abstract = {Solvers for quantified Boolean formulas (QBF) have become powerful tools for tackling hard computational problems from various application domains, even beyond the scope of SAT. This chapter gives a description of the main algorithmic paradigms for QBF solving, including quantified conflict driven clause learning (QCDCL), expansion-based solving, dependency schemes, and QBF preprocessing. Particular emphasis is laid on the connections of these solving approaches to QBF proof systems: Q-Resolution and its variants in the case of QCDCL, expansion QBF resolution calculi for expansion-based solving, and QRAT for preprocessing. The chapter also surveys the relations between the various QBF proof systems and results on their proof complexity, thereby shedding light on the diverse performance characteristics of different solving approaches that are observed in practice.},
keywords = {},
pubstate = {published},
tppubtype = {incollection}
}
Solvers for quantified Boolean formulas (QBF) have become powerful tools for tackling hard computational problems from various application domains, even beyond the scope of SAT. This chapter gives a description of the main algorithmic paradigms for QBF solving, including quantified conflict driven clause learning (QCDCL), expansion-based solving, dependency schemes, and QBF preprocessing. Particular emphasis is laid on the connections of these solving approaches to QBF proof systems: Q-Resolution and its variants in the case of QCDCL, expansion QBF resolution calculi for expansion-based solving, and QRAT for preprocessing. The chapter also surveys the relations between the various QBF proof systems and results on their proof complexity, thereby shedding light on the diverse performance characteristics of different solving approaches that are observed in practice.
Mann, Makai; Irfan, Ahmed; Lonsing, Florian; Yang, Yahan; Zhang, Hongce; Brown, Kristopher; Gupta, Aarti; Barrett, Clark W.
Pono: A Flexible and Extensible SMT-Based Model Checker Proceedings Article
In: Silva, Alexandra; Leino, K. Rustan M. (Ed.): Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, pp. 461–474, Springer, 2021.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/cav/MannILYZBGB20,
title = {Pono: A Flexible and Extensible SMT-Based Model Checker},
author = {Makai Mann and Ahmed Irfan and Florian Lonsing and Yahan Yang and Hongce Zhang and Kristopher Brown and Aarti Gupta and Clark W. Barrett},
editor = {Alexandra Silva and K. Rustan M. Leino},
url = {https://doi.org/10.1007/978-3-030-81688-9_22},
doi = {10.1007/978-3-030-81688-9_22},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Computer Aided Verification - 33rd International Conference, CAV
2021, Virtual Event, July 20-23, 2021, Proceedings, Part II},
volume = {12760},
pages = {461–474},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
abstract = {Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present Pono, an open-source SMT-based model checker. Pono is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, Pono prioritizes transparency (developed as an open-source project on GitHub), flexibility (Pono can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers). In this paper, we describe the design of the tool with a focus on the flexible and extensible architecture, cover its current capabilities, and demonstrate that Pono is competitive with state-of-the-art tools.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present Pono, an open-source SMT-based model checker. Pono is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, Pono prioritizes transparency (developed as an open-source project on GitHub), flexibility (Pono can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers). In this paper, we describe the design of the tool with a focus on the flexible and extensible architecture, cover its current capabilities, and demonstrate that Pono is competitive with state-of-the-art tools.
Chattopadhyay, Saranyu; Lonsing, Florian; Piccolboni, Luca; Soni, Deepraj; Wei, Peng; Zhang, Xiaofan; Zhou, Yuan; Carloni, Luca P.; Chen, Deming; Cong, Jason; Karri, Ramesh; Zhang, Zhiru; Trippel, Caroline; Barrett, Clark W.; Mitra, Subhasish
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition Proceedings Article
In: 2021 Formal Methods in Computer Aided Design, FMCAD 2021, online event, pp. 1–10, IEEE, 2021.
Abstract | Links | BibTeX | Tags:
@inproceedings{FMCAD2021accepted,
title = {Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition},
author = {Saranyu Chattopadhyay and Florian Lonsing and Luca Piccolboni and Deepraj Soni and Peng Wei and Xiaofan Zhang and Yuan Zhou and Luca P. Carloni and Deming Chen and Jason Cong and Ramesh Karri and Zhiru Zhang and Caroline Trippel and Clark W. Barrett and Subhasish Mitra},
url = {https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_12},
doi = {10.34727/2021/isbn.978-3-85448-046-4},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {2021 Formal Methods in Computer Aided Design, FMCAD 2021, online event},
pages = {1–10},
publisher = {IEEE},
abstract = {Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique which uses Bounded Model Checking for pre-silicon verification of HAs. A-QED checks an HA for self-consistency, i.e., whether identical inputs within a sequence of operations always produce the same output. Under modest assumptions, A-QED is both sound and complete. However, as is well-known, large design sizes significantly limit the scalability of formal verification, including A-QED. We overcome this scalability challenge through a new decomposition technique for A-QED, called A-QED with Decomposition (A-QED^2). A-QED^2 systematically decomposes an HA into smaller, functional sub-modules, called sub-accelerators, which are then verified independently using A-QED. We prove completeness of A-QED^2; in particular, if the full HA under verification contains a bug, then A-QED2 ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED^2.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique which uses Bounded Model Checking for pre-silicon verification of HAs. A-QED checks an HA for self-consistency, i.e., whether identical inputs within a sequence of operations always produce the same output. Under modest assumptions, A-QED is both sound and complete. However, as is well-known, large design sizes significantly limit the scalability of formal verification, including A-QED. We overcome this scalability challenge through a new decomposition technique for A-QED, called A-QED with Decomposition (A-QED^2). A-QED^2 systematically decomposes an HA into smaller, functional sub-modules, called sub-accelerators, which are then verified independently using A-QED. We prove completeness of A-QED^2; in particular, if the full HA under verification contains a bug, then A-QED2 ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED^2.
Bloem, Roderick; Braud-Santoni, Nicolas; Hadzic, Vedad; Egly, Uwe; Lonsing, Florian; Seidl, Martina
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations Journal Article
In: Formal Methods Syst. Des., vol. 57, no. 2, pp. 157–177, 2021.
Abstract | Links | BibTeX | Tags:
@article{DBLP:journals/fmsd/FMCADQBFextension,
title = {Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations},
author = {Roderick Bloem and Nicolas Braud-Santoni and Vedad Hadzic and Uwe Egly and Florian Lonsing and Martina Seidl},
url = {https://doi.org/10.1007/s10703-021-00371-7},
doi = {10.1007/S10703-021-00371-7},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
journal = {Formal Methods Syst. Des.},
volume = {57},
number = {2},
pages = {157–177},
abstract = {In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) for obtaining a propositional abstraction of the QBF. If this formula is false, the truth value of the QBF is decided, otherwise further refinement steps are necessary. Classically, expansion-based solvers process the given formula quantifier-block wise and use one SAT solver per quantifier block. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided and only two incremental SAT solvers are required. While our algorithm is naturally based on the Exp+Res calculus that is the formal foundation of expansion-based solving, it is conceptually simpler than present recursive approaches. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) for obtaining a propositional abstraction of the QBF. If this formula is false, the truth value of the QBF is decided, otherwise further refinement steps are necessary. Classically, expansion-based solvers process the given formula quantifier-block wise and use one SAT solver per quantifier block. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided and only two incremental SAT solvers are required. While our algorithm is naturally based on the Exp+Res calculus that is the formal foundation of expansion-based solving, it is conceptually simpler than present recursive approaches. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.
Ganesan, Karthik; Lonsing, Florian; Nuthakki, Srinivasa Shashank; Singh, Eshan; Fadiheh, Mohammad Rahmani; Kunz, Wolfgang; Stoffel, Dominik; Barrett, Clark W.; Mitra, Subhasish
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection Technical Report
2021.
Abstract | Links | BibTeX | Tags:
@techreport{DBLP:journals/corr/abs-2106-10392,
title = {Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection},
author = {Karthik Ganesan and Florian Lonsing and Srinivasa Shashank Nuthakki and Eshan Singh and Mohammad Rahmani Fadiheh and Wolfgang Kunz and Dominik Stoffel and Clark W. Barrett and Subhasish Mitra},
url = {https://arxiv.org/abs/2106.10392},
year = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
journal = {CoRR},
volume = {abs/2106.10392},
abstract = {We present a novel approach to pre-silicon verification of processor designs. The purpose of pre-silicon verification is to find logic bugs in a design at an early stage and thus avoid time- and cost-intensive post-silicon debugging. Our approach relies on symbolic quick error detection (Symbolic QED, or SQED). SQED is targeted at finding logic bugs in a symbolic representation of a design by combining bounded model checking (BMC) with QED tests. QED tests are powerful in generating short sequences of instructions (traces) that trigger bugs. We extend an existing SQED approach with symbolic starting states. This way, we enable the BMC tool to select starting states arbitrarily when generating a trace. To avoid false positives, (e.g., traces starting in unreachable states that may not be-have in accordance with the processor instruction-set architecture), we define constraints to restrict the set of possible starting states. We demonstrate that these constraints, together with reasonable assumptions about the system behavior, allow us to avoid false positives. Using our approach, we discovered previously unknown bugs in open-source RISC-V processor cores that existing methods cannot detect. Moreover, our novel approach out-performs existing ones in the detection of bugs having long traces and in the detection of hardware Trojans, i.e., unauthorized modifications of a design.},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
We present a novel approach to pre-silicon verification of processor designs. The purpose of pre-silicon verification is to find logic bugs in a design at an early stage and thus avoid time- and cost-intensive post-silicon debugging. Our approach relies on symbolic quick error detection (Symbolic QED, or SQED). SQED is targeted at finding logic bugs in a symbolic representation of a design by combining bounded model checking (BMC) with QED tests. QED tests are powerful in generating short sequences of instructions (traces) that trigger bugs. We extend an existing SQED approach with symbolic starting states. This way, we enable the BMC tool to select starting states arbitrarily when generating a trace. To avoid false positives, (e.g., traces starting in unreachable states that may not be-have in accordance with the processor instruction-set architecture), we define constraints to restrict the set of possible starting states. We demonstrate that these constraints, together with reasonable assumptions about the system behavior, allow us to avoid false positives. Using our approach, we discovered previously unknown bugs in open-source RISC-V processor cores that existing methods cannot detect. Moreover, our novel approach out-performs existing ones in the detection of bugs having long traces and in the detection of hardware Trojans, i.e., unauthorized modifications of a design.
2020
Lonsing, Florian; Mitra, Subhasish; Barrett, Clark W.
A Theoretical Framework for Symbolic Quick Error Detection Proceedings Article
In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pp. 1–10, IEEE, 2020.
Abstract | Links | BibTeX | Tags:
@inproceedings{FMCAD2020accepted,
title = {A Theoretical Framework for Symbolic Quick Error Detection},
author = {Florian Lonsing and Subhasish Mitra and Clark W. Barrett},
url = {https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_9
https://arxiv.org/abs/2006.05449},
doi = {10.34727/2020/isbn.978-3-85448-042-6_9},
year = {2020},
date = {2020-01-01},
urldate = {2020-01-01},
booktitle = {2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa,
Israel, September 21-24, 2020},
pages = {1–10},
publisher = {IEEE},
abstract = {Symbolic quick error detection (SQED) is a formal pre-silicon verification technique targeted at processor designs. It leverages bounded model checking (BMC) to check a design for counterexamples to a self-consistency property: given the instruction set architecture (ISA) of the design, executing an instruction sequence twice on the same inputs must always produce the same outputs. Self-consistency is a universal, implementation-independent property. Consequently, in contrast to traditional verification approaches that use implementation-specific assertions (often generated manually), SQED does not require a full formal design specification or manually-written properties. Case studies have shown that SQED is effective for commercial designs and that SQED substantially improves design productivity. However, until now there has been no formal characterization of its bug-finding capabilities. We aim to close this gap by laying a formal foundation for SQED. We use a transition-system processor model and define the notion of a bug using an abstract specification relation. We prove the soundness of SQED, i.e., that any bug reported by SQED is in fact a real bug in the processor. Importantly, this result holds regardless of what the actual specification relation is. We next describe conditions under which SQED is complete, that is, what kinds of bugs it is guaranteed to find. We show that for a large class of bugs, SQED can always find a trace exhibiting the bug. Ultimately, we prove full completeness of a variant of SQED that uses specialized state reset instructions. Our results enable a rigorous understanding of SQED and its bug-finding capabilities and give insights on how to optimize implementations of SQED in practice.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Symbolic quick error detection (SQED) is a formal pre-silicon verification technique targeted at processor designs. It leverages bounded model checking (BMC) to check a design for counterexamples to a self-consistency property: given the instruction set architecture (ISA) of the design, executing an instruction sequence twice on the same inputs must always produce the same outputs. Self-consistency is a universal, implementation-independent property. Consequently, in contrast to traditional verification approaches that use implementation-specific assertions (often generated manually), SQED does not require a full formal design specification or manually-written properties. Case studies have shown that SQED is effective for commercial designs and that SQED substantially improves design productivity. However, until now there has been no formal characterization of its bug-finding capabilities. We aim to close this gap by laying a formal foundation for SQED. We use a transition-system processor model and define the notion of a bug using an abstract specification relation. We prove the soundness of SQED, i.e., that any bug reported by SQED is in fact a real bug in the processor. Importantly, this result holds regardless of what the actual specification relation is. We next describe conditions under which SQED is complete, that is, what kinds of bugs it is guaranteed to find. We show that for a large class of bugs, SQED can always find a trace exhibiting the bug. Ultimately, we prove full completeness of a variant of SQED that uses specialized state reset instructions. Our results enable a rigorous understanding of SQED and its bug-finding capabilities and give insights on how to optimize implementations of SQED in practice.
Singh, Eshan; Lonsing, Florian; Chattopadhyay, Saranyu; Strange, Maxwell; Wei, Peng; Zhang, Xiaofan; Zhou, Yuan; Chen, Deming; Cong, Jason; Raina, Priyanka; Zhang, Zhiru; Barrett, Clark W.; Mitra, Subhasish
A-QED Verification of Hardware Accelerators Proceedings Article
In: 57th ACM/IEEE Design Automation Conference, DAC 2020, San Francisco, CA, USA, July 20-24, 2020, pp. 1–6, IEEE, 2020.
Abstract | Links | BibTeX | Tags:
@inproceedings{AQED,
title = {A-QED Verification of Hardware Accelerators},
author = {Eshan Singh and Florian Lonsing and Saranyu Chattopadhyay and Maxwell Strange and Peng Wei and Xiaofan Zhang and Yuan Zhou and Deming Chen and Jason Cong and Priyanka Raina and Zhiru Zhang and Clark W. Barrett and Subhasish Mitra},
url = {https://doi.org/10.1109/DAC18072.2020.9218715
https://wp.florianlonsing.com/wp-content/uploads/2024/01/Singh-et-al-AQED-DAC2020.pdf},
doi = {10.1109/DAC18072.2020.9218715},
year = {2020},
date = {2020-01-01},
urldate = {2020-01-01},
booktitle = {57th ACM/IEEE Design Automation Conference, DAC 2020, San Francisco,
CA, USA, July 20-24, 2020},
pages = {1–6},
publisher = {IEEE},
abstract = {We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking -- however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking -- however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).
2019
Lonsing, Florian; Ganesan, Karthik; Mann, Makai; Nuthakki, Srinivasa Shashank; Singh, Eshan; Srouji, Mario; Yang, Yahan; Mitra, Subhasish; Barrett, Clark W.
Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper Proceedings Article
In: Pan, David Z. (Ed.): Proceedings of the International Conference on Computer-Aided Design, ICCAD 2019, Westminster, CO, USA, November 4-7, 2019, pp. 1–8, ACM, 2019.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/iccad/LonsingGMNSSYMB19,
title = {Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper},
author = {Florian Lonsing and Karthik Ganesan and Makai Mann and Srinivasa Shashank Nuthakki and Eshan Singh and Mario Srouji and Yahan Yang and Subhasish Mitra and Clark W. Barrett},
editor = {David Z. Pan},
url = {https://doi.org/10.1109/ICCAD45719.2019.8942096
https://wp.florianlonsing.com/wp-content/uploads/2024/01/ICCAD2019-SQED-invited.pdf},
doi = {10.1109/ICCAD45719.2019.8942096},
year = {2019},
date = {2019-01-01},
urldate = {2019-01-01},
booktitle = {Proceedings of the International Conference on Computer-Aided Design,
ICCAD 2019, Westminster, CO, USA, November 4-7, 2019},
pages = {1–8},
publisher = {ACM},
abstract = {As designs grow in size and complexity, design verification becomes one of the most difficult and costly tasks facing design teams. Formal verification techniques offer great promise because of their ability to exhaustively explore design behaviors. However, formal techniques also have a reputation for being labor-intensive and limited to small blocks. Is there any hope for successful application of formal techniques at design scale? We answer this question affirmatively by digging deeper to understand what the real technological issues and opportunities are. First, we look at satisfiability solvers, the engines underlying formal techniques such as model checking. Given the recent innovations in satisfiability solving, we argue that there are many reasons to be optimistic that formal techniques will scale to designs of practical interest. We use our CoSA model checker as a demonstration platform to illustrate how advances in solvers can improve scalability. However, even if solvers become blazingly fast, applying them well is still labor-intensive. This is because formal tools are only as useful as the properties they are given to prove, which traditionally have required great effort to develop. Symbolic quick error detection (SQED) addresses this issue by using a single, universal property that checks designs automatically. We demonstrate how SQED can automatically find logic and security bugs in a variety of designs and report on bugs found and efficiency gains realized in academic and industry designs. We also present a generator for an improved SQED module that further reduces the amount of manual effort that has to be spent by the designer.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
As designs grow in size and complexity, design verification becomes one of the most difficult and costly tasks facing design teams. Formal verification techniques offer great promise because of their ability to exhaustively explore design behaviors. However, formal techniques also have a reputation for being labor-intensive and limited to small blocks. Is there any hope for successful application of formal techniques at design scale? We answer this question affirmatively by digging deeper to understand what the real technological issues and opportunities are. First, we look at satisfiability solvers, the engines underlying formal techniques such as model checking. Given the recent innovations in satisfiability solving, we argue that there are many reasons to be optimistic that formal techniques will scale to designs of practical interest. We use our CoSA model checker as a demonstration platform to illustrate how advances in solvers can improve scalability. However, even if solvers become blazingly fast, applying them well is still labor-intensive. This is because formal tools are only as useful as the properties they are given to prove, which traditionally have required great effort to develop. Symbolic quick error detection (SQED) addresses this issue by using a single, universal property that checks designs automatically. We demonstrate how SQED can automatically find logic and security bugs in a variety of designs and report on bugs found and efficiency gains realized in academic and industry designs. We also present a generator for an improved SQED module that further reduces the amount of manual effort that has to be spent by the designer.
Lonsing, Florian; Egly, Uwe
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, pp. 203–210, 2019.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingE19,
title = {QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties},
author = {Florian Lonsing and Uwe Egly},
url = {https://doi.org/10.1007/978-3-030-24258-9_14
https://arxiv.org/pdf/1904.12927.pdf},
doi = {10.1007/978-3-030-24258-9_14},
year = {2019},
date = {2019-01-01},
urldate = {2019-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd
International Conference, SAT 2019, Lisbon, Portugal, July 9-12,
2019, Proceedings},
pages = {203–210},
crossref = {DBLP:conf/sat/2019},
abstract = {We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong redundancy properties of clauses and universal literals. QRATPre+ is the first implementation of these redundancy properties in QRAT and QRAT+ used to simplify QBFs in preprocessing. It is written in C and features an API for easy integration in other QBF tools. We present implementation details and report on experimental results demonstrating that QRATPre+ improves upon the power of state-of-the-art preprocessors and solvers.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong redundancy properties of clauses and universal literals. QRATPre+ is the first implementation of these redundancy properties in QRAT and QRAT+ used to simplify QBFs in preprocessing. It is written in C and features an API for easy integration in other QBF tools. We present implementation details and report on experimental results demonstrating that QRATPre+ improves upon the power of state-of-the-art preprocessors and solvers.
Lonsing, Florian
QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving Journal Article
In: Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 11, no. 1, pp. 211–220, 2019.
Abstract | Links | BibTeX | Tags:
@article{DBLP:journals/jsat/Lonsing19,
title = {QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving},
author = {Florian Lonsing},
url = {https://doi.org/10.3233/SAT190122},
doi = {10.3233/SAT190122},
year = {2019},
date = {2019-01-01},
urldate = {2019-01-01},
journal = {Journal on Satisfiability, Boolean Modeling and Computation (JSAT)},
volume = {11},
number = {1},
pages = {211–220},
abstract = {DepQBF is a search-based quantified Boolean formula (QBF) solver implementing the QCDCL paradigm. We submitted DepQBF as part of several tool packages to the QBFEVAL’18 competition, which was part of the FLoC Olympic Games 2018. These packages integrate DepQBF as a back end QBF solver and a preprocessing front end called QBFRelay. This front end consists of a shell script that runs several preprocessors in multiple rounds on a given QBF, thus resulting in incremental preprocessing. QBFRelay employs publicly available preprocessors developed by the QBF community and, additionally, our novel preprocessor QRATPre+ that is based on a generalization of the QRAT proof system. We present an overview of DepQBF, QRATPre+, and QBFRelay and report on the performance of our submissions, which were awarded a medal in the FLoC Olympic Games.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
DepQBF is a search-based quantified Boolean formula (QBF) solver implementing the QCDCL paradigm. We submitted DepQBF as part of several tool packages to the QBFEVAL’18 competition, which was part of the FLoC Olympic Games 2018. These packages integrate DepQBF as a back end QBF solver and a preprocessing front end called QBFRelay. This front end consists of a shell script that runs several preprocessors in multiple rounds on a given QBF, thus resulting in incremental preprocessing. QBFRelay employs publicly available preprocessors developed by the QBF community and, additionally, our novel preprocessor QRATPre+ that is based on a generalization of the QRAT proof system. We present an overview of DepQBF, QRATPre+, and QBFRelay and report on the performance of our submissions, which were awarded a medal in the FLoC Olympic Games.
2018
Lonsing, Florian; Seidl, Martina
Parallel Solving of Quantified Boolean Formulas Book Section
In: Handbook of Parallel Constraint Reasoning, pp. 101–139, Springer International Publishing, 2018, ISBN: 978-3-319-63516-3.
Abstract | Links | BibTeX | Tags:
@incollection{HamadiSaisPCRBookQBFChapter,
title = {Parallel Solving of Quantified Boolean Formulas},
author = {Florian Lonsing and Martina Seidl},
doi = {10.1007/978-3-319-63516-3_4},
isbn = {978-3-319-63516-3},
year = {2018},
date = {2018-01-01},
urldate = {2018-01-01},
booktitle = {Handbook of Parallel Constraint Reasoning},
pages = {101–139},
publisher = {Springer International Publishing},
chapter = {4},
crossref = {HamadiSaisPCRBook},
abstract = {Quantified Boolean formulas (QBFs) extend propositional logic by universal and existential quantifiers over the propositional variables. In the same way as the satisfiability problem of propositional logic is the archetypical problem for NP, the satisfiability problem of QBFs is the archetypical problem for PSPACE. Hence, QBFs provide an attractive framework for encoding many applications from verification, artificial intelligence, and synthesis, thus motivating the quest for efficient solving technology. Already in the very early stages of QBF solving history, attempts have been made to parallelize the solving process, either by splitting the search space or by portfolio-based approaches. In this chapter, we review and compare approaches for solving QBFs in parallel.},
keywords = {},
pubstate = {published},
tppubtype = {incollection}
}
Quantified Boolean formulas (QBFs) extend propositional logic by universal and existential quantifiers over the propositional variables. In the same way as the satisfiability problem of propositional logic is the archetypical problem for NP, the satisfiability problem of QBFs is the archetypical problem for PSPACE. Hence, QBFs provide an attractive framework for encoding many applications from verification, artificial intelligence, and synthesis, thus motivating the quest for efficient solving technology. Already in the very early stages of QBF solving history, attempts have been made to parallelize the solving process, either by splitting the search space or by portfolio-based approaches. In this chapter, we review and compare approaches for solving QBFs in parallel.
Bloem, Roderick; Braud-Santoni, Nicolas; Hadzic, Vedad; Egly, Uwe; Lonsing, Florian; Seidl, Martina
Expansion-Based QBF Solving Without Recursion Proceedings Article
In: Formal Methods in Computer-Aided Design (FMCAD), October 30 - November 2, 2018, Austin, Texas, USA, IEEE, 2018.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/fmcad/BloemEtAl2018accepted,
title = {Expansion-Based QBF Solving Without Recursion},
author = {Roderick Bloem and Nicolas Braud-Santoni and Vedad Hadzic and Uwe Egly and Florian Lonsing and Martina Seidl},
url = {https://arxiv.org/pdf/1807.08964},
year = {2018},
date = {2018-01-01},
urldate = {2018-01-01},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD), October 30 - November 2, 2018, Austin, Texas, USA},
publisher = {IEEE},
abstract = {In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) and pass the obtained formula to a SAT solver for deciding the QBF. State-of-the-art expansion-based solvers process the given formula quantifier-block wise and recursively apply expansion until a solution is found. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) and pass the obtained formula to a SAT solver for deciding the QBF. State-of-the-art expansion-based solvers process the given formula quantifier-block wise and recursively apply expansion until a solution is found. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.
Lonsing, Florian; Egly, Uwe
Evaluating QBF Solvers: Quantifier Alternations Matter Proceedings Article
In: Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, pp. 276–294, 2018.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/cp/LonsingE18,
title = {Evaluating QBF Solvers: Quantifier Alternations Matter},
author = {Florian Lonsing and Uwe Egly},
url = {https://doi.org/10.1007/978-3-319-98334-9_19
https://arxiv.org/pdf/1701.06612.pdf},
doi = {10.1007/978-3-319-98334-9_19},
year = {2018},
date = {2018-01-01},
urldate = {2018-01-01},
booktitle = {Principles and Practice of Constraint Programming - 24th International
Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings},
pages = {276–294},
crossref = {DBLP:conf/cp/2018},
abstract = {We present an experimental study of the effects of quantifier alternations on the evaluation of quantified Boolean formula (QBF) solvers. The number of quantifier alternations in a QBF in prenex conjunctive normal form (PCNF) is directly related to the theoretical hardness of the respective QBF satisfiability problem in the polynomial hierarchy. We show empirically that the performance of solvers based on different solving paradigms substantially varies depending on the numbers of alternations in PCNFs. In related theoretical work, quantifier alternations have become the focus of understanding the strengths and weaknesses of various QBF proof systems implemented in solvers. Our results motivate the development of methods to evaluate orthogonal solving paradigms by taking quantifier alternations into account. This is necessary to showcase the broad range of existing QBF solving paradigms for practical QBF applications. Moreover, we highlight the potential of combining different approaches and QBF proof systems in solvers.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present an experimental study of the effects of quantifier alternations on the evaluation of quantified Boolean formula (QBF) solvers. The number of quantifier alternations in a QBF in prenex conjunctive normal form (PCNF) is directly related to the theoretical hardness of the respective QBF satisfiability problem in the polynomial hierarchy. We show empirically that the performance of solvers based on different solving paradigms substantially varies depending on the numbers of alternations in PCNFs. In related theoretical work, quantifier alternations have become the focus of understanding the strengths and weaknesses of various QBF proof systems implemented in solvers. Our results motivate the development of methods to evaluate orthogonal solving paradigms by taking quantifier alternations into account. This is necessary to showcase the broad range of existing QBF solving paradigms for practical QBF applications. Moreover, we highlight the potential of combining different approaches and QBF proof systems in solvers.
Lonsing, Florian; Egly, Uwe
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property Proceedings Article
In: Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, pp. 161–177, 2018.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/cade/LonsingE18,
title = {QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property},
author = {Florian Lonsing and Uwe Egly},
url = {https://doi.org/10.1007/978-3-319-94205-6_12
https://arxiv.org/pdf/1804.02908},
doi = {10.1007/978-3-319-94205-6_12},
year = {2018},
date = {2018-01-01},
urldate = {2018-01-01},
booktitle = {Automated Reasoning - 9th International Joint Conference, IJCAR
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings},
pages = {161–177},
crossref = {DBLP:conf/cade/2018},
abstract = {The QRAT (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning tools. It consists of rules to rewrite a QBF by adding and deleting clauses and universal literals that have a certain redundancy property. To check for this redundancy property in QRAT, propositional unit propagation (UP) is applied to the quantifier free, i.e., propositional part of the QBF. We generalize the redundancy property in the QRAT system by QBF specific UP (QUP). QUP extends UP by the universal reduction operation to eliminate universal literals from clauses. We apply QUP to an abstraction of the QBF where certain universal quantifiers are converted into existential ones. This way, we obtain a generalization of QRAT we call QRAT+. The redundancy property in QRAT+ based on QUP is more powerful than the one in QRAT based on UP. We report on proof theoretical improvements and experimental results to illustrate the benefits of QRAT+ for QBF preprocessing. },
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The QRAT (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning tools. It consists of rules to rewrite a QBF by adding and deleting clauses and universal literals that have a certain redundancy property. To check for this redundancy property in QRAT, propositional unit propagation (UP) is applied to the quantifier free, i.e., propositional part of the QBF. We generalize the redundancy property in the QRAT system by QBF specific UP (QUP). QUP extends UP by the universal reduction operation to eliminate universal literals from clauses. We apply QUP to an abstraction of the QBF where certain universal quantifiers are converted into existential ones. This way, we obtain a generalization of QRAT we call QRAT+. The redundancy property in QRAT+ based on QUP is more powerful than the one in QRAT based on UP. We report on proof theoretical improvements and experimental results to illustrate the benefits of QRAT+ for QBF preprocessing.
2017
Lonsing, Florian; Egly, Uwe
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL Proceedings Article
In: Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pp. 371–384, 2017.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/cade/LonsingE17,
title = {DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL},
author = {Florian Lonsing and Uwe Egly},
url = {https://doi.org/10.1007/978-3-319-63046-5_23
https://arxiv.org/pdf/1702.08256},
doi = {10.1007/978-3-319-63046-5_23},
year = {2017},
date = {2017-01-01},
urldate = {2017-01-01},
booktitle = {Automated Deduction - CADE 26 - 26th International Conference on
Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
pages = {371–384},
crossref = {DBLP:conf/cade/2017},
abstract = {We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional satisfiability (SAT) solvers. The Q-resolution calculus (QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produce QRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0 implements a variant of QCDCL which is based on a generalization of QRES. This generalization is due to a set of additional axioms and leaves the original Q-resolution rules unchanged. The generalization of QRES enables QCDCL to potentially produce exponentially shorter proofs than the traditional variant. We present an overview of the features implemented in DepQBF and report on experimental results which demonstrate the effectiveness of generalized QRES in QCDCL.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional satisfiability (SAT) solvers. The Q-resolution calculus (QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produce QRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0 implements a variant of QCDCL which is based on a generalization of QRES. This generalization is due to a set of additional axioms and leaves the original Q-resolution rules unchanged. The generalization of QRES enables QCDCL to potentially produce exponentially shorter proofs than the traditional variant. We present an overview of the features implemented in DepQBF and report on experimental results which demonstrate the effectiveness of generalized QRES in QCDCL.
Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas
Conformant Planning as a Case Study of Incremental QBF Solving Journal Article
In: Ann.~Math.~Artif.~Intell., vol. 80, no. 1, pp. 21–45, 2017.
Abstract | Links | BibTeX | Tags:
@article{DBLP:journals/amai/EglyKLP17,
title = {Conformant Planning as a Case Study of Incremental QBF Solving},
author = {Uwe Egly and Martin Kronegger and Florian Lonsing and Andreas Pfandler},
url = {https://doi.org/10.1007/s10472-016-9501-2},
doi = {10.1007/s10472-016-9501-2},
year = {2017},
date = {2017-01-01},
urldate = {2017-01-01},
journal = {Ann.~Math.~Artif.~Intell.},
volume = {80},
number = {1},
pages = {21–45},
abstract = {We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of successively constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase as well as in the solving phase. We also present experiments with incremental preprocessing techniques that are based on blocked clause elimination (QBCE). QBCE allows to eliminate certain clauses from a QBF in a satisfiability preserving way. We implemented the QBCE-based techniques in DepQBF in three variants: as preprocessing, as inprocessing (which extends preprocessing by taking into account variable assignments that were fixed by the QBF solver), and as a novel dynamic approach where QBCE is tightly integrated in the solving process. For DepQBF, experimental results show that incremental QBF solving with incremental QBCE outperforms incremental QBF solving without QBCE, which in turn outperforms nonincremental QBF solving. For the first time we report on incremental QBF solving with incremental QBCE as inprocessing. Our results are the first empirical study of incremental QBF solving in the context of planning and motivate its use in other application domains.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of successively constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase as well as in the solving phase. We also present experiments with incremental preprocessing techniques that are based on blocked clause elimination (QBCE). QBCE allows to eliminate certain clauses from a QBF in a satisfiability preserving way. We implemented the QBCE-based techniques in DepQBF in three variants: as preprocessing, as inprocessing (which extends preprocessing by taking into account variable assignments that were fixed by the QBF solver), and as a novel dynamic approach where QBCE is tightly integrated in the solving process. For DepQBF, experimental results show that incremental QBF solving with incremental QBCE outperforms incremental QBF solving without QBCE, which in turn outperforms nonincremental QBF solving. For the first time we report on incremental QBF solving with incremental QBCE as inprocessing. Our results are the first empirical study of incremental QBF solving in the context of planning and motivate its use in other application domains.
2016
Lonsing, Florian; Egly, Uwe; Seidl, Martina
Q-Resolution with Generalized Axioms Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, pp. 435–452, 2016.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingES16,
title = {Q-Resolution with Generalized Axioms},
author = {Florian Lonsing and Uwe Egly and Martina Seidl},
url = {http://dx.doi.org/10.1007/978-3-319-40970-2_27
http://arxiv.org/pdf/1604.05994},
doi = {10.1007/978-3-319-40970-2_27},
year = {2016},
date = {2016-01-01},
urldate = {2016-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2016 - 19th
International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
pages = {435–452},
crossref = {DBLP:conf/sat/2016},
abstract = {Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.
Balyo, Tomas; Lonsing, Florian
HordeQBF: A Modular and Massively Parallel QBF Solver Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, pp. 531–538, 2016.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/BalyoL16,
title = {HordeQBF: A Modular and Massively Parallel QBF Solver},
author = {Tomas Balyo and Florian Lonsing},
url = {http://dx.doi.org/10.1007/978-3-319-40970-2_33
http://arxiv.org/pdf/1604.03793},
doi = {10.1007/978-3-319-40970-2_33},
year = {2016},
date = {2016-01-01},
urldate = {2016-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2016 - 19th
International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
pages = {531–538},
crossref = {DBLP:conf/sat/2016},
abstract = {The recently developed massively parallel satisfiability (SAT) solver HordeSAT was designed in a modular way to allow the integration of any sequential CDCL-based SAT solver in its core. We integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT to obtain a massively parallel QBF solver—HordeQBF. In this paper we describe the details of this integration and report on results of the experimental evaluation of HordeQBF’s performance. HordeQBF achieves superlinear average and median speedup on the hard application instances of the 2014 QBF Gallery.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The recently developed massively parallel satisfiability (SAT) solver HordeSAT was designed in a modular way to allow the integration of any sequential CDCL-based SAT solver in its core. We integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT to obtain a massively parallel QBF solver—HordeQBF. In this paper we describe the details of this integration and report on results of the experimental evaluation of HordeQBF’s performance. HordeQBF achieves superlinear average and median speedup on the hard application instances of the 2014 QBF Gallery.
Lonsing, Florian; Seidl, Martina (Ed.)
CEUR-WS.org, vol. 1719, 2016.
Abstract | Links | BibTeX | Tags:
@proceedings{QBF2016proceedings,
title = {Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France, July 4, 2016 co-located with 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016)},
editor = {Florian Lonsing and Martina Seidl},
url = {http://ceur-ws.org/Vol-1719/},
year = {2016},
date = {2016-01-01},
urldate = {2016-01-01},
volume = {1719},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
abstract = {The goal of the International Workshop on Quantified Boolean Formulas (QBF Workshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. The aim of this workshop is to provide an interactive platform for discussing recent advancements and alternative approaches to QBF solving. The QBF Workshop addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges. The 4th edition of the QBF Workshop took place on the 4th of July in Bordeaux and was co-located with the 19th International Conference on Theory and Applications of Satisfiability Testing. In its 4th edition, the QBF Workshop broadened its scope. Apart from topics related to QBF, topics of interest included the theory and practice of quantification in other formalisms like quantified constraint satisfaction problems (QCSP), satisfiability modulo theories (SMT) or theorem proving. After a careful reviewing process, three contributed papers were chosen for presentation. The papers are the first three papers included in these proceedings. Besides three invited talks by M. Janota, C. Scholl and R. Wimmer, and M. Suda, the QBF Workshop had the pleasure to feature a keynote by H. Kleine Büning on “Open Problems for Quantified Boolean Formulas”. In six short presentations, several solvers participating the QBFEval 2016, were presented. We invited all participants to include a solver description in this proceedings. Three teams provided such descriptions which were accepted for this proceedings after an additional round of reviews. L. Pulina concluded the QBF Workshop with a presentation of the results of the QBFEval 2016. A summary is included in this proceedings as invited contribution. Last but not least, we would like to thank all the PC members and subreviewers for their work helping us to set up an interesting program for the workshop and to ensure the quality of this proceedings.},
keywords = {},
pubstate = {published},
tppubtype = {proceedings}
}
The goal of the International Workshop on Quantified Boolean Formulas (QBF Workshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. The aim of this workshop is to provide an interactive platform for discussing recent advancements and alternative approaches to QBF solving. The QBF Workshop addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges. The 4th edition of the QBF Workshop took place on the 4th of July in Bordeaux and was co-located with the 19th International Conference on Theory and Applications of Satisfiability Testing. In its 4th edition, the QBF Workshop broadened its scope. Apart from topics related to QBF, topics of interest included the theory and practice of quantification in other formalisms like quantified constraint satisfaction problems (QCSP), satisfiability modulo theories (SMT) or theorem proving. After a careful reviewing process, three contributed papers were chosen for presentation. The papers are the first three papers included in these proceedings. Besides three invited talks by M. Janota, C. Scholl and R. Wimmer, and M. Suda, the QBF Workshop had the pleasure to feature a keynote by H. Kleine Büning on “Open Problems for Quantified Boolean Formulas”. In six short presentations, several solvers participating the QBFEval 2016, were presented. We invited all participants to include a solver description in this proceedings. Three teams provided such descriptions which were accepted for this proceedings after an additional round of reviews. L. Pulina concluded the QBF Workshop with a presentation of the results of the QBFEval 2016. A summary is included in this proceedings as invited contribution. Last but not least, we would like to thank all the PC members and subreviewers for their work helping us to set up an interesting program for the workshop and to ensure the quality of this proceedings.
Janota, Mikolas; Jordan, Charles; Klieber, Will; Lonsing, Florian; Seidl, Martina; Gelder, Allen Van
The QBF Gallery 2014: The QBF Competition at the FLoC Olympic Games Journal Article
In: Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 9, pp. 187-206, 2016.
Abstract | Links | BibTeX | Tags:
@article{gallery14,
title = {The QBF Gallery 2014: The QBF Competition at the FLoC Olympic Games},
author = {Mikolas Janota and Charles Jordan and Will Klieber and Florian Lonsing and Martina Seidl and Allen Van Gelder},
url = {https://doi.org/10.3233/sat190108},
year = {2016},
date = {2016-01-01},
urldate = {2016-01-01},
journal = {Journal on Satisfiability, Boolean Modeling and Computation (JSAT)},
volume = {9},
pages = {187-206},
abstract = {The QBF Gallery 2014 was a competitive evaluation for QBF solvers organized as part of the FLoC 2014 Olympic Games during the Vienna Summer of Logic. The QBF Gallery 2014 featured three different tracks on formulas in prenex conjunctive normal form (PCNF) including more than 1200 formulas to be solved. Gold, silver, and bronze track medals were awarded to the solvers that solved the most formulas in each of the three tracks. Additionally, the three participants that were most successful over the complete benchmark set were awarded with Kurt Gödel medals, the official prizes of the FLoC 2014 Olympic Games. In this paper, we give an overview of the setup and rules of the competition, briefly review the participating solvers, and finally report on the results of the QBF Gallery 2014.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The QBF Gallery 2014 was a competitive evaluation for QBF solvers organized as part of the FLoC 2014 Olympic Games during the Vienna Summer of Logic. The QBF Gallery 2014 featured three different tracks on formulas in prenex conjunctive normal form (PCNF) including more than 1200 formulas to be solved. Gold, silver, and bronze track medals were awarded to the solvers that solved the most formulas in each of the three tracks. Additionally, the three participants that were most successful over the complete benchmark set were awarded with Kurt Gödel medals, the official prizes of the FLoC 2014 Olympic Games. In this paper, we give an overview of the setup and rules of the competition, briefly review the participating solvers, and finally report on the results of the QBF Gallery 2014.
Lonsing, Florian; Seidl, Martina; Gelder, Allen Van
The QBF Gallery: Behind the scenes Journal Article
In: Artif. Intell., vol. 237, pp. 92–114, 2016.
Abstract | Links | BibTeX | Tags:
@article{DBLP:journals/ai/LonsingSG16,
title = {The QBF Gallery: Behind the scenes},
author = {Florian Lonsing and Martina Seidl and Allen Van Gelder},
url = {http://dx.doi.org/10.1016/j.artint.2016.04.002
http://arxiv.org/pdf/1508.01045},
doi = {10.1016/j.artint.2016.04.002},
year = {2016},
date = {2016-01-01},
urldate = {2016-01-01},
journal = {Artif. Intell.},
volume = {237},
pages = {92–114},
abstract = {Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.
2015
Egly, Uwe; Lonsing, Florian; Oetsch, Johannes
Automated Benchmarking of Incremental SAT and QBF Solvers Proceedings Article
In: Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, pp. 178–186, 2015.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/lpar/EglyLO15,
title = {Automated Benchmarking of Incremental SAT and QBF Solvers},
author = {Uwe Egly and Florian Lonsing and Johannes Oetsch},
url = {http://dx.doi.org/10.1007/978-3-662-48899-7_13
http://arxiv.org/pdf/1506.08563.pdf},
doi = {10.1007/978-3-662-48899-7_13},
year = {2015},
date = {2015-01-01},
urldate = {2015-01-01},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
International Conference, LPAR-20 2015, Suva, Fiji, November 24-28,
2015, Proceedings},
pages = {178–186},
crossref = {DBLP:conf/lpar/2015},
abstract = {Incremental SAT and QBF solving potentially yields improvements when sequences of related formulas are solved. An incremental application is usually tailored towards some specific solver and decomposes a problem into incremental solver calls. This hinders the independent comparison of different solvers, particularly when the application program is not available. As a remedy, we present an approach to automated benchmarking of incremental SAT and QBF solvers. Given a collection of formulas in (Q)DIMACS format generated incrementally by an application program, our approach automatically translates the formulas into instructions to import and solve a formula by an incremental SAT/QBF solver. The result of the translation is a program which replays the incremental solver calls and thus allows to evaluate incremental solvers independently from the application program. We illustrate our approach by different hardware verification problems for SAT and QBF solvers.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Incremental SAT and QBF solving potentially yields improvements when sequences of related formulas are solved. An incremental application is usually tailored towards some specific solver and decomposes a problem into incremental solver calls. This hinders the independent comparison of different solvers, particularly when the application program is not available. As a remedy, we present an approach to automated benchmarking of incremental SAT and QBF solvers. Given a collection of formulas in (Q)DIMACS format generated incrementally by an application program, our approach automatically translates the formulas into instructions to import and solve a formula by an incremental SAT/QBF solver. The result of the translation is a program which replays the incremental solver calls and thus allows to evaluate incremental solvers independently from the application program. We illustrate our approach by different hardware verification problems for SAT and QBF solvers.
Lonsing, Florian; Bacchus, Fahiem; Biere, Armin; Egly, Uwe; Seidl, Martina
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination Proceedings Article
In: Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, pp. 418–433, 2015.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/lpar/LonsingBBES15,
title = {Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination},
author = {Florian Lonsing and Fahiem Bacchus and Armin Biere and Uwe Egly and Martina Seidl},
url = {http://dx.doi.org/10.1007/978-3-662-48899-7_29
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingBBES-LPAR2015.pdf},
doi = {10.1007/978-3-662-48899-7_29},
year = {2015},
date = {2015-01-01},
urldate = {2015-01-01},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
International Conference, LPAR-20 2015, Suva, Fiji, November 24-28,
2015, Proceedings},
pages = {418–433},
crossref = {DBLP:conf/lpar/2015},
abstract = {Among preprocessing techniques for quantified Boolean formula (QBF) solving, quantified blocked clause elimination (QBCE) has been found to be extremely effective. We investigate the power of dynamically applying QBCE in search-based QBF solving with clause and cube learning (QCDCL). This dynamic application of QBCE is in sharp contrast to its typical use as a mere preprocessing technique. In our dynamic approach, QBCE is applied eagerly to the formula interpreted under the assignments that have been enumerated in QCDCL. The tight integration of QBCE in QCDCL results in a variant of cube learning which is exponentially stronger than the traditional method. We implemented our approach in the QBF solver DepQBF and ran experiments on instances from the QBF Gallery 2014. On application benchmarks, QCDCL with dynamic QBCE substantially outperforms traditional QCDCL. Moreover, our approach is compatible with incremental solving and can be combined with preprocessing techniques other than QBCE.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Among preprocessing techniques for quantified Boolean formula (QBF) solving, quantified blocked clause elimination (QBCE) has been found to be extremely effective. We investigate the power of dynamically applying QBCE in search-based QBF solving with clause and cube learning (QCDCL). This dynamic application of QBCE is in sharp contrast to its typical use as a mere preprocessing technique. In our dynamic approach, QBCE is applied eagerly to the formula interpreted under the assignments that have been enumerated in QCDCL. The tight integration of QBCE in QCDCL results in a variant of cube learning which is exponentially stronger than the traditional method. We implemented our approach in the QBF solver DepQBF and ran experiments on instances from the QBF Gallery 2014. On application benchmarks, QCDCL with dynamic QBCE substantially outperforms traditional QCDCL. Moreover, our approach is compatible with incremental solving and can be combined with preprocessing techniques other than QBCE.
Lonsing, Florian; Egly, Uwe
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, pp. 191–198, 2015.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingE15,
title = {Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API},
author = {Florian Lonsing and Uwe Egly},
url = {http://dx.doi.org/10.1007/978-3-319-24318-4_14
http://arxiv.org/abs/1502.02484},
doi = {10.1007/978-3-319-24318-4_14},
year = {2015},
date = {2015-01-01},
urldate = {2015-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2015 - 18th
International Conference, Austin, TX, USA, September 24-27, 2015,
Proceedings},
pages = {191–198},
crossref = {DBLP:conf/sat/2015},
abstract = {We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of the novel API is related to incremental SAT solving based on selector variables and assumptions. However, the API entirely hides selector variables and assumptions from the user, which facilitates the integration of DepQBF in other tools. We present implementation details and, for the first time, report on experiments related to the computation of MUCs of QBFs using DepQBF’s novel clause group API.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of the novel API is related to incremental SAT solving based on selector variables and assumptions. However, the API entirely hides selector variables and assumptions from the user, which facilitates the integration of DepQBF in other tools. We present implementation details and, for the first time, report on experiments related to the computation of MUCs of QBFs using DepQBF’s novel clause group API.
Heule, Marijn; Järvisalo, Matti; Lonsing, Florian; Seidl, Martina; Biere, Armin
Clause Elimination for SAT and QSAT Journal Article
In: J. Artif. Intell. Res. (JAIR), vol. 53, pp. 127–168, 2015.
Abstract | Links | BibTeX | Tags:
@article{DBLP:journals/jair/HeuleJLSB15,
title = {Clause Elimination for SAT and QSAT},
author = {Marijn Heule and Matti Järvisalo and Florian Lonsing and Martina Seidl and Armin Biere},
url = {http://dx.doi.org/10.1613/jair.4694},
doi = {10.1613/jair.4694},
year = {2015},
date = {2015-01-01},
urldate = {2015-01-01},
journal = {J. Artif. Intell. Res. (JAIR)},
volume = {53},
pages = {127–168},
abstract = {The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT—the standard input formats of SAT and QSAT solvers—have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to recon-struct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT—the standard input formats of SAT and QSAT solvers—have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to recon-struct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.
2014
Lonsing, Florian; Egly, Uwe
Incremental QBF Solving Proceedings Article
In: Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, pp. 514–530, 2014.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/cp/LonsingE14,
title = {Incremental QBF Solving},
author = {Florian Lonsing and Uwe Egly},
url = {http://dx.doi.org/10.1007/978-3-319-10428-7_38
http://arxiv.org/abs/1402.2410},
doi = {10.1007/978-3-319-10428-7_38},
year = {2014},
date = {2014-01-01},
urldate = {2014-01-01},
booktitle = {Principles and Practice of Constraint Programming - 20th International
Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings},
pages = {514–530},
crossref = {DBLP:conf/cp/2014},
abstract = {We consider the problem of incrementally solving a sequence of quantified Boolean formulae (QBF). Incremental solving aims at using information learned from one formula in the process of solving the next formulae in the sequence. Based on a general overview of the problem and related challenges, we present an approach to incremental QBF solving which is application-independent and hence applicable to QBF encodings of arbitrary problems. We implemented this approach in our incremental search-based QBF solver DepQBF and report on implementation details. Experimental results illustrate the potential benefits of incremental solving in QBF-based workflows.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We consider the problem of incrementally solving a sequence of quantified Boolean formulae (QBF). Incremental solving aims at using information learned from one formula in the process of solving the next formulae in the sequence. Based on a general overview of the problem and related challenges, we present an approach to incremental QBF solving which is application-independent and hence applicable to QBF encodings of arbitrary problems. We implemented this approach in our incremental search-based QBF solver DepQBF and report on implementation details. Experimental results illustrate the potential benefits of incremental solving in QBF-based workflows.
Lonsing, Florian; Egly, Uwe
Incremental QBF Solving by DepQBF Proceedings Article
In: Mathematical Software - ICMS 2014 - 4th International Congress, Seoul, South Korea, August 5-9, 2014. Proceedings, pp. 307–314, 2014.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/icms/LonsingE14,
title = {Incremental QBF Solving by DepQBF},
author = {Florian Lonsing and Uwe Egly},
url = {http://dx.doi.org/10.1007/978-3-662-44199-2_48
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingEgly-ICMS2014.pdf},
doi = {10.1007/978-3-662-44199-2_48},
year = {2014},
date = {2014-01-01},
urldate = {2014-01-01},
booktitle = {Mathematical Software - ICMS 2014 - 4th International Congress,
Seoul, South Korea, August 5-9, 2014. Proceedings},
pages = {307–314},
crossref = {DBLP:conf/icms/2014},
abstract = {The logic of quantified Boolean formulae (QBF) extends propositional logic by explicit existential and universal quantification of the variables. We present the search-based QBF solver DepQBF which allows to solve a sequence of QBFs incrementally. The goal is to exploit information which was learned when solving previous formulae in the process of solving the next formula in a sequence. We illustrate incremental QBF solving and potential usage scenarios by examples. Incremental QBF solving has the potential to considerably improve QBF-based workflows in many application domains.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The logic of quantified Boolean formulae (QBF) extends propositional logic by explicit existential and universal quantification of the variables. We present the search-based QBF solver DepQBF which allows to solve a sequence of QBFs incrementally. The goal is to exploit information which was learned when solving previous formulae in the process of solving the next formula in a sequence. We illustrate incremental QBF solving and potential usage scenarios by examples. Incremental QBF solving has the potential to considerably improve QBF-based workflows in many application domains.
Jordan, Charles; Kaiser, Lukasz; Lonsing, Florian; Seidl, Martina
MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pp. 430–437, 2014.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/JordanKLS14,
title = {MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing},
author = {Charles Jordan and Lukasz Kaiser and Florian Lonsing and Martina Seidl},
url = {http://dx.doi.org/10.1007/978-3-319-09284-3_32},
doi = {10.1007/978-3-319-09284-3_32},
year = {2014},
date = {2014-01-01},
urldate = {2014-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2014 - 17th
International Conference, Held as Part of the Vienna Summer of Logic,
VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
pages = {430–437},
crossref = {DBLP:conf/sat/2014},
abstract = {Inspired by recent work on parallel SAT solving, we present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel. In particular, our approach uses a sequential state-of-the-art QBF solver to evaluate subformulas in working processes. It abstains from globally exchanging information between the workers, but keeps learnt information only locally. To this end, we equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated it in our novel solver MPIDepQBF as backend solver. Extensive experiments on standard computers as well as on the supercomputer Tsubame show the impact of our approach.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Inspired by recent work on parallel SAT solving, we present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel. In particular, our approach uses a sequential state-of-the-art QBF solver to evaluate subformulas in working processes. It abstains from globally exchanging information between the workers, but keeps learnt information only locally. To this end, we equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated it in our novel solver MPIDepQBF as backend solver. Extensive experiments on standard computers as well as on the supercomputer Tsubame show the impact of our approach.
Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas
Conformant Planning as a Case Study of Incremental QBF Solving Proceedings Article
In: Artificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Sevilla, Spain, December 11-13, 2014. Proceedings, pp. 120–131, 2014.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/aisc/EglyKLP14,
title = {Conformant Planning as a Case Study of Incremental QBF Solving},
author = {Uwe Egly and Martin Kronegger and Florian Lonsing and Andreas Pfandler},
url = {http://dx.doi.org/10.1007/978-3-319-13770-4_11
http://arxiv.org/abs/1405.7253},
doi = {10.1007/978-3-319-13770-4_11},
year = {2014},
date = {2014-01-01},
urldate = {2014-01-01},
booktitle = {Artificial Intelligence and Symbolic Computation - 12th International
Conference, AISC 2014, Sevilla, Spain, December 11-13, 2014. Proceedings},
pages = {120–131},
crossref = {DBLP:conf/aisc/2014},
abstract = {We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of successively constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase and in the solving phase. Experimental results show that incremental QBF solving outperforms non-incremental QBF solving. Our results are the first empirical study of incremental QBF solving in the context of planning and motivate its use in other application domains.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of successively constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase and in the solving phase. Experimental results show that incremental QBF solving outperforms non-incremental QBF solving. Our results are the first empirical study of incremental QBF solving in the context of planning and motivate its use in other application domains.
Bloem, Roderick; Egly, Uwe; Klampfl, Patrick; Könighofer, Robert; Lonsing, Florian
SAT-Based Methods for Circuit Synthesis Proceedings Article
In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, pp. 31–34, 2014.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/fmcad/BloemEKKL14,
title = {SAT-Based Methods for Circuit Synthesis},
author = {Roderick Bloem and Uwe Egly and Patrick Klampfl and Robert Könighofer and Florian Lonsing},
url = {http://dx.doi.org/10.1109/FMCAD.2014.6987592
http://arxiv.org/abs/1408.2333},
doi = {10.1109/FMCAD.2014.6987592},
year = {2014},
date = {2014-01-01},
urldate = {2014-01-01},
booktitle = {Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland,
October 21-24, 2014},
pages = {31–34},
crossref = {DBLP:conf/fmcad/2014},
abstract = {Reactive synthesis supports designers by automatically constructing correct hardware from declarative specifications. Synthesis algorithms usually compute a strategy, and then construct a circuit that implements it. In this work, we study SAT- and QBF-based methods for the second step, i.e., computing circuits from strategies. This includes methods based on QBF-certification, interpolation, and computational learning. We present optimizations, efficient implementations, and experimental results for synthesis from safety specifications, where we outperform BDDs both regarding execution time and circuit size.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Reactive synthesis supports designers by automatically constructing correct hardware from declarative specifications. Synthesis algorithms usually compute a strategy, and then construct a circuit that implements it. In this work, we study SAT- and QBF-based methods for the second step, i.e., computing circuits from strategies. This includes methods based on QBF-certification, interpolation, and computational learning. We present optimizations, efficient implementations, and experimental results for synthesis from safety specifications, where we outperform BDDs both regarding execution time and circuit size.
2013
Egly, Uwe; Lonsing, Florian; Widl, Magdalena
Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving Proceedings Article
In: Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, pp. 291–308, 2013.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/lpar/EglyLW13,
title = {Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving},
author = {Uwe Egly and Florian Lonsing and Magdalena Widl},
url = {http://dx.doi.org/10.1007/978-3-642-45221-5_21
https://wp.florianlonsing.com/wp-content/uploads/2024/01/EglyLonsingWidl-LPAR2013.pdf},
doi = {10.1007/978-3-642-45221-5_21},
year = {2013},
date = {2013-01-01},
urldate = {2013-01-01},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 19th
International Conference, LPAR-19, Stellenbosch, South Africa, December
14-19, 2013. Proceedings},
pages = {291–308},
crossref = {DBLP:conf/lpar/2013},
abstract = {Strategies (and certificates) for quantified Boolean formulas (QBFs) are of high practical relevance as they facilitate the verification of results returned by QBF solvers and the generation of solutions to problems formulated as QBFs. State of the art approaches to obtain strategies require traversing a Q-resolution proof of a QBF, which for many real-life instances is too large to handle. In this work, we consider the long-distance Q-resolution (LDQ) calculus, which allows particular tautological resolvents. We show that for a family of QBFs using the LDQ-resolution allows for exponentially shorter proofs compared to Q-resolution. We further show that an approach to strategy extraction originally presented for Q-resolution proofs can also be applied to LDQ-resolution proofs. As a practical application, we consider search-based QBF solvers which are able to learn tautological clauses based on resolution and the conflict-driven clause learning method. We prove that the resolution proofs produced by these solvers correspond to proofs in the LDQ calculus and can therefore be used as input for strategy extraction algorithms. Experimental results illustrate the potential of the LDQ calculus in search-based QBF solving.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Strategies (and certificates) for quantified Boolean formulas (QBFs) are of high practical relevance as they facilitate the verification of results returned by QBF solvers and the generation of solutions to problems formulated as QBFs. State of the art approaches to obtain strategies require traversing a Q-resolution proof of a QBF, which for many real-life instances is too large to handle. In this work, we consider the long-distance Q-resolution (LDQ) calculus, which allows particular tautological resolvents. We show that for a family of QBFs using the LDQ-resolution allows for exponentially shorter proofs compared to Q-resolution. We further show that an approach to strategy extraction originally presented for Q-resolution proofs can also be applied to LDQ-resolution proofs. As a practical application, we consider search-based QBF solvers which are able to learn tautological clauses based on resolution and the conflict-driven clause learning method. We prove that the resolution proofs produced by these solvers correspond to proofs in the LDQ calculus and can therefore be used as input for strategy extraction algorithms. Experimental results illustrate the potential of the LDQ calculus in search-based QBF solving.
Lonsing, Florian; Egly, Uwe; Gelder, Allen Van
Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, pp. 100–115, 2013.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingEG13,
title = {Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation},
author = {Florian Lonsing and Uwe Egly and Allen Van Gelder},
url = {http://dx.doi.org/10.1007/978-3-642-39071-5_9
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingEglyVanGelder-SAT2013.pdf},
doi = {10.1007/978-3-642-39071-5_9},
year = {2013},
date = {2013-01-01},
urldate = {2013-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2013 - 16th
International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings},
pages = {100–115},
crossref = {DBLP:conf/sat/2013},
abstract = {Recent solvers for quantified boolean formulas (QBF) use a clause learning method based on a procedure proposed by Giunchiglia et al. (JAIR 2006), which avoids creating tautological clauses. Recently, an exponential worst case for this procedure has been shown by Van Gelder (CP 2012). That paper introduced QBF Pseudo Unit Propagation (QPUP) for non-tautological clause learning in a limited setting and showed that its worst case is theoretically polynomial, although it might be impractical in a high-performance QBF solver, due to excessive time and space consumption. No implementation was reported.
We describe an enhanced version of QPUP learning that is practical to incorporate into high-performance QBF solvers, being compatible with pure-literal rules and dependency schemes. It can be used for proving in a concise format that a QBF formula is either unsatisfiable or satisfiable (working on both proofs in tandem). A lazy version of QPUP permits non-tautological clauses to be learned without actually carrying out resolutions, but this version is unable to produce proofs.
Experimental results show that QPUP is somewhat faster than the previous non-tautological clause learning procedure on benchmarks from QBFEVAL-12-SR.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Recent solvers for quantified boolean formulas (QBF) use a clause learning method based on a procedure proposed by Giunchiglia et al. (JAIR 2006), which avoids creating tautological clauses. Recently, an exponential worst case for this procedure has been shown by Van Gelder (CP 2012). That paper introduced QBF Pseudo Unit Propagation (QPUP) for non-tautological clause learning in a limited setting and showed that its worst case is theoretically polynomial, although it might be impractical in a high-performance QBF solver, due to excessive time and space consumption. No implementation was reported.
We describe an enhanced version of QPUP learning that is practical to incorporate into high-performance QBF solvers, being compatible with pure-literal rules and dependency schemes. It can be used for proving in a concise format that a QBF formula is either unsatisfiable or satisfiable (working on both proofs in tandem). A lazy version of QPUP permits non-tautological clauses to be learned without actually carrying out resolutions, but this version is unable to produce proofs.
Experimental results show that QPUP is somewhat faster than the previous non-tautological clause learning procedure on benchmarks from QBFEVAL-12-SR.
We describe an enhanced version of QPUP learning that is practical to incorporate into high-performance QBF solvers, being compatible with pure-literal rules and dependency schemes. It can be used for proving in a concise format that a QBF formula is either unsatisfiable or satisfiable (working on both proofs in tandem). A lazy version of QPUP permits non-tautological clauses to be learned without actually carrying out resolutions, but this version is unable to produce proofs.
Experimental results show that QPUP is somewhat faster than the previous non-tautological clause learning procedure on benchmarks from QBFEVAL-12-SR.
2012
Gelder, Allen Van; Wood, Samuel B.; Lonsing, Florian
Extended Failed-Literal Preprocessing for Quantified Boolean Formulas Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, pp. 86–99, 2012.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/GelderWL12,
title = {Extended Failed-Literal Preprocessing for Quantified Boolean Formulas},
author = {Allen Van Gelder and Samuel B. Wood and Florian Lonsing},
url = {http://dx.doi.org/10.1007/978-3-642-31612-8_8},
doi = {10.1007/978-3-642-31612-8_8},
year = {2012},
date = {2012-01-01},
urldate = {2012-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2012 - 15th
International Conference, Trento, Italy, June 17-20, 2012. Proceedings},
pages = {86–99},
crossref = {DBLP:conf/sat/2012},
abstract = {Building on recent work that adapts failed-literal analysis (FL) to Quantified Boolean Formulas (QBF), this paper introduces extended failed-literal analysis (EFL). FL and EFL are both preprocessing methods that apply a fast, but incomplete reasoning procedure to abstractions of the underlying QBF. EFL extends FL by remembering certain binary clauses that are implied by the same reasoning procedure as FL when it assumes one literal and that implies a second literal. This extension is almost free because the second literals are implied anyway during FL, but compared to analogous techniques for propositional satisfiability, its correctness involves some subtleties. For the first time, application of the universal pure literal rule is considered without also applying the existential pure literal rule. It is shown that using both pure literal rules in EFL is unsound. A modified reasoning procedure for QBF, called Unit-clause Propagation with Universal Pure literals (UPUP) is described and correctness is proved for EFL based on UPUP. Empirical results on the 568-benchmark suite of QBFEVAL-10 are presented.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Building on recent work that adapts failed-literal analysis (FL) to Quantified Boolean Formulas (QBF), this paper introduces extended failed-literal analysis (EFL). FL and EFL are both preprocessing methods that apply a fast, but incomplete reasoning procedure to abstractions of the underlying QBF. EFL extends FL by remembering certain binary clauses that are implied by the same reasoning procedure as FL when it assumes one literal and that implies a second literal. This extension is almost free because the second literals are implied anyway during FL, but compared to analogous techniques for propositional satisfiability, its correctness involves some subtleties. For the first time, application of the universal pure literal rule is considered without also applying the existential pure literal rule. It is shown that using both pure literal rules in EFL is unsound. A modified reasoning procedure for QBF, called Unit-clause Propagation with Universal Pure literals (UPUP) is described and correctness is proved for EFL based on UPUP. Empirical results on the 568-benchmark suite of QBFEVAL-10 are presented.
Niemetz, Aina; Preiner, Mathias; Lonsing, Florian; Seidl, Martina; Biere, Armin
Resolution-Based Certificate Extraction for QBF - (Tool Presentation) Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, pp. 430–435, 2012.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/NiemetzPLSB12,
title = {Resolution-Based Certificate Extraction for QBF - (Tool Presentation)},
author = {Aina Niemetz and Mathias Preiner and Florian Lonsing and Martina Seidl and Armin Biere},
url = {http://dx.doi.org/10.1007/978-3-642-31612-8_33},
doi = {10.1007/978-3-642-31612-8_33},
year = {2012},
date = {2012-01-01},
urldate = {2012-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2012 - 15th
International Conference, Trento, Italy, June 17-20, 2012. Proceedings},
pages = {430–435},
crossref = {DBLP:conf/sat/2012},
abstract = {A certificate of (un)satisfiability for a quantified Boolean formula (QBF) represents sets of assignments to the variables, which act as witnesses for its truth value. Certificates are highly requested for practical applications of QBF like formal verification and model checking. We present an integrated set of tools realizing resolution-based certificate extraction for QBF in prenex conjunctive normal form. Starting from resolution proofs produced by the solver DepQBF, we describe the workflow consisting of proof checking, certificate extraction, and certificate checking. We implemented the steps of that workflow in stand-alone tools and carried out comprehensive experiments. Our results demonstrate the practical applicability of resolution-based certificate extraction.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
A certificate of (un)satisfiability for a quantified Boolean formula (QBF) represents sets of assignments to the variables, which act as witnesses for its truth value. Certificates are highly requested for practical applications of QBF like formal verification and model checking. We present an integrated set of tools realizing resolution-based certificate extraction for QBF in prenex conjunctive normal form. Starting from resolution proofs produced by the solver DepQBF, we describe the workflow consisting of proof checking, certificate extraction, and certificate checking. We implemented the steps of that workflow in stand-alone tools and carried out comprehensive experiments. Our results demonstrate the practical applicability of resolution-based certificate extraction.
Lonsing, Florian
Dependency Schemes and Search-Based QBF Solving: Theory and Practice PhD Thesis
Johannes Kepler University, Linz, Austria, 2012.
Abstract | Links | BibTeX | Tags:
@phdthesis{PhDLonsing,
title = {Dependency Schemes and Search-Based QBF Solving: Theory and Practice},
author = {Florian Lonsing},
url = {https://wp.florianlonsing.com/wp-content/uploads/2024/01/Lonsing-PhD-Thesis-2012.pdf
https://permalink.obvsg.at/AC07813151},
year = {2012},
date = {2012-01-01},
urldate = {2012-01-01},
school = {Johannes Kepler University, Linz, Austria},
abstract = {The logic of quantified Boolean formulae (QBF) extends propositional logic with universal quantification over propositional variables. The presence of universal quantifiers in QBF does not add expressiveness, but often allows for more compact encodings of problems. From a theoretical point of view, the decision problems of propositional logic (SAT) and QBF are NP-complete and PSPACE-complete, respectively. Compared to SAT, which successfully has been used for practical applications in model checking or formal verification, for example, empirical studies show that current approaches to QBF solving do not scale well in practice.
The quantifier prefix of QBFs in prenex conjunctive normal form (PCNF) imposes a linear ordering on the variables. In general, the ordering of the prefix gives rise to dependencies between variables which are differently quantified. Variable dependencies restrict the freedom of QBF solvers and must be respected during semantical evaluation to avoid incorrect results.
We consider dependency schemes, which were introduced in related work, to overcome the drawbacks of quantifier prefixes in PCNFs. A dependency scheme is a binary relation over the set of variables of a PCNF which expresses independence between variables. If two variables are independent then a search-based QBF solver can safely assign them in arbitrary order. Thus independence increases the freedom for QBF solvers.
We analyze theoretical properties of different dependency schemes which can be computed by analyzing the syntactic structure of a PCNF. We show that the common approach of mini-scoping is not optimal among syntactic methods of dependency analysis. As an alternative, we introduce specific approaches to compute and represent the standard dependency scheme efficiently. As a byproduct, we obtain compact dependency graphs as a representation of arbitrary dependency schemes. A main contribution of this work is the combination of arbitrary dependency schemes and search-based QBF solvers relying on the QDPLL algorithm. This way, QDPLL can profit from independence of variables which otherwise is hidden by the quantifier prefix. We implemented the solver DepQBF which tightly integrates dependency schemes. Experimental results confirm the potential benefits for practical QBF solving in contrast to quantifier prefixes. Our results motivate further research on dependency schemes for applications in QBF solving.},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
The logic of quantified Boolean formulae (QBF) extends propositional logic with universal quantification over propositional variables. The presence of universal quantifiers in QBF does not add expressiveness, but often allows for more compact encodings of problems. From a theoretical point of view, the decision problems of propositional logic (SAT) and QBF are NP-complete and PSPACE-complete, respectively. Compared to SAT, which successfully has been used for practical applications in model checking or formal verification, for example, empirical studies show that current approaches to QBF solving do not scale well in practice.
The quantifier prefix of QBFs in prenex conjunctive normal form (PCNF) imposes a linear ordering on the variables. In general, the ordering of the prefix gives rise to dependencies between variables which are differently quantified. Variable dependencies restrict the freedom of QBF solvers and must be respected during semantical evaluation to avoid incorrect results.
We consider dependency schemes, which were introduced in related work, to overcome the drawbacks of quantifier prefixes in PCNFs. A dependency scheme is a binary relation over the set of variables of a PCNF which expresses independence between variables. If two variables are independent then a search-based QBF solver can safely assign them in arbitrary order. Thus independence increases the freedom for QBF solvers.
We analyze theoretical properties of different dependency schemes which can be computed by analyzing the syntactic structure of a PCNF. We show that the common approach of mini-scoping is not optimal among syntactic methods of dependency analysis. As an alternative, we introduce specific approaches to compute and represent the standard dependency scheme efficiently. As a byproduct, we obtain compact dependency graphs as a representation of arbitrary dependency schemes. A main contribution of this work is the combination of arbitrary dependency schemes and search-based QBF solvers relying on the QDPLL algorithm. This way, QDPLL can profit from independence of variables which otherwise is hidden by the quantifier prefix. We implemented the solver DepQBF which tightly integrates dependency schemes. Experimental results confirm the potential benefits for practical QBF solving in contrast to quantifier prefixes. Our results motivate further research on dependency schemes for applications in QBF solving.
The quantifier prefix of QBFs in prenex conjunctive normal form (PCNF) imposes a linear ordering on the variables. In general, the ordering of the prefix gives rise to dependencies between variables which are differently quantified. Variable dependencies restrict the freedom of QBF solvers and must be respected during semantical evaluation to avoid incorrect results.
We consider dependency schemes, which were introduced in related work, to overcome the drawbacks of quantifier prefixes in PCNFs. A dependency scheme is a binary relation over the set of variables of a PCNF which expresses independence between variables. If two variables are independent then a search-based QBF solver can safely assign them in arbitrary order. Thus independence increases the freedom for QBF solvers.
We analyze theoretical properties of different dependency schemes which can be computed by analyzing the syntactic structure of a PCNF. We show that the common approach of mini-scoping is not optimal among syntactic methods of dependency analysis. As an alternative, we introduce specific approaches to compute and represent the standard dependency scheme efficiently. As a byproduct, we obtain compact dependency graphs as a representation of arbitrary dependency schemes. A main contribution of this work is the combination of arbitrary dependency schemes and search-based QBF solvers relying on the QDPLL algorithm. This way, QDPLL can profit from independence of variables which otherwise is hidden by the quantifier prefix. We implemented the solver DepQBF which tightly integrates dependency schemes. Experimental results confirm the potential benefits for practical QBF solving in contrast to quantifier prefixes. Our results motivate further research on dependency schemes for applications in QBF solving.
Seidl, Martina; Lonsing, Florian; Biere, Armin
qbf2epr: A Tool for Generating EPR Formulas from QBF Proceedings Article
In: Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, June 30 - July 1, 2012, pp. 139–148, 2012.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/cade/SeidlLB12,
title = {qbf2epr: A Tool for Generating EPR Formulas from QBF},
author = {Martina Seidl and Florian Lonsing and Armin Biere},
url = {https://easychair.org/publications/paper/nW
https://wp.florianlonsing.com/wp-content/uploads/2024/01/SeidlLonsingBiere-PAAR12.pdf},
year = {2012},
date = {2012-01-01},
urldate = {2012-01-01},
booktitle = {Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012,
Manchester, UK, June 30 - July 1, 2012},
pages = {139–148},
crossref = {DBLP:conf/cade/2012paar},
abstract = {We present the tool qbf2epr which translates quantified Boolean formulas (QBF) to formulas in effectively propositional logic (EPR). The decision problem of QBF is the prototypical problem for PSPACE, whereas EPR is NEXPTIME-complete. Thus QBF is embedded in a formalism, which is potentially more succinct. The motivation for this workis twofold. On the one hand, our tool generates challenging benchmarks for EPR solvers. On the other hand, we are interested in how EPR solvers perform compared to QBF solvers and if there are techniques implemented in EPR solvers which would also be valuable in QBF solvers and vice versa.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
We present the tool qbf2epr which translates quantified Boolean formulas (QBF) to formulas in effectively propositional logic (EPR). The decision problem of QBF is the prototypical problem for PSPACE, whereas EPR is NEXPTIME-complete. Thus QBF is embedded in a formalism, which is potentially more succinct. The motivation for this workis twofold. On the one hand, our tool generates challenging benchmarks for EPR solvers. On the other hand, we are interested in how EPR solvers perform compared to QBF solvers and if there are techniques implemented in EPR solvers which would also be valuable in QBF solvers and vice versa.
2011
Biere, Armin; Lonsing, Florian; Seidl, Martina
Blocked Clause Elimination for QBF Proceedings Article
In: Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, pp. 101–115, 2011.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/cade/BiereLS11,
title = {Blocked Clause Elimination for QBF},
author = {Armin Biere and Florian Lonsing and Martina Seidl},
url = {http://dx.doi.org/10.1007/978-3-642-22438-6_10},
doi = {10.1007/978-3-642-22438-6_10},
year = {2011},
date = {2011-01-01},
urldate = {2011-01-01},
booktitle = {Automated Deduction - CADE-23 - 23rd International Conference on
Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
pages = {101–115},
crossref = {DBLP:conf/cade/2011},
abstract = {Quantified Boolean formulas (QBF) provide a powerful framework for encoding problems from various application domains, not least because efficient QBF solvers are available. Despite sophisticated evaluation techniques, the performance of such a solver usually depends on the way a problem is represented. However, the translation to processable QBF encodings is in general not unique and may either introduce variables and clauses not relevant for the solving process or blur information which could be beneficial for the solving process. To deal with both of these issues, preprocessors have been introduced which rewrite a given QBF before it is passed to a solver.
In this paper, we present novel preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques as BCE in SAT. We have implemented QBCE and extensions of QBCE in the preprocessor bloqqer. In our experiments we show that preprocessing with QBCE reduces formulas substantially and allows us to solve considerable more instances than the previous state-of-the-art.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Quantified Boolean formulas (QBF) provide a powerful framework for encoding problems from various application domains, not least because efficient QBF solvers are available. Despite sophisticated evaluation techniques, the performance of such a solver usually depends on the way a problem is represented. However, the translation to processable QBF encodings is in general not unique and may either introduce variables and clauses not relevant for the solving process or blur information which could be beneficial for the solving process. To deal with both of these issues, preprocessors have been introduced which rewrite a given QBF before it is passed to a solver.
In this paper, we present novel preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques as BCE in SAT. We have implemented QBCE and extensions of QBCE in the preprocessor bloqqer. In our experiments we show that preprocessing with QBCE reduces formulas substantially and allows us to solve considerable more instances than the previous state-of-the-art.
In this paper, we present novel preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques as BCE in SAT. We have implemented QBCE and extensions of QBCE in the preprocessor bloqqer. In our experiments we show that preprocessing with QBCE reduces formulas substantially and allows us to solve considerable more instances than the previous state-of-the-art.
Lonsing, Florian; Biere, Armin
Failed Literal Detection for QBF Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, pp. 259–272, 2011.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingB11,
title = {Failed Literal Detection for QBF},
author = {Florian Lonsing and Armin Biere},
url = {http://dx.doi.org/10.1007/978-3-642-21581-0_21
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingBiere-SAT11.pdf},
doi = {10.1007/978-3-642-21581-0_21},
year = {2011},
date = {2011-01-01},
urldate = {2011-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2011 - 14th
International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22,
2011. Proceedings},
pages = {259–272},
crossref = {DBLP:conf/sat/2011},
abstract = {Failed literal detection (FL) in SAT is a powerful approach for preprocessing. The basic idea is to assign a variable as assumption. If boolean constraint propagation (BCP) yields an empty clause then the negated assumption is necessary for satisfiability. Whereas FL is common in SAT, it cannot easily be applied to QBF due to universal quantification. We present two approaches for FL to preprocess prenex CNFs. The first one is based on abstraction where certain universal variables are treated as existentially quantified. Second we combine QBF-specific BCP (QBCP) in FL with Q-resolution to validate assignments learnt by FL. Finally we compare these two approaches to a third common approach based on SAT. It turns out that the three approaches are incomparable. Experimental evaluation demonstrates that FL for QBF can improve the performance of search- and elimination-based QBF solvers.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Failed literal detection (FL) in SAT is a powerful approach for preprocessing. The basic idea is to assign a variable as assumption. If boolean constraint propagation (BCP) yields an empty clause then the negated assumption is necessary for satisfiability. Whereas FL is common in SAT, it cannot easily be applied to QBF due to universal quantification. We present two approaches for FL to preprocess prenex CNFs. The first one is based on abstraction where certain universal variables are treated as existentially quantified. Second we combine QBF-specific BCP (QBCP) in FL with Q-resolution to validate assignments learnt by FL. Finally we compare these two approaches to a third common approach based on SAT. It turns out that the three approaches are incomparable. Experimental evaluation demonstrates that FL for QBF can improve the performance of search- and elimination-based QBF solvers.
2010
Brummayer, Robert; Lonsing, Florian; Biere, Armin
Automated Testing and Debugging of SAT and QBF Solvers Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 44–57, 2010.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/BrummayerLB10,
title = {Automated Testing and Debugging of SAT and QBF Solvers},
author = {Robert Brummayer and Florian Lonsing and Armin Biere},
url = {http://dx.doi.org/10.1007/978-3-642-14186-7_6
https://wp.florianlonsing.com/wp-content/uploads/2024/01/BrummayerLonsingBiere-SAT10.pdf},
doi = {10.1007/978-3-642-14186-7_6},
year = {2010},
date = {2010-01-01},
urldate = {2010-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2010, 13th
International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010.
Proceedings},
pages = {44–57},
crossref = {DBLP:conf/sat/2010},
abstract = {Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.
Lonsing, Florian; Biere, Armin
Integrating Dependency Schemes in Search-Based QBF Solvers Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 158–171, 2010.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingB10,
title = {Integrating Dependency Schemes in Search-Based QBF Solvers},
author = {Florian Lonsing and Armin Biere},
url = {http://dx.doi.org/10.1007/978-3-642-14186-7_14
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingBiere-SAT10-errata.txt
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingBiere-SAT10.pdf},
doi = {10.1007/978-3-642-14186-7_14},
year = {2010},
date = {2010-01-01},
urldate = {2010-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2010, 13th
International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010.
Proceedings},
pages = {158–171},
crossref = {DBLP:conf/sat/2010},
abstract = {Many search-based QBF solvers implementing the DPLL algorithm for QBF (QDPLL) process formulae in prenex conjunctive normal form (PCNF). The quantifier prefix of PCNFs often results in strong variable dependencies which can influence solver performance negatively. A common approach to overcome this problem is to reconstruct quantifier structure e.g. by quantifier trees. Dependency schemes are a generalization of quantifier trees in the sense that more general dependency graphs can be obtained. So far, dependency graphs have not been applied in QBF solving. In this work we consider the problem of efficiently integrating dependency graphs in QDPLL. Thereby we generalize related work on integrating quantifier trees. By analyzing the core parts of QDPLL, we report on modifications necessary to profit from general dependency graphs. In comprehensive experiments we show that QDPLL using a particular dependency graph, despite of increased overhead, outperforms classical QDPLL relying on quantifier prefixes of PCNFs.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Many search-based QBF solvers implementing the DPLL algorithm for QBF (QDPLL) process formulae in prenex conjunctive normal form (PCNF). The quantifier prefix of PCNFs often results in strong variable dependencies which can influence solver performance negatively. A common approach to overcome this problem is to reconstruct quantifier structure e.g. by quantifier trees. Dependency schemes are a generalization of quantifier trees in the sense that more general dependency graphs can be obtained. So far, dependency graphs have not been applied in QBF solving. In this work we consider the problem of efficiently integrating dependency graphs in QDPLL. Thereby we generalize related work on integrating quantifier trees. By analyzing the core parts of QDPLL, we report on modifications necessary to profit from general dependency graphs. In comprehensive experiments we show that QDPLL using a particular dependency graph, despite of increased overhead, outperforms classical QDPLL relying on quantifier prefixes of PCNFs.
Lonsing, Florian; Biere, Armin
DepQBF: A Dependency-Aware QBF Solver Journal Article
In: Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 7, no. 2-3, pp. 71–76, 2010.
Abstract | Links | BibTeX | Tags:
@article{DBLP:journals/jsat/LonsingB10,
title = {DepQBF: A Dependency-Aware QBF Solver},
author = {Florian Lonsing and Armin Biere},
url = {https://content.iospress.com/articles/journal-on-satisfiability-boolean-modeling-and-computation/sat190077},
year = {2010},
date = {2010-01-01},
urldate = {2010-01-01},
journal = {Journal on Satisfiability, Boolean Modeling and Computation (JSAT)},
volume = {7},
number = {2-3},
pages = {71–76},
abstract = {We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quantifier prefixes of QBFs in prenex conjunctive normal form (PCNF). DepQBF 0.1 was placed first in the main track of QBFEVAL’10 in a score-based ranking. We provide a general system overview and describe selected orthogonal features such as restarts and removal of learnt constraints.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quantifier prefixes of QBFs in prenex conjunctive normal form (PCNF). DepQBF 0.1 was placed first in the main track of QBFEVAL’10 in a score-based ranking. We provide a general system overview and describe selected orthogonal features such as restarts and removal of learnt constraints.
2009
Lonsing, Florian; Biere, Armin
A Compact Representation for Syntactic Dependencies in QBFs Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, pp. 398–411, 2009.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingB09,
title = {A Compact Representation for Syntactic Dependencies in QBFs},
author = {Florian Lonsing and Armin Biere},
url = {http://dx.doi.org/10.1007/978-3-642-02777-2_37
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingBiere-SAT09.pdf},
doi = {10.1007/978-3-642-02777-2_37},
year = {2009},
date = {2009-01-01},
urldate = {2009-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2009, 12th
International Conference, SAT 2009, Swansea, UK, June 30 - July
3, 2009. Proceedings},
pages = {398–411},
crossref = {DBLP:conf/sat/2009},
abstract = {Different quantifier types in Quantified Boolean Formulae (QBF) introduce variable dependencies which have to be taken into consideration when deciding satisfiability of a QBF. In this work, we focus on dependencies based on syntactically connected variables. We generalize our previous ideas for efficiently representing dependency sets of universal variables to existential ones. We obtain a dependency graph which is applicable to arbitrary QBF solvers. The core part of our work is the formulation and correctness proof of a static and compact, tree-shaped connection relation over equivalence classes of existential variables. In practice, this relation is constructed once from a given QBF and allows to share connection information among all variables. We report on practical aspects and demonstrate the effectiveness of our approach in experiments on structured formulae from QBF competitions. Further, we show by example that the common approach of quantifier scope analysis is not optimal among syntactic methods for dependency computation.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Different quantifier types in Quantified Boolean Formulae (QBF) introduce variable dependencies which have to be taken into consideration when deciding satisfiability of a QBF. In this work, we focus on dependencies based on syntactically connected variables. We generalize our previous ideas for efficiently representing dependency sets of universal variables to existential ones. We obtain a dependency graph which is applicable to arbitrary QBF solvers. The core part of our work is the formulation and correctness proof of a static and compact, tree-shaped connection relation over equivalence classes of existential variables. In practice, this relation is constructed once from a given QBF and allows to share connection information among all variables. We report on practical aspects and demonstrate the effectiveness of our approach in experiments on structured formulae from QBF competitions. Further, we show by example that the common approach of quantifier scope analysis is not optimal among syntactic methods for dependency computation.
Lonsing, Florian; Biere, Armin
Efficiently Representing Existential Dependency Sets for Expansion-Based QBF Solvers Journal Article
In: Electr. Notes Theor. Comput. Sci., vol. 251, pp. 83–95, 2009.
Abstract | Links | BibTeX | Tags:
@article{DBLP:journals/entcs/LonsingB09,
title = {Efficiently Representing Existential Dependency Sets for Expansion-Based QBF Solvers},
author = {Florian Lonsing and Armin Biere},
url = {http://dx.doi.org/10.1016/j.entcs.2009.08.029},
doi = {10.1016/j.entcs.2009.08.029},
year = {2009},
date = {2009-01-01},
urldate = {2009-01-01},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {251},
pages = {83–95},
abstract = {Given a quantified boolean formula (QBF) in prenex conjunctive normal form (PCNF), we consider the problem of identifying variable dependencies. In related work, a formal definition of dependencies has been suggested based on quantifier prefix reordering: two variables are independent if swapping them in the prefix does not change satisfiability of the formula. Instead of the general case, we focus on the sets of depending existential variables for all universal variables. This is relevant particularly for expansion-based QBF solvers. We present an approach for efficiently computing existential dependency sets by means of a directed connection relation over variables and demonstrate how this relation can be compactly represented as a tree using a union-find data structure. Experimental results show the effectiveness of our approach.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Given a quantified boolean formula (QBF) in prenex conjunctive normal form (PCNF), we consider the problem of identifying variable dependencies. In related work, a formal definition of dependencies has been suggested based on quantifier prefix reordering: two variables are independent if swapping them in the prefix does not change satisfiability of the formula. Instead of the general case, we focus on the sets of depending existential variables for all universal variables. This is relevant particularly for expansion-based QBF solvers. We present an approach for efficiently computing existential dependency sets by means of a directed connection relation over variables and demonstrate how this relation can be compactly represented as a tree using a union-find data structure. Experimental results show the effectiveness of our approach.
2008
Lonsing, Florian; Biere, Armin
Nenofex: Expanding NNF for QBF Solving Proceedings Article
In: Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, pp. 196–210, 2008.
Abstract | Links | BibTeX | Tags:
@inproceedings{DBLP:conf/sat/LonsingB08,
title = {Nenofex: Expanding NNF for QBF Solving},
author = {Florian Lonsing and Armin Biere},
url = {http://dx.doi.org/10.1007/978-3-540-79719-7_19
https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingBiere-SAT08.pdf},
doi = {10.1007/978-3-540-79719-7_19},
year = {2008},
date = {2008-01-01},
urldate = {2008-01-01},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2008, 11th
International Conference, SAT 2008, Guangzhou, China, May 12-15,
2008. Proceedings},
pages = {196–210},
crossref = {DBLP:conf/sat/2008},
abstract = {The topic of this paper is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form (NNF), which relies on expansion as the core technique for eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes the formula size to increase quadratically in the worst case, expansion on NNF is involved with only a linear increase of the formula size. This property motivates the use of NNF instead of CNF combined with expansion. In Nenofex, a formula in NNF is represented as a tree with structural restrictions in order to keep its size small and distances from nodes to the root short. Expansions of variables are scheduled based on estimated expansion cost. The variable with the smallest estimated cost is expanded first. In order to remove redundancy from the formula, limited versions of two approaches from the domain of circuit optimization have been integrated. Experimental results on latest benchmarks show that Nenofex indeed exceeds a given memory limit less frequently than a resolution-based QBF solver for CNF, but also that there is the need for runtime-related improvements.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
The topic of this paper is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form (NNF), which relies on expansion as the core technique for eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes the formula size to increase quadratically in the worst case, expansion on NNF is involved with only a linear increase of the formula size. This property motivates the use of NNF instead of CNF combined with expansion. In Nenofex, a formula in NNF is represented as a tree with structural restrictions in order to keep its size small and distances from nodes to the root short. Expansions of variables are scheduled based on estimated expansion cost. The variable with the smallest estimated cost is expanded first. In order to remove redundancy from the formula, limited versions of two approaches from the domain of circuit optimization have been integrated. Experimental results on latest benchmarks show that Nenofex indeed exceeds a given memory limit less frequently than a resolution-based QBF solver for CNF, but also that there is the need for runtime-related improvements.
Lonsing, Florian
An Expansion-Based QBF Solver for Negation Normal Form Masters Thesis
Johannes Kepler University, Linz, Austria, 2008.
Abstract | Links | BibTeX | Tags:
@mastersthesis{MScLonsing,
title = {An Expansion-Based QBF Solver for Negation Normal Form},
author = {Florian Lonsing},
url = {https://wp.florianlonsing.com/wp-content/uploads/2024/01/Lonsing-nenofex-master-thesis-2008.pdf},
year = {2008},
date = {2008-01-01},
urldate = {2008-01-01},
school = {Johannes Kepler University, Linz, Austria},
abstract = {The topic of this master thesis is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form (NNF), which relies on expansion as the core technique for eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes the formula size to increase quadratically in the worst case, expansion on NNF is involved with only a linear increase of the formula size. This property motivates the use of NNF instead of CNF combined with expansion. In Nenofex, a formula in NNF is represented as a tree with structural restrictions in order to keep its size small and distances from nodes to the root short. Expansions of variables are scheduled based on estimated expansion costs. The variable with the smallest estimated costs is expanded first. In order to remove redundancy from the formula, limited versions of two approaches from the domain of circuit optimization have been integrated. Experimental results show that Nenofex indeed exceeds a given memory limit less frequently than a resolution-based QBF solver for CNF, but also that there is still room for runtime improvements.},
keywords = {},
pubstate = {published},
tppubtype = {mastersthesis}
}
The topic of this master thesis is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form (NNF), which relies on expansion as the core technique for eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes the formula size to increase quadratically in the worst case, expansion on NNF is involved with only a linear increase of the formula size. This property motivates the use of NNF instead of CNF combined with expansion. In Nenofex, a formula in NNF is represented as a tree with structural restrictions in order to keep its size small and distances from nodes to the root short. Expansions of variables are scheduled based on estimated expansion costs. The variable with the smallest estimated costs is expanded first. In order to remove redundancy from the formula, limited versions of two approaches from the domain of circuit optimization have been integrated. Experimental results show that Nenofex indeed exceeds a given memory limit less frequently than a resolution-based QBF solver for CNF, but also that there is still room for runtime improvements.
Lonsing, Florian; Biere, Armin
Efficiently Representing Existential Dependency Sets for Expansion-Based QBF Solvers Proceedings Article
In: Proceedings of the 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS), Znojmo, Czech Republic, November 14-16, 2008, pp. 148–155, 2008.
Abstract | Links | BibTeX | Tags:
@inproceedings{LonsingBiereMEMICS08,
title = {Efficiently Representing Existential Dependency Sets for Expansion-Based QBF Solvers},
author = {Florian Lonsing and Armin Biere},
url = {https://wp.florianlonsing.com/wp-content/uploads/2024/01/LonsingBiere-MEMICS08.pdf},
year = {2008},
date = {2008-01-01},
urldate = {2008-01-01},
booktitle = {Proceedings of the 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS), Znojmo, Czech Republic, November 14-16, 2008},
pages = {148–155},
abstract = {Given a quantified boolean formula (QBF) in prenex conjunctive normal form (PCNF), we consider the problem of identifying variable dependencies. In related work, a formal definition of dependencies has been suggested based on quantifier prefix reordering: two variables are independent if swapping them in the prefix does not change satisfiability of the formula. Instead of the general case, we focus on the sets of depending existential variables for all universal variables. This is relevant particularly for expansion-based QBF solvers. We present an approach for efficiently computing existential dependency sets by means of a directed connection relation over variables and demonstrate how this relation can be compactly represented as a tree using a union-find data structure. Experimental results show the effectiveness of our approach.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
Given a quantified boolean formula (QBF) in prenex conjunctive normal form (PCNF), we consider the problem of identifying variable dependencies. In related work, a formal definition of dependencies has been suggested based on quantifier prefix reordering: two variables are independent if swapping them in the prefix does not change satisfiability of the formula. Instead of the general case, we focus on the sets of depending existential variables for all universal variables. This is relevant particularly for expansion-based QBF solvers. We present an approach for efficiently computing existential dependency sets by means of a directed connection relation over variables and demonstrate how this relation can be compactly represented as a tree using a union-find data structure. Experimental results show the effectiveness of our approach.
Brummayer, Robert; Biere, Armin; Lonsing, Florian
BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking Proceedings Article
In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, pp. 33–38, ACM, Princeton, New Jersey, USA, 2008, ISBN: 978-1-60558-440-9.
Abstract | Links | BibTeX | Tags:
@inproceedings{Brummayer:2008:BBM:1512464.1512472,
title = {BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking},
author = {Robert Brummayer and Armin Biere and Florian Lonsing},
url = {http://doi.acm.org/10.1145/1512464.1512472
https://wp.florianlonsing.com/wp-content/uploads/2024/01/BrummayerBiereLonsing-BPR08.pdf},
doi = {10.1145/1512464.1512472},
isbn = {978-1-60558-440-9},
year = {2008},
date = {2008-01-01},
urldate = {2008-01-01},
booktitle = {Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning},
pages = {33–38},
publisher = {ACM},
address = {Princeton, New Jersey, USA},
series = {SMT'08/BPR'08},
abstract = {This is a proposal for a bit-precise word-level format, called BTOR. It is easy to parse and has precise semantics. In its basic form it allows to model SMT problems over the quantifier-free theory of bit-vectors in combination with one-dimensional arrays. Our main contribution is a sequential extension that can be used to capture model checking problems on the word-level. We present two case studies where BTOR is used as sequential format. Finally, we report on experimental results for the model checking extension of our SMT solver Boolector.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
This is a proposal for a bit-precise word-level format, called BTOR. It is easy to parse and has precise semantics. In its basic form it allows to model SMT problems over the quantifier-free theory of bit-vectors in combination with one-dimensional arrays. Our main contribution is a sequential extension that can be used to capture model checking problems on the word-level. We present two case studies where BTOR is used as sequential format. Finally, we report on experimental results for the model checking extension of our SMT solver Boolector.