publications | Nils Froleyks

2025

Deep Integration of SAT Solving and Model Checking

Nils Froleyks

PhD Thesis

Johannes Kepler Universität Linz, 2025

Abs PDF

Once just considered the archetypal intractable problem, Boolean satisfiability (SAT) has flourished into one of the most effective tools for automated reasoning. One of its most successful applications is model checking, where SAT solvers are used to verify the correctness of systems by checking whether certain properties hold. This thesis investigates how to deepen the integration between SAT solving and model checking to improve performance and increase trust in the results. We begin by presenting the state-of-the-art incremental SAT solver CaDiCaL 2.0. We extend its assumption-based interface with clause assumptions, and demonstrate how this enhancement accelerates IC3-based model checking. Building on CaDiCaL, we introduce a new backbone extraction tool, CadiBack. A formula’s backbone—the set of literals true in every satisfying assignment—can benefit various SAT-based applications, including verification, state space approximation, and fault localization. As part of this work, we present a polynomial-time backbone extraction algorithm and evaluate it as a preprocessor for CadiBack. Additionally, we formalize ternary simulation through the lens of abstract interpretation and propose a technique to improve accuracy using backbone extraction. We then address how to achieve a similar level of trust in model checking as is commonly vested in SAT solvers. To this end, we develop a certification approach for hardware model checking. Specifically, we present certificate constructions for the preprocessing techniques of phase abstraction and constraint extraction. Our efforts culminate in the Hardware Model Checking Competition 2024, which marks the introduction of mandatory certificates for all participating tools. The results convincingly show the practical efficiency and effectiveness of our approach. Finally, this thesis further explores competitions as a scientific method for advancing solver technology. Drawing on the author’s experience co-organizing several SAT and hardware model checking competitions, we examine what insights into solver innovation can be gained from these events.
Introducing Certificates to the Hardware Model Checking Competition

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

In Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, 2025

Abs DOI PDF

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.
Challenging Certificates from Model Checking

Nils Froleyks, Emily Yu, and Armin Biere

SAT Competition Benchmark Description

2025

2024

CaDiCaL 2.0

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

In CAV, 2024

Abs PDF

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.
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

Abs DOI PDF

Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.
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

Abs DOI PDF

The state-of-the-art to combinational equivalence checking is based on SAT sweeping. It recursively establishes equivalence of internal nodes of two circuits to prove equivalence of their outputs. The approach follows the topological order from inputs to outputs and makes use of simulation to refine the set of potentially equivalent nodes to reduce the number of SAT solver queries. This non-uniform hybrid reasoning, using both the circuit structure and a clausal encoding, is complex to orchestrate. In earlier work, clausal encoding was avoided using a dedicated circuit-aware SAT solver. Instead, we propose to perform SAT sweeping directly on the clausal encoding of the complete equivalence checking problem within the SAT solver, but again relying on a second, dedicated, internal SAT solver. Both SAT solvers work on a clausal representation. This allows to transparently make use of all the advanced reasoning capabilities of the SAT solver, particularly pre- and inprocessing techniques.
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, Pune, India, 2024

Abs DOI PDF

Many practical applications of satisfiability solving employ multiple steps to encode an original problem formulation into conjunctive normal form. Often circuits are used as intermediate representation before encoding those circuits into clausal form. These circuits however might contain redundant isomorphic sub-circuits. If blindly translated into clausal form, this redundancy is retained and increases solving time unless specific preprocessing algorithms are used. Furthermore, such redundant sub-formula structure might only emerge during solving and needs to be addressed by inprocessing. This paper presents a new approach which extracts gate information from the formula and applies congruence closure to match and eliminate redundant gates. Besides new algorithms for gate extraction, we also describe previous unpublished attempts to tackle this problem. Experiments focus on the important problem of combinational equivalence checking for hardware designs and show that our new approach yields a substantial gain in CNF solver performance.
Ternary Simulation as Abstract Interpretation

Nils Froleyks, Emily Yu, and Armin Biere

In MBMV 2024; 27. Workshop, 2024

Abs PDF

We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking.
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
Hardware Equivalence Checking Problems

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

SAT Competition Benchmark Description

2024
CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024

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

In Proc. of SAT Competition 2024 – Solver, Benchmark and Proof Checker Descriptions, 2024

