Mathias Fleury

TACAS Conference 2026 Conference Paper

Real-time Proof Checking for Distributed Incremental SAT Solving

• Dominik Schreiber
• Mathias Fleury
• Katalin Fazekas
• Armin Biere

SAT Conference 2025 Conference Paper

Learn to Unlearn

• Bernhard Gstrein
• Florian Pollitt
• André Schidler
• Mathias Fleury
• Armin Biere

Clause learning is a significant milestone in the development of SAT solving. However, keeping all learned clauses without discrimination gradually slows down the solver. Thus, selectively removing some learned clauses during routine database reduction is essential. In this paper, we reexamine and test several long-standing ideas for clause removal in the modern solver Kissat. Our experiments show that retaining all clauses alters performance in all instances. For satisfiable instances, periodically removing all learned clauses surprisingly yields near state-of-the-art performance. For unsatisfiable instances, it is vital to always keep some learned clauses. Building on the influential Glucose paper, we find that it is crucial to always retain the clauses most likely to help, regardless of whether they are ranked by size or LBD in practice. Another key factor is whether a clause was used recently during conflict resolution steps. Eagerly keeping used clauses improves all unlearning strategies.

LPAR Conference 2024 Conference Paper

Certifying Incremental SAT Solving

• Katalin Fazekas
• Florian Pollitt
• Mathias Fleury
• Armin Biere

Certifying results by checking proofs and models is an essential feature of modern SAT solving. While incremental solving with assumptions and core extraction is crucial for many applications, support for incremental proof certificates remains lacking. We propose a proof format and corresponding checkers for incremental SAT solving. We further extend it to leverage resolution hints. Experiments on incremental SAT solving for Bounded Model Checking and Satisfiability Modulo Theories demonstrate the feasibility of our approach, further confirming that resolution hints substantially reduce checking time.

SAT Conference 2024 Conference Paper

Clausal Congruence Closure

• Armin Biere
• Katalin Fazekas
• Mathias Fleury
• Nils Christian Froleyks

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.

SAT Conference 2024 Conference Paper

Lazy Reimplication in Chronological Backtracking

• Robin Coutelier
• Mathias Fleury
• Laura Kovács

Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.

SAT Conference 2023 Conference Paper

Faster LRAT Checking Than Solving with CaDiCaL

• Florian Pollitt
• Mathias Fleury
• Armin Biere

DRAT is the standard proof format used in the SAT Competition. It is easy to generate but checking proofs often takes even more time than solving the problem. An alternative is to use the LRAT proof system. While LRAT is easier and way more efficient to check, it is more complex to generate directly. Due to this complexity LRAT is not supported natively by any state-of-the-art SAT solver. Therefore Carneiro and Heule proposed the mixed proof format FRAT which still suffers from costly intermediate translation. We present an extension to the state-of-the-art solver CaDiCaL which is able to generate LRAT natively for all procedures implemented in CaDiCaL. We further present Lrat-Trim, a tool which not only trims and checks LRAT proofs in both ASCII and binary format but also produces clausal cores and has been tested thoroughly. Our experiments on recent competition benchmarks show that our approach reduces time of proof generation and certification substantially compared to competing approaches using intermediate DRAT or FRAT proofs.

JAIR Journal 2022 Journal Article

Better Decision Heuristics in CDCL through Local Search and Target Phases

• Shaowei Cai
• Xindi Zhang
• Mathias Fleury
• Armin Biere

