| Publication | Date of Publication | Type |
|---|
| CaDiCaL 2.2 System Description Artifact | 2025-02-25 | Dataset |
| HWMCC'24 Benchmarks and Results | 2025-01-30 | Dataset |
| Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker | 2025-01-13 | Paper |
| On enumerating short projected models | 2025-01-06 | Paper |
| IPASIR-up: user propagators for CDCL | 2024-11-26 | Paper |
| Cadiback: Extracting backbones with CaDiCaL | 2024-11-26 | Paper |
| Faster LRAT checking than solving with CaDiCaL | 2024-11-26 | Paper |
| Migrating solver state | 2024-07-12 | Paper |
| Certified SAT solving with GPU accelerated inprocessing | 2024-06-28 | Paper |
| Clausal Congruence Closure Paper Source Code | 2024-06-14 | Dataset |
| Clausal Congruence Closure Paper Logs, Plots and Tables | 2024-06-14 | Dataset |
| SAT Race 2010 Benchmarks | 2024-06-11 | Dataset |
| SAT Competition 2009 Application Track Benchmarks | 2024-06-11 | Dataset |
| SAT Race 2008 Benchmarks | 2024-06-11 | Dataset |
| SAT Competition 2007 Industrial Track Benchmarks | 2024-06-11 | Dataset |
| SAT Race 2006 Benchmarks | 2024-06-11 | Dataset |
| Distributed SAT Competition 2005 Industrial Track Benchmarks | 2024-06-11 | Dataset |
| Distributed SAT Competition 2004 Industrial Track Benchmarks | 2024-06-11 | Dataset |
| Distributed SAT Competition 2003 Industrial Track Benchmarks | 2024-06-11 | Dataset |
| Distributed SAT Competition 2002 Industrial Track Benchmarks | 2024-06-11 | Dataset |
| SAT Competition 2014 Application Track Benchmarks | 2024-06-08 | Dataset |
| SAT Competition 2013 Application Track Benchmarks | 2024-06-08 | Dataset |
| SAT Challenge 2012 Application Track Benchmarks | 2024-06-08 | Dataset |
| SAT Competition 2011 Application Track Benchmarks | 2024-06-08 | Dataset |
| SAT Competition 2021 Main Track Benchmarks | 2024-06-02 | Dataset |
| SAT Competition 2020 Main Track Benchmarks | 2024-06-02 | Dataset |
| SAT Competition 2022 Main Track Benchmarks | 2024-06-02 | Dataset |
| SAT Race 2019 Benchmarks | 2024-06-02 | Dataset |
| SAT Competition 2018 Main Track Benchmarks | 2024-06-02 | Dataset |
| SAT Competition 2016 Application Track Benchmarks | 2024-06-02 | Dataset |
| SAT Competition 2017 Main Track Benchmarks | 2024-06-02 | Dataset |
| SAT Race 2015 Benchmarks | 2024-06-02 | Dataset |
| SAT Competition 2023 Main Track Benchmarks | 2024-06-02 | Dataset |
| CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2020 Models | 2024-05-16 | Dataset |
| Clausal Equivalence Sweeping Paper Logs | 2024-05-16 | Dataset |
| CNF Encoded Hard Miters from IWLS'22 Paper | 2024-03-15 | Dataset |
| CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2012 Models | 2024-03-15 | Dataset |
| Clausal proofs for pseudo-Boolean reasoning | 2024-01-23 | Paper |
| Encoding Redundancy for Satisfaction-Driven Clause Learning | 2023-11-24 | Paper |
| Mining definitions in Kissat with Kittens | 2023-10-30 | Paper |
| The SAT Museum POS'23 Artifact | 2023-10-24 | Dataset |
| Sampled and Normalized Satisfiable Instances from the main track of the SAT Competition 2004 to 2022 | 2023-03-19 | Dataset |
| 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 |
| Artifact for Paper ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving | 2022-11-07 | Dataset |
| 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 |
| Distributed cube and conquer with Paracooba | 2021-04-07 | Paper |
| Four flavors of entailment | 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 |
| Compositional Propositional Proofs | 2016-01-12 | Paper |
| Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination | 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 |
| A Unified Proof System for QBF Preprocessing | 2014-09-26 | 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 |
| 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 |
| Liveness checking as safety checking for infinite state spaces | 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 |
| Failed Literal Detection for QBF | 2011-06-17 | Paper |
| Efficient CNF Simplification Based on Binary Implication Graphs | 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 |
| Nenofex: Expanding NNF for QBF Solving | 2008-05-27 | Paper |
| Adaptive Restart Strategies for Conflict Driven SAT Solvers | 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 |
