| Publication | Date of Publication | Type |
|---|
| Encoding Redundancy for Satisfaction-Driven Clause Learning | 2023-11-24 | Paper |
| Mining definitions in Kissat with Kittens | 2023-10-30 | Paper |
| Nullstellensatz-proofs for multiplier verification | 2022-12-21 | Paper |
| Duplex encoding of staircase at-most-one constraints for the antibandwidth problem | 2022-12-21 | Paper |
| Covered clauses are not propagation redundant | 2022-11-09 | Paper |
| Better Decision Heuristics in CDCL through Local Search and Target Phases | 2022-08-30 | Paper |
| Skolem Function Continuation for Quantified Boolean Formulas | 2022-07-01 | Paper |
| Progress in certifying hardware model checking results | 2022-03-25 | Paper |
| Efficient all-UIP learned clause minimization | 2022-03-22 | Paper |
| XOR local search for Boolean Brent equations | 2022-03-22 | Paper |
| Non-clausal redundancy properties | 2021-12-01 | Paper |
| Four flavors of entailment | 2021-04-07 | Paper |
| Distributed cube and conquer with Paracooba | 2021-04-07 | Paper |
| Incremental column-wise verification of arithmetic circuits using computer algebra | 2021-02-08 | Paper |
| Simulating strong practical proof systems with extended resolution | 2020-11-02 | Paper |
| Counterexample-Guided Model Synthesis | 2020-08-05 | Paper |
| Truth Assignments as Conditional Autarkies | 2020-07-20 | Paper |
| Incremental inprocessing in SAT solving | 2020-05-20 | Paper |
| Backing backtracking | 2020-05-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5219922 | 2020-03-09 | Paper |
| Strong extension-free proof systems | 2020-03-03 | Paper |
| What a difference a variable makes | 2019-09-16 | Paper |
| Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories | 2019-05-03 | Paper |
| Blocked Clauses in First-Order Logic | 2019-01-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4553279 | 2018-11-02 | Paper |
| SAT-Based Model Checking | 2018-07-20 | Paper |
| Propagation based local search for bit-precise reasoning | 2018-01-08 | Paper |
| Short proofs without new variables | 2017-09-22 | Paper |
| Solution validation and extraction for QBF preprocessing | 2017-07-10 | Paper |
| Complexity of fixed-size bit-vector logics | 2017-01-18 | Paper |
| SAT race 2015 | 2016-11-01 | Paper |
| Super-Blocked Clauses | 2016-09-05 | Paper |
| Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination | 2016-01-12 | Paper |
| Compositional Propositional Proofs | 2016-01-12 | Paper |
| Evaluating CDCL Variable Scoring Schemes | 2015-11-20 | Paper |
| Clause Elimination for SAT and QSAT | 2015-08-25 | Paper |
| On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic | 2014-10-14 | Paper |
| Detecting Cardinality Constraints in CNF | 2014-09-26 | Paper |
| Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses | 2014-09-26 | Paper |
| Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask) | 2014-09-26 | Paper |
| A Unified Proof System for QBF Preprocessing | 2014-09-26 | Paper |
| Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers | 2014-07-23 | Paper |
| Blocked Clause Decomposition | 2014-01-17 | Paper |
| Compressing BMC Encodings with QBF | 2013-12-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2852018 | 2013-10-07 | Paper |
| Factoring Out Assumptions to Speed Up MUS Extraction | 2013-08-05 | Paper |
| Simulating circuit-level simplifications on CNF | 2013-07-05 | Paper |
| bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR | 2013-06-14 | Paper |
| More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding | 2013-06-14 | Paper |
| Revisiting Hyper Binary Resolution | 2013-06-04 | Paper |
| Inprocessing Rules | 2012-09-05 | Paper |
| Blocked Clause Elimination for QBF | 2011-07-29 | Paper |
| Efficient CNF Simplification Based on Binary Implication Graphs | 2011-06-17 | Paper |
| Failed Literal Detection for QBF | 2011-06-17 | Paper |
| Clause Elimination Procedures for CNF Formulas | 2010-10-12 | Paper |
| Automated Testing and Debugging of SAT and QBF Solvers | 2010-09-29 | Paper |
| Integrating Dependency Schemes in Search-Based QBF Solvers | 2010-09-29 | Paper |
| Reconstructing Solutions after Blocked Clause Elimination | 2010-09-29 | Paper |
| Blocked Clause Elimination | 2010-04-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3181652 | 2009-10-12 | Paper |
| A Compact Representation for Syntactic Dependencies in QBFs | 2009-07-07 | Paper |
| A First Step Towards a Unified Proof Checker for QBF | 2009-03-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3604000 | 2009-02-24 | Paper |
| Tutorial on Model Checking: Modelling and Verification in Computer Science | 2009-02-03 | Paper |
| Adaptive Restart Strategies for Conflict Driven SAT Solvers | 2008-05-27 | Paper |
| Nenofex: Expanding NNF for QBF Solving | 2008-05-27 | Paper |
| Linear Encodings of Bounded LTL Model Checking | 2007-10-11 | Paper |
| Extended Resolution Proofs for Symbolic SAT Solving with Quantification | 2007-09-04 | Paper |
| Extended Resolution Proofs for Conjoining BDDs | 2007-05-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3429163 | 2007-03-30 | Paper |
| Automated Technology for Verification and Analysis | 2006-10-25 | Paper |
| Formal Methods in Computer-Aided Design | 2006-10-20 | Paper |
| Theory and Applications of Satisfiability Testing | 2005-12-16 | Paper |
| Theory and Applications of Satisfiability Testing | 2005-12-15 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2005-12-06 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2005-11-10 | Paper |
| Computer Aided Verification | 2005-08-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4817533 | 2004-09-24 | Paper |
| A satisfiability procedure for quantified Boolean formulae | 2003-09-15 | Paper |
| Verifying the IEEE 1394 fireWire tree identify protocol with SMV | 2003-08-27 | Paper |
| Verification of out-of-order processor designs using model Checking and a light-weight completion function | 2002-07-08 | Paper |
| Bounded model checking using satisfiability solving | 2002-05-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754079 | 2001-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4255565 | 1999-08-17 | Paper |