On practical applications, state-of-the-art SAT solvers dominantly use the conflict-driven clause learning (CDCL) paradigm. An alternative for satisfiable instances is local search solvers, which is more successful on random and hard combinatorial instances. Although there have been attempts to combine these methods in one framework, a tight integration which improves the state of the art on a broad set of application instances has been missing. We present a combination of techniques that achieves such an improvement. Our first contribution is to maximize in a local search fashion the assignment trail in CDCL, by sticking to and extending promising assignments via a technique called target phases. Second, we relax the CDCL framework by again extending promising branches to complete assignments while ignoring conflicts. These assignments are then used as starting point of local search which tries to find improved assignments with fewer unsatisfied clauses. Third, these improved assignments are imported back to the CDCL loop where they are used to determine the value assigned to decision variables. Finally, the conflict frequency of variables in local search can be exploited during variable selection in branching heuristics of CDCL. We implemented these techniques to improve three representative CDCL solvers (Glucose, MapleLcm DistChronoBT, and Kissat). Experiments on benchmarks from the main tracks of the last three SAT Competitions from 2019 to 2021 and an additional benchmark set from spectrum allocation show that the techniques bring significant improvements, particularly and not surprisingly, on satisfiable real-world application instances. We claim that these techniques were essential to the large increase in performance witnessed in the SAT Competition 2020 where Kissat and Relaxed LcmdCbDl NewTech were leading the field followed by CryptoMiniSAT-Ccnr, which also incorporated similar ideas.

SAT Conference 2021 Conference Paper

Efficient All-UIP Learned Clause Minimization

• Mathias Fleury
• Armin Biere

Abstract In 2020 Feng & Bacchus revisited variants of the all-UIP learning strategy, which considerably improved performance of their version of CaDiCaL submitted to the SAT Competition 2020, particularly on large planning instances. We improve on their algorithm by tightly integrating this idea with learned clause minimization. This yields a clean shrinking algorithm with complexity linear in the size of the implication graph. It is fast enough to unconditionally shrink learned clauses until completion. We further define trail redundancy and show that our version of shrinking removes all redundant literals. Independent experiments with the three SAT solvers CaDiCaL, Kissat, and Satch confirm the effectiveness of our approach.

LPAR Conference 2020 Conference Paper

A Verified SAT Solver Framework including Optimization and Partial Valuations

• Mathias Fleury
• Christoph Weidenbach

Based on our formal framework for CDCL (conflict-driven clause learning) using the proof assistant Isabelle/HOL, we verify an extension of CDCL computing cost-minimal models called OCDCL. It is based on branch and bound and computes models of minimal cost with respect to total valuations. The verification starts by developing a framework for CDCL with branch and bound, called CDCLBnB, which is then instantiated to get OCDCL. We then apply our formalization to three different applications. Firstly, through the dual rail encoding, we reduce the search for cost-optimal models with respect to partial valuations to searching for total cost-optimal models, as derived by OCDCL. Secondly, we instantiate OCDCL to solve MAX-SAT, and, thirdly, CDCLBnB to compute a set of covering models. A large part of the original CDCL verification framework was reused without changes to reduce the complexity of the new formalization. To the best of our knowledge, this is the first rigorous formalization of CDCL with branch and bound and its application to an optimizing CDCL calculus, and the first solution that computes cost-optimal models with respect to partial valuations.

SAT Conference 2020 Conference Paper

Distributed Cube and Conquer with Paracooba

• Maximilian Heisinger
• Mathias Fleury
• Armin Biere

Abstract Cube and conquer is currently the most effective approach to solve hard combinatorial problems in parallel. It organizes the search in two phases. First, a look-ahead solver splits the problem into many sub-problems, called cubes, which are then solved in parallel by incremental CDCL solvers. In this tool paper we present the first fully integrated and automatic distributed cube-and-conquer solver Paracooba targeting cluster and cloud computing. Previous work was limited to multi-core parallelism or relied on manual orchestration of the solving process. Our approach uses one master per problem to initialize the solving process and automatically discovers and releases compute nodes through elastic resource usage. Multiple problems can be solved in parallel on shared compute nodes, controlled by a custom peer-to-peer based load-balancing protocol. Experiments show the scalability of our approach.

IJCAI Conference 2017 Conference Paper

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

• Jasmin Christian Blanchette
• Mathias Fleury
• Christoph Weidenbach

We developed a formal framework for SAT solving using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL (conflict-driven clause learning) calculus is connected to a SAT solver that always terminates with correct answers. The framework offers a convenient way to prove theorems about the SAT solver and experiment with variants of the calculus. Compared with earlier verifications, the main novelties are the inclusion of the CDCL rules for forget, restart, and incremental solving and the use of refinement.