| Publication | Date of Publication | Type |
|---|
| QMusExt: A minimal (un)satisfiable core extractor for quantified Boolean formulas | 2024-11-26 | Paper |
| Validation of QBF encodings with winning strategies | 2024-11-26 | Paper |
Never trust your solver: certification for SAT and QBF
Lecture Notes in Computer Science | 2024-02-28 | Paper |
True crafted formula families for benchmarking quantified satisfiability solvers
Lecture Notes in Computer Science | 2024-02-28 | Paper |
OuterCount: a first-level solution-counter for quantified Boolean formulas
Lecture Notes in Computer Science | 2023-06-02 | Paper |
A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications
ACM Communications in Computer Algebra | 2023-01-11 | Paper |
Skolem function continuation for quantified Boolean formulas
Tests and Proofs | 2022-07-01 | Paper |
| QBFFam: a tool for generating QBF families from proof complexity | 2022-03-22 | Paper |
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
Formal Methods in System Design | 2021-12-08 | Paper |
New ways to multiply \(3 \times 3\)-matrices
Journal of Symbolic Computation | 2021-02-18 | Paper |
| QRAT polynomially simulates \(\forall\)-Exp+Res | 2020-05-20 | Paper |
Local search for fast matrix multiplication
(available as arXiv preprint) | 2020-05-20 | Paper |
| On the maximal minimal cube lengths in distinct DNF tautologies | 2020-01-21 | Paper |
On the maximal minimal cube lengths in distinct DNF tautologies
(available as arXiv preprint) | 2020-01-21 | Paper |
The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
Artificial Intelligence | 2019-08-28 | 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 |
Short proofs for some symmetric quantified Boolean formulas
Information Processing Letters | 2018-10-19 | Paper |
Symmetries of quantified Boolean formulas
(available as arXiv preprint) | 2018-08-10 | Paper |
Intra- and interdiagram consistency checking of behavioral multiview models
Computer Languages, Systems & Structures | 2018-05-15 | Paper |
| A little blocked literal goes a long way | 2017-11-15 | Paper |
Solution validation and extraction for QBF preprocessing
Journal of Automated Reasoning | 2017-07-10 | Paper |
Q-resolution with generalized axioms
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Super-blocked clauses
Automated Reasoning | 2016-09-05 | Paper |
The QBF Gallery: behind the scenes
Artificial Intelligence | 2016-05-20 | Paper |
Enhancing search-based QBF solving by dynamic blocked clause elimination
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Clause elimination for SAT and QSAT
Journal of Artificial Intelligence Research | 2015-08-25 | Paper |
SAT-Based Synthesis Methods for Safety Specs
Lecture Notes in Computer Science | 2015-01-13 | Paper |
\(\mathsf{MPIDepQBF}\): towards parallel QBF solving without knowledge sharing
Lecture Notes in Computer Science | 2014-09-26 | Paper |
A unified proof system for QBF preprocessing
Automated Reasoning | 2014-09-26 | Paper |
Blocked clause elimination for QBF
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2009-07-24 | Paper |
A solver for QBFs in negation normal form
Constraints | 2009-05-29 | Paper |