Abs

In this short system description we describe our three sequential SAT solvers CaDiCaL, IsaSAT and Kissat submitted to the main track of the SAT competition 2024 as well as an update to Gimsatul submitted to the parallel track.

2023

BIG Backbones

Nils Froleyks, Emily Yu, and Armin Biere

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

DOI
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

Abs DOI PDF

In this paper, we revisit and formalize temporal decomposition, as one of the most basic, widely-used and effective preprocessing techniques in hardware model checking. The main contribution is a certification framework for hardware model checking using temporal decomposition. Our approach enables generation of a single inductive invariant in a compositional way using inductive invariant certificates provided by existing certifying model checkers on the result of preprocessing a model through temporal decomposition. We implement and evaluate the method on hardware model checking competition benchmarks. The experiments confirm the effectiveness of temporal decomposition. The proposed certification approach makes it feasible to generate a generic proof for model checking and preprocessing.
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

Abs PDF

The virtual SAT Solver Museum is an effort towards preserving historical SAT solvers, by collecting and porting their source code to modern compilers and evaluating them on representative benchmark sets on the same hardware. This allows us to compare historic and modern solvers in the same environment. Our results clearly show a remarkable improvement of SAT solver performance in the last 30 years.
CadiBack: Extracting Backbones with CaDiCaL

Armin Biere, Nils Froleyks, and Wenxi Wang

In SAT, 2023

Abs PDF

The backbone of a satisfiable formula is the set of literals that are true in all its satisfying assignments. Backbone computation can improve a wide range of SAT-based applications, such as verification, fault localization and product configuration. In this tool paper, we introduce a new backbone extraction tool called CadiBack. It takes advantage of unique features available in our state-of-the-art SAT solver CaDiCaL including transparent inprocessing and single clause assumptions, which have not been evaluated in this context before. In addition, CaDiCaL is enhanced with an improved algorithm to support model rotation by utilizing watched literal data structures. In our comprehensive experiments with a large number of benchmarks, CadiBack solves 60% more instances than the state-of-the-art backbone extraction tool MiniBones. Our tool is thoroughly tested with fuzzing, internal correctness checking and cross-checking on a large benchmark set. It is publicly available as open source, well documented and easy to extend.

2022

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

Abs DOI PDF

Our recently proposed certification framework for bit-level k-induction-based model checking has been shown to be quite effective in increasing the trust of verification results even though it partially involved quantifier reasoning. In this paper we show how to simplify the approach by assuming reset functions to be stratified. This way it can be lifted to word-level and in principle to other theories where quantifier reasoning is difficult. Our new method requires six simple SAT checks and one polynomial-time check, allowing certification to remain in co-NP while the previous approach required five SAT checks and one QBF check. Experimental results show a substantial performance gain for our new approach. Finally, we present and evaluate our new tool Certifaiger-wl which is able to certify k-induction-based word-level model checking.
Unique Reconfiguration Sequence

Nils Froleyks, Emily Yu, and Armin Biere

SAT Competition Benchmark Description

2022
Hardware Model Checking Certificates

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

SAT Competition Benchmark Description

2022
ReconfAIGERation entering Core Challenge 2022

Nils Froleyks, Emily Yu, and Armin Biere

2022

2021

Single Clause Assumption without Activation Literals to Speed-up IC3

Nils Froleyks and Armin Biere

In Formal Methods in Computer Aided Design, FMCAD, 2021

Abs DOI PDF

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 im- plement 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.
SAT Competition 2020

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

Artificial Intelligence, 2021

Abs DOI PDF

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.
AI Assisted Design of Sokoban Puzzles Using Automated Planning

Tomás Balyo and Nils Froleyks

In ArtsIT, Interactivity and Game Creation - Creative Heritage. New Perspectives from Media Arts and Artificial Intelligence. 10th EAI International Conference, ArtsIT 2021, Virtual Event, December 2-3, 2021, Proceedings, 2021

Abs DOI PDF

Designing interesting and challenging levels for a puzzle game is a very difficult and time consuming task. It is often possible to develop random puzzle generators that can produce solvable levels. However, in order to obtain appealing levels, usually a human designer needs to be involved. In this paper we propose a new generic method for assisting human designers to create solvable levels for a puzzle game by using Automated Planning. We will demonstrate our method on the well-known Japanese puzzle game Sokoban.

