@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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/abs/1904.12927},

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}

}

@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/abs/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}

}

@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/abs/1701.06612},

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}

}

@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/abs/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}

}

@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/abs/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}

}

@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/abs/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}

}

@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/abs/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}

}

@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/abs/1506.08563},

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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}

@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}

}