| 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
Formal Methods in System Design | 2025-01-13 | Paper |
On enumerating short projected models
Discrete Applied Mathematics | 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
Formal Methods in System Design | 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
Tools and Algorithms for the Construction and Analysis of Systems | 2023-11-24 | Paper |
Mining definitions in Kissat with Kittens
Formal Methods in System Design | 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
Journal of Artificial Intelligence Research | 2022-08-30 | Paper |
Skolem function continuation for quantified Boolean formulas
Tests and Proofs | 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
Formal Methods in System Design | 2021-02-08 | Paper |
Simulating strong practical proof systems with extended resolution
Journal of Automated Reasoning | 2020-11-02 | Paper |
Counterexample-Guided Model Synthesis
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Truth assignments as conditional autarkies
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
| Incremental inprocessing in SAT solving | 2020-05-20 | Paper |
| Backing backtracking | 2020-05-20 | Paper |
| scientific article; zbMATH DE number 7178357 (Why is no real title available?) | 2020-03-09 | Paper |
Strong extension-free proof systems
Journal of Automated Reasoning | 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
Computer Aided Verification | 2019-05-03 | Paper |
Blocked clauses in first-order logic
EPiC Series in Computing | 2019-01-10 | Paper |
Local redundancy in SAT: generalizations of blocked clauses
(available as arXiv preprint) | 2018-11-02 | Paper |
SAT-Based Model Checking
Handbook of Model Checking | 2018-07-20 | Paper |
Propagation based local search for bit-precise reasoning
Formal Methods in System Design | 2018-01-08 | Paper |
| Short proofs without new variables | 2017-09-22 | Paper |
Solution validation and extraction for QBF preprocessing
Journal of Automated Reasoning | 2017-07-10 | Paper |
Complexity of fixed-size bit-vector logics
Theory of Computing Systems | 2017-01-18 | Paper |
SAT race 2015
Artificial Intelligence | 2016-11-01 | Paper |
Super-blocked clauses
Automated Reasoning | 2016-09-05 | Paper |
Compositional propositional proofs
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Enhancing search-based QBF solving by dynamic blocked clause elimination
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Evaluating CDCL variable scoring schemes
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Clause elimination for SAT and QSAT
Journal of Artificial Intelligence Research | 2015-08-25 | Paper |
On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Mathematical Foundations of Computer Science 2014 | 2014-10-14 | Paper |
A unified proof system for QBF preprocessing
Automated Reasoning | 2014-09-26 | Paper |
Detecting cardinality constraints in CNF
Lecture Notes in Computer Science | 2014-09-26 | Paper |
Improving implementation of SLS solvers for SAT and new heuristics for \(k\)-SAT with long clauses
Lecture Notes in Computer Science | 2014-09-26 | Paper |
Everything you always wanted to know about blocked sets (but were afraid to ask)
Lecture Notes in Computer Science | 2014-09-26 | Paper |
Efficiently representing existential dependency sets for expansion-based QBF solvers
Electronic Notes in Theoretical Computer Science | 2014-07-23 | Paper |
Blocked clause decomposition
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
Compressing BMC encodings with QBF
Electronic Notes in Theoretical Computer Science | 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
Theory and Applications of Satisfiability Testing – SAT 2013 | 2013-08-05 | Paper |
Simulating circuit-level simplifications on CNF
Journal of Automated Reasoning | 2013-07-05 | Paper |
bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
Computer Science – Theory and Applications | 2013-06-14 | Paper |
Revisiting hyper binary resolution
Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems | 2013-06-04 | Paper |
Inprocessing rules
Automated Reasoning | 2012-09-05 | Paper |
Blocked clause elimination for QBF
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Failed literal detection for QBF
Theory and Applications of Satisfiability Testing - SAT 2011 | 2011-06-17 | Paper |
Efficient CNF simplification based on binary implication graphs
Theory and Applications of Satisfiability Testing - SAT 2011 | 2011-06-17 | Paper |
Clause elimination procedures for CNF formulas
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Automated testing and debugging of SAT and QBF solvers
Theory and Applications of Satisfiability Testing – SAT 2010 | 2010-09-29 | Paper |
Integrating dependency schemes in search-based QBF solvers
Theory and Applications of Satisfiability Testing – SAT 2010 | 2010-09-29 | Paper |
Reconstructing solutions after blocked clause elimination
Theory and Applications of Satisfiability Testing – SAT 2010 | 2010-09-29 | Paper |
Blocked clause elimination
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
| scientific article; zbMATH DE number 5613976 (Why is no real title available?) | 2009-10-12 | Paper |
A Compact Representation for Syntactic Dependencies in QBFs
Lecture Notes in Computer Science | 2009-07-07 | Paper |
A First Step Towards a Unified Proof Checker for QBF
Theory and Applications of Satisfiability Testing – SAT 2007 | 2009-03-10 | Paper |
| scientific article; zbMATH DE number 5510691 (Why is no real title available?) | 2009-02-24 | Paper |
Tutorial on Model Checking: Modelling and Verification in Computer Science
Algebraic Biology | 2009-02-03 | Paper |
Nenofex: Expanding NNF for QBF Solving
Theory and Applications of Satisfiability Testing – SAT 2008 | 2008-05-27 | Paper |
Adaptive Restart Strategies for Conflict Driven SAT Solvers
Theory and Applications of Satisfiability Testing – SAT 2008 | 2008-05-27 | Paper |
Linear Encodings of Bounded LTL Model Checking
Logical Methods in Computer Science | 2007-10-11 | Paper |
Extended Resolution Proofs for Symbolic SAT Solving with Quantification
Lecture Notes in Computer Science | 2007-09-04 | Paper |
Extended Resolution Proofs for Conjoining BDDs
Computer Science – Theory and Applications | 2007-05-02 | Paper |
| Decomposing SAT problems into connected components | 2007-03-30 | Paper |
Automated Technology for Verification and Analysis
Lecture Notes in Computer Science | 2006-10-25 | Paper |
Formal Methods in Computer-Aided Design
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2005-12-16 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2005-12-15 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2005-12-06 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
| scientific article; zbMATH DE number 2102695 (Why is no real title available?) | 2004-09-24 | Paper |
A satisfiability procedure for quantified Boolean formulae
Discrete Applied Mathematics | 2003-09-15 | Paper |
Verifying the IEEE 1394 fireWire tree identify protocol with SMV
Formal Aspects of Computing | 2003-08-27 | Paper |
Verification of out-of-order processor designs using model Checking and a light-weight completion function
Formal Methods in System Design | 2002-07-08 | Paper |
Bounded model checking using satisfiability solving
Formal Methods in System Design | 2002-05-21 | Paper |
| scientific article; zbMATH DE number 1670773 (Why is no real title available?) | 2001-11-11 | Paper |
| scientific article; zbMATH DE number 1324663 (Why is no real title available?) | 1999-08-17 | Paper |