2020

Hardware Model Checking Competition 2020

Armin Biere, Nils Froleyks, and Mathias Preiner

In Formal Methods in Computer-Aided Design, FMCAD, 2020
Proceedings of SAT Competition 2020: Solver and benchmark descriptions

Tomáš Balyo, Nils Froleyks, Marijn JH Heule, and 3 more authors

2020

2019

PASAR - Planning as Satisfiability with Abstraction Refinement

Nils Christian Froleyks, Tomás Balyo, and Dominik Schreiber

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

Abs DOI PDF

One of the classical approaches to automated planning is the reduction to propositional satisfiability (SAT). Recently, it has been shown that incremental SAT solving can increase the capabilities of several modern encodings for SAT-based planning. In this paper, we present a further improvement to SAT-based planning by introducing a new algorithm named PASAR based on the principles of counterexample guided abstraction refinement (CEGAR). As an abstraction of the original problem, we use a simplified encoding where interference between actions is generally allowed. Abstract plans are converted into actual plans where possible or otherwise used as a counterexample to refine the abstraction. Using benchmark domains from recent International Planning Competitions, we compare our approach to different state-of-the-art planners and find that, in particular, combining PASAR with forward state-space search techniques leads to promising results.
PASAR Entering the Sparkle Planning Challenge 2019

Nils Froleyks, Tomáš Balyo, and Dominik Schreiber

2019
PASAR – Planning as Satisfiability with Abstraction Refinement

Nils Froleyks

Master’s Thesis

Sep 2019

Abs

We present a new algorithm for the satisficing (non-optimal) classical planning prob- lem. The presented planner participated in the Sparkle Planning Challenge 2019 and won a considerable share (22.13%) of the first prize. We combine SAT-based planning with forward state space search using the principles of counterexample-guided abstraction refinement (CEGAR). A state-of-the-art SAT solver is used to solve an abstraction of the planning task at hand. As an abstraction, we use an incomplete encoding where interference between actions is ignored. With a graph-theoretic test we determine whether the solution found by the SAT solver can be directly transformed into a plan. If it can be transformed, we realize an encoding allowing the application of many actions in parallel (exist-step semantics) in a very compact manner, without imposing a fixed order on the actions. If the transformation is not possible, we use the solution to define a heuristic function that is used during a state space search. If the search fails to find a plan within a very short timeout, the abstraction is refined. To increase the synergy between SAT solving and forward search, both can learn new actions and add them to the problem. This allows the SAT solver to make big jumps in the search space, while the forward search benefits from the SAT solver’s ability to solve combinatorially hard problems. Using benchmark domains from recent international planning competitions, we com- pare our approach with various state-of-the-art planners from the fields of SAT-based planning and heuristic search. On almost all tested domains we can match the per- formance of the best tested solvers and on some domains we outperform the entire competition.

2017

Using an Algorithm Portfolio to Solve Sokoban

Nils Christian Froleyks and Tomás Balyo

In Proceedings of the Tenth International Symposium on Combinatorial Search, SOCS 2017, 16-17 June 2017, Pittsburgh, Pennsylvania, USA, 2017

Abs DOI PDF

The game of Sokoban is an interesting platform for algorithm research. It is hard for humans and computers alike. Even small levels can take a lot of computation for all known algorithms. In this paper we will describe how a search based Sokoban solver can be structured and which algorithms can be used to realize each critical part. We implement a variety of those, construct a number of different solvers and combine them into an algorithm portfolio. The solver we construct this way can outperform existing solvers when run in parallel, that is, our solver with 16 processors outperforms the previous sequential solvers.
Using an Algorithm Portfolio to Solve Sokoban

Nils Froleyks

Bachelor’s Thesis

Feb 2017

Abs

The game of Sokoban is an interesting platform for algorithm research. It is hard for humans and computers alike. Even with its simple rules and small average level sizes there are levels that take a lot of computation for all known algorithms. In this thesis we will combine different Sokoban solvers with different domain specific enhancements into one portfolio. This portfolio can then be run in parallel on one problem until one solver finds a solution. Additionally the solvers in the portfolio can exchange data to speed up computation. We will validate the approach of algorithm portfolios for designing a parallel Sokoban solver.