publications

2025

1. Introducing Certificates to the Hardware Model Checking Competition

   Nils Froleyks, Emily Yu, Mathias Preiner, and 2 more authors

   In Computer Aided Verification, 2025

   Abs DOI

   Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.

2. Clausal Equivalence Checking

   Armin Biere, Katalin Fazekas, Mathias Fleury, and 2 more authors

   2025

   Journal Submission
3. Certifying Constraints in Hardware Model Checking

   Nils Froleyks, Emily Yu, Armin Biere, and 1 more author

   2025

   Submitted

2024

1. CaDiCaL 2.0

   Armin Biere, Tobias Faller, Katalin Fazekas, and 3 more authors

   In CAV (1), 2024

   Abs DOI

   The SAT solver CaDiCaL provides a rich feature set with a clean library interface. It has been adopted by many users, is well documented and easy to extend due to its effective testing and debugging infrastructure. In this tool paper we give a high-level introduction into the solver architecture and then go briefly over implemented techniques. We describe basic features and novel advanced usage scenarios. Experiments confirm that CaDiCaL despite this flexibility has state-of-the-art performance both in a stand-alone as well as incremental setting.

2. Certifying Phase Abstraction

   Nils Froleyks, Emily Yu, Armin Biere, and 1 more author

   In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, 2024

   DOI
3. Clausal Congruence Closure

   Armin Biere, Katalin Fazekas, Mathias Fleury, and 1 more author

   In 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, 2024

   DOI
4. Clausal Equivalence Sweeping

   Armin Biere, Katalin Fazekas, Mathias Fleury, and 1 more author

   In Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, 2024

   DOI
5. Ternary Simulation as Abstract Interpretation (Work in Progress)

   Nils Froleyks, Emily Yu, and Armin Biere

   In MBMV 2024; 27. Workshop, 2024
6. Hardware Model Checking Competition 2024

   Armin Biere, Nils Froleyks, and Mathias Preiner

   In Proceedings 24th International Conference on Formal Methods in Computer-Aided Design (FMCAD’24), 2024

   DOI

2023

1. The SAT Museum

   Armin Biere, Mathias Fleury, Nils Froleyks, and 1 more author

   In Proceedings of the 14th International Workshop on Pragmatics of SAT co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Alghero, Italy, July 4, 2023, 2023
2. CadiBack: Extracting Backbones with CaDiCaL

   Armin Biere, Nils Froleyks, and Wenxi Wang

   In SAT, 2023
3. BIG Backbones

   Nils Froleyks, Emily Yu, and Armin Biere

   In FMCAD, 2023
4. Towards Compositional Hardware Model Checking Certification

   Emily Yu, Nils Froleyks, Armin Biere, and 1 more author

   In Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, 2023

   DOI

2022

1. Stratified Certification for K-Induction

   Emily Yu, Nils Froleyks, Armin Biere, and 1 more author

   In 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, 2022

   DOI

2021

1. SAT Competition 2020

   Nils Froleyks, Marijn Heule, Markus Iser, and 2 more authors

   Artif. Intell., 2021

   Abs DOI

   The SAT Competitions constitute a well-established series of yearly open international algorithm implementation competitions, focusing on the Boolean satisfiability (or propositional satisfiability, SAT) problem. In this article, we provide a detailed account on the 2020 instantiation of the SAT Competition, including the new competition tracks and benchmark selection procedures, overview of solving strategies implemented in top-performing solvers, and a detailed analysis of the empirical data obtained from running the competition.

2. Single Clause Assumption without Activation Literals to Speed-up IC3

   Nils Froleyks and Armin Biere

   In Formal Methods in Computer Aided Design, FMCAD 2021, 2021

   Abs DOI

   We extend the well-established assumption-based interface of incremental SAT solvers to clauses, allowing the addition of a temporary clause that has the same lifespan as literal assumptions. Our approach is efficient and easy to implement in modern CDCL-based solvers. Compared to previous approaches, it does not come with any memory overhead and does not slow down the solver due to disabled activation literals, thus eliminating the need for algorithms like IC3 to restart the SAT solver. All clauses learned under literal and clause assumptions are safe to keep and not implicitly invalidated for containing an activation literal. These changes increase the quality of learned clauses, resulting in better generalization for IC3. We implement the extension in the SAT solver CaDiCaL and evaluate it with the IC3 implementation in the model checker ABC. Our experiments on the benchmarks from a recent hardware model checking competition show a speedup for the average SAT call and a reduction in number of calls per verification instance, resulting in a substantial improvement in model checking time.

3. Ai assisted design of sokoban puzzles using automated planning

   Tomáš Balyo and Nils Froleyks

   In International Conference on ArtsIT, Interactivity and Game Creation, 2021
4. The results of SAT competition 2021

   Tomáš Balyo, Nils Froleyks, Markus Iser, and 2 more authors

   Sat, 2021

2020

1. Hardware Model Checking Competition (HWMCC’20)

   Armin Biere, Nils Froleyks, and Mathias Preiner

   2020
2. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions

   2020

2019

1. PASAR - Planning as Satisfiability with Abstraction Refinement

   Nils Froleyks, Tomáš Balyo, and Dominik Schreiber

   In Proceedings of the Twelfth International Symposium on Combinatorial Search, SOCS 2019, Napa, California, 16-17 July 2019, 2019

2017

1. Using an algorithm portfolio to solve sokoban

   Nils Froleyks and Tomáš Balyo

   In Proceedings of the International Symposium on Combinatorial Search, 2017