2021 | 2022 | 2023 | 2024 | 2025
Publications
[ Armin Biere | Tobias Faller | Mathias Fleury | Tobias Paxian | Peter Winterer ]
Publication lists of other team members are available from their team home-pages.
2025
On Enumerating Short Projected Models
Sibylle Möhle, Roberto Sebastiani, Armin Biere
Discrete Applied Mathematics (DAM)
vol. 361,
pages 412-439,
Elsevier 2025
[ paper
| bibtex
| doi
]
2024
SAT Solving for Variants of First‑Order Subsumption
Robin Coutelier,
Jakob Rath,
Michael Rawson,
Armin Biere,
Laura Kovács
Formal Methods in System Design
Springer 2024, published online
[ paper
| bibtex
| doi
]
Clausal Equivalence Sweeping
Armin Biere,
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks
Proc. 24th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'24)
page 236-241,
TU Wien Academic Press
2024
[ paper
| bibtex
| slides
| doi
| kissat
| hwmcc20miters
| hwmcc12miters
| experiments
]
Hardware Model Checking Competition 2024
Armin Biere,
Nils Froleyks,
Mathias Preiner
Proc. 24th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'24)
page 7,
TU Wien Academic Press
2024
[ paper
| bibtex
| competition
| slides
| doi
]
CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024
Armin Biere,
Tobias Faller,
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks
and
Florian Pollitt
Proc. SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions
Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2024-1,
pages 8-10,
University of Helsinki 2024
[ paper
| bibtex
| cadical
| isasat
| kissat
| gimsatul
| medals
]
Challenging Combinational Hardware Equivalence Checking Problems Submitted to the SAT Competition 2024
Armin Biere,
Tobias Faller,
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks
and
Florian Pollitt
Proc. SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions
Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2024-1,
page 33,
University of Helsinki 2024
[ paper
| bibtex
]
Dynamic Blocked Clause Elimination for Projected Model Counting
Jean-Marie Lagniez,
Pierre Marquis and
Armin Biere.
Proc. 27th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'24)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 305,
pages 21:1-21:17
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024
[ paper
| bibtex
| slides
| doi
]
Clausal Congruence Closure
Armin Biere, Katalin Fazekas,
Mathias Fleury and
Nils Frolekys
Proc. 27th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'24)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 305,
pages 6:1-6:25
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024
[ paper
| preprint
| bibtex
| slides
| doi
]
CaDiCaL 2.0
Armin Biere,
Tobias Faller
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks and
Florian Pollitt
Proc. Computer Aided Verification - 26th Intl. Conf. (CAV'24)
Lecture Notes in Computer Science (LNCS)
vol. 14681,
pages 133-152,
Springer 2024
[ paper
| bibtex
| official
| artifact
| cadical
| doi
]
Certifying Phase Abstraction
Nils Froleyks,
Emily Yu,
Armin Biere and
Keijo Heljanko
Proc. Automated Reasoning - 12th Intl. Joint Conf. (IJCAR'24)
Lecture Notes in Computer Science (LNCS)
vol. 14739,
pages 284-303,
Springer 2024
[
doi |
paper |
bibtex |
extended |
arxiv |
certifaiger
]
Certifying Incremental SAT Solving
Katalin Fazekas, Florian Pollitt,
Mathias Fleury and
Armin Biere
Proc. 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24)
EasyChair Proceedings and Collections (EPIC)
vol. 100,
pages 321-340,
Easychair 2024
[ paper
| bibtex
| lidrup-check
| idrup-check
| cvc5-branch
| cvc5-modifications
| cadical-version
]
Certified SAT solving with GPU accelerated Inprocessing
Muhammad Osama, Anton Wijs and Armin Biere
Formal Methods in System Design
vol. 62(1),
pages 79-118,
Springer 2024
[ paper
| bibtex
| parafrost
| doi
]
Incremental Proofs for Bounded Model Checking
Katalin Fazekas, Florian Pollitt,
Mathias Fleury and
Armin Biere
Proc. 27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'24)
ITG Fachberichte
vol. 314,
pages 133-143,
VDE Verlag 2024
[ preprint
| bibtex
]
Ternary Simulation as Abstract Interpretation (Work in Progress)
Nils Froleyks, Emily Yu and Armin Biere
Proc. 27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'24)
ITG Fachberichte
vol. 314,
pages 148-151,
VDE Verlag 2024
[ preprint
| bibtex
]
Disjoint Partial Enumeration without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
Proc. 38th AAAI Conference on Artificial Intelligence (AAAI'24)
pages 8126 - 8135, AAAI Press 2024
[ preprint
| doi
| zenodo
]
Lazy Reimplication in Chronological Backtracking
Robin Coutelier,
Mathias Fleury and
Laura Kovács
Proc. 27th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'24)
Leibniz International Proceedings in Informatics (LIPIcs)
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024
[ preprint
]
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, and Cesare Tinelli
TACAS 2024
Leibniz International Proceedings in Informatics (LIPIcs)
LNCS
[ springer
]
2023
A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper)
Mathias Fleury and
Peter Lammich
Proc. 29th Intl. Conf. on Automated Deduction (CADE'23)
Lecture Notes in Computer Science (LNCS)
vol. 14132,
pages 207-219,
Springer 2023
[ preprint
]
BIG Backbones
Nils Froleyks,
Emily Yu and
Armin Biere
Proc. 23rd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'23)
pages 162-167,
TU Wien Academic Press
2023
[
paper |
bibtex |
doi |
kb3 |
benchmarks
]
Towards Compositional Hardware Model Checking Certification
Emily Yu,
Nils Froleyks and
Armin Biere
Proc. 23rd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'23)
pages 44-54,
TU Wien Academic Press
2023
[
paper |
bibtex |
doi |
chmc |
certifaiger
]
The SAT Museum
Armin Biere,
Mathias Fleury,
Nils Froleyks and
Marijn Heule
Proc. 14th Intl. Workshop on Pragmatics of SAT (POS'23)
CEUR Workshop Proceedings
vol. 3545,
pages 72-87,
CEUR-WS.org 2023
[ paper
| bibtex
| data
| zenodo
| ceur
]
Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging
Tobias Paxian and
Armin Biere
Proc. 14th Intl. Workshop on Pragmatics of SAT (POS'23)
CEUR Workshop Proceedings
vol. 3545,
pages 59-71,
CEUR-WS.org 2023
[ paper
| bibtex
| data
| ceur
]
Armin Biere,
Mathias Fleury and
Florian Pollitt
CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT Entering
the SAT Competition 2023
Proc. SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2023-1,
pages 14-15,
University of Helsinki 2023
[ paper
| bibtex
]
Verifying Floating-Point Commutativity with GRS
Robin Trüby,
Mathias Fleury and
Armin Biere
Proc. SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2023-1,
page 53,
University of Helsinki, 2023
[ paper
| bibtex
]
Faster LRAT Checking Than Solving with CaDiCaL
Florian Pollitt,
Mathias Fleury and
Armin Biere
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 271,
pages 21:1-21:12,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2023
[ paper
| bibtex
]
Highlighted paper
IPASIR-Up: User Propagators for CDCL
Katalin Fazekas,
Aina Niemetz,
Mathias Preiner,
Markus Kirchweger,
Stefan Szeider and
Armin Biere
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 271,
pages 8:1-8:13,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2023
[ paper
| bibtex
| zenodo
| sms
| cvc5
| cadical
]
CadiBack: Extracting Backbones with CaDiCaL
Armin Biere,
Nils Froleyks
and Wenxi Wang
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 271,
pages 3:1-3:12,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2023
[ paper
| bibtex
| cadiback
| benchmarks
]
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
Maximilian Heisinger,
Martina Seidl
and
Armin Biere
Proc. 29th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)
Lecture Notes in Computer Science (LNCS)
vol. 13993,
pages 426-447,
Springer 2023
[ paper
| doi
| bibtex
| paracooba
]
Improving AMulet2 for Verifying Multiplier Circuits using SAT Solving and Computer Algebra
Daniela Kaufmann and
Armin Biere
International Journal on Software Tools for Technology Transfer (STTT)
vol. 25(2),
pages 133-144,
Springer 2023
[ paper
| doi
| bibtex ]
Efficient Proof Checking with LRAT in CaDiCaL (Work in Progress)
Florian Pollitt,
Mathias Fleury,
and Armin Biere
Proc. 26th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'23)
ITG Fachberichte
vol. 309,
pages 64-67,
VDE Verlag 2023
[
paper |
bibtex
]
Emily Yu,
Nils Froleyks,
Armin Biere and
Keijo Heljanko
Stratified Certification for k-Induction (Extended Abstract)
Proc. 26th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'23)
ITG Fachberichte
vol. 309,
pages 68-69,
VDE Verlag 2023
[
paper |
bibtex |
certifaiger
]
2022
First-Order Subsumption via SAT Solving
Jakob Rath,
Armin Biere,
Laura Kovács
Proc. 22nd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'22)
pages 160-169,
TU Wien Academic Press
2023
[ paper
| bibtex
| doi
]
Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss-Check
Daniela Kaufmann,
Mathias Fleury,
Armin Biere and
Manuel Kauers
Formal Methods in System Design
Springer 2022
[ preprint
| bibtex
| doi
]
Mining Definitions in Kissat with Kittens
Mathias Fleury and
Armin Biere
Formal Methods in System Design
vol. 60(3),
pages 381-404,
Springer 2022
[ preprint
| bibtex
| paper
| data
| doi
]
Emily Yu,
Nils Froleyks,
Armin Biere and
Keijo Heljanko
Stratified Certification for k-Induction
Proc. 22nd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'22)
pages 59-64,
TU Wien Academic Press
2022
[
paper |
bibtex |
certifaiger
]
Better Decision Heuristics in CDCL through Local Search and Target Phases
Shaowei Cai,
Xindi Zhang,
Mathias Fleury and
Armin Biere
Journal of Artificial Intelligence Research (JAIR)
vol. 74,
pages 1515-1563,
2022
[ paper
| doi
| bibtex
| code
| data
]
QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Maximilian Heisinger,
Martina Seidl and
Armin Biere
Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR'22)
CEUR Workshop Proceedings
vol. 3201,
CEUR-WS.org 2022
[ paper
| bibtex
| quapi
| ceur
]
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
Mathias Fleury
and
Armin Biere
CoRR abs/2207.13577 (2022)
presented at
POS'22
[ paper
| arxiv
| bibtex
| gimsatul
| slides
]
Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022
Armin Biere and
Mathias Fleury
Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2022-1,
pages 10-11,
University of Helsinki 2022
[ paper
| bibtex
]
Hardware Model Checking Certificates
Emily Yu,
Nils Froleyks,
Armin Biere and
Mathias Fleury
In Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B</b>
vol. B-2022-1,
page 46,
University of Helsinki 2022
[ paper
| bibtex
]
Migrating Solver State
Armin Biere,
Md Solimul Chowdhury,
Marijn J. H. Heule,
Benjamin Kiesl
and Michael W. Whalen
Proc. 25th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'22)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 236,
pages 21:1-21:24,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2022
[ preprint
| doi
| bibtex
| migrating CaDiCaL source code
]
Fuzzing and Delta Debugging And-Inverter Graph Verification Tools
Daniela Kaufmann and Armin Biere
Proc. 16th Intl. Conf. on Tests and Proofs (TAP'22)
Lecture Notes in Computer Science (LNCS)
vol. 13361,
pages 69-88,
Springer 2022
[ preprint
| bibtex
| artifact
| amulet
]
Clausal Proofs for Pseudo-Boolean Reasoning
Randal E. Bryant,
Armin Biere and
Marijn J. H. Heule
Proc. 28th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Lecture Notes in Computer Science (LNCS)
vol. 13243,
pages 443-461,
Springer 2022
[ paper
| bibtex
| github
| zenodo
]
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
Daniela Kaufmann,
Paul Beame, Armin Biere,
and Jakob Nordström
Proc. Design, Automation and Test in Europe (DATE'22)
IEEE 2022
[ paper
| bibtex
| experiments
]
2021
Single Clause Assumption without Activation Literals to Speed-up IC3
Nils Froleyks and Armin Biere
Proc. 21st Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'21)
pages 72-76,
TU Wien Academic Press
2021
[
paper |
bibtex |
experiments |
cadical
]
Publications before 2022 are listed on the IRA Publication web-page.