Armin Biere

FM Conference 2026 Conference Paper

Certifying Constraints in Hardware Model Checking

• Nils Froleyks
• Emily Yu
• Armin Biere
• Keijo Heljanko

Abstract Model checking is a powerful automated reasoning technique for verifying hardware designs, ensuring that they function correctly before deployment. However, modern model checkers are complex software systems with hundreds of thousands of lines of code, making them prone to errors. To increase confidence in verification results, recent efforts in hardware verification focus on requiring model checkers to produce machine-checkable proofs according to a standardized format that can be independently validated. Yet, implementing proof generation across different verification algorithms presents a unique challenge. In hardware model checking, constraints play an essential role, as they encode assumptions about the environment and help simplify analysis. This paper addresses the challenge by developing a certification approach that ensures verification results remain trustworthy when constraints are present. We introduce certificate generation methods for three classes of constraints that can be extracted from the models. Furthermore, to support a broader range of constraints and more complex reset logic for industrial use, we also provide alternative Quantified Boolean Formula checks in the proof format with a single quantifier alternation. Lastly, we present a certificate generation method for k -induction with uniqueness constraints, an important model checking technique. We implement these in a certification toolkit, and provide empirical evaluation on competition benchmarks, demonstrating their effectiveness.

JAIR Journal 2026 Journal Article

MaxSAT Fuzzing and Delta Debugging

• Tobias Paxian
• Armin Biere

This article presents the first systematic study to evaluate a suite of automated fuzzing techniques for Maximum Satisfiability (MaxSAT) solvers. It combines large-scale stress testing with a novel MaxSAT-specific delta debugging method to assess and improve solver robustness. A parallel framework orchestrates the generation of millions of structured MaxSAT instances. It efficiently isolates failure-inducing input and distills failing cases into minimal counterexamples for precise failure localization. Over a 100-hour fuzzing effort, this approach revealed previously unknown failures in almost all 43 solvers from recent MaxSAT competitions and in three certificate-producing solvers. Failures ranged from crashes and incorrect optimality bounds to severe performance slowdowns. Notably, a critical soundness error was identified in one certified solver. The resulting corpus of minimal counterexamples was published as a public regression suite. This suite was adopted as a mandatory check in the 2024 MaxSAT Evaluation, helping cut average solver failure rates by more than half. The MaxSAT community quickly embraced these resources: some solver development teams have already integrated our fuzzer into their workflows. The complete tool chain and benchmark corpus are available at Zenodo (Paxian 2025a). Our study demonstrates that systematic fuzz testing coupled with targeted debugging can significantly raise the reliability standards of MaxSAT solvers and provide valuable resources for future solver development.

TACAS Conference 2026 Conference Paper

Real-time Proof Checking for Distributed Incremental SAT Solving

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

AIJ Journal 2025 Journal Article

Disjoint projected enumeration for SAT and SMT without blocking clauses

• Giuseppe Spallitta
• Roberto Sebastiani
• Armin Biere

All-Solution Satisfiability (AllSAT) and its extension, All-Solution Satisfiability Modulo Theories (AllSMT), have become more relevant in recent years, mainly in formal verification and artificial intelligence applications. The goal of these problems is the enumeration of all satisfying assignments of a formula (for SAT and SMT problems, respectively), making them useful for test generation, model checking, and probabilistic inference. Nevertheless, traditional AllSAT algorithms face significant computational challenges due to the exponential growth of the search space and inefficiencies caused by blocking clauses, which cause memory blowups and degrade unit propagation performance in the long term. This paper presents two novel solvers: TABULARALLSAT, a projected AllSAT solver, and TABULARALLSMT, a projected AllSMT solver. Both solvers combine Conflict-Driven Clause Learning (CDCL) with chronological backtracking to improve efficiency while ensuring disjoint enumeration. To retrieve compact partial assignments we propose a novel aggressive implicant shrinking algorithm, compatible with chronological backtracking, to minimize the number of partial assignments, reducing overall search complexity. Furthermore, we extend the solver framework to handle projected enumeration and SMT formulas effectively and efficiently, adapting the baseline framework to integrate theory reasoning and the distinction between important and non-important variables. An extensive experimental evaluation demonstrates the superiority of our approach compared to state-of-the-art solvers, particularly in scenarios requiring projection and SMT-based reasoning.

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.

SAT Conference 2025 Conference Paper

Streamlining Distributed SAT Solver Design

• Dominik Schreiber 0001
• Niccolò Rigi-Luperti
• Armin Biere

Distributed clause-sharing SAT solvers have recently been established as powerful automated reasoning tools that can conquer previously infeasible instances. A common design of distributed SAT solvers is to run many off-the-shelf sequential solvers in parallel, employ some diversification (e. g. , restart intervals or decision orders), and share conflict clauses among the solver threads. This approach, naïvely, adopts all best practices of sequential solver design for distributed solving, where these practices may be less useful or even actively detrimental. In this work we diagnose such shortcomings in the state-of-the-art system MallobSat and propose first effective mitigations. In particular, we replace the redundant pre- and inprocessing at all threads with single-core preprocessing that runs next to the parallel search, remove LBD values from the clause-sharing operation, and slim down solver diversification to very few lightweight and uniform methods. Experimental evaluations on up to 3072 cores (64 nodes) confirm that our measures improve performance while also drastically simplifying the SAT solving program that is run in parallel.

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.

AAAI Conference 2024 Conference Paper

Disjoint Partial Enumeration without Blocking Clauses

• Giuseppe Spallitta
• Roberto Sebastiani
• Armin Biere

A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is based on adding blocking clauses incrementally, ruling out previously found models. On the one hand, blocking clauses have the potential to reduce the number of generated models exponentially, as they can handle partial models. On the other hand, the introduction of a large number of blocking clauses affects memory consumption and drastically slows down unit propagation. We propose a new approach that allows for enumerating disjoint partial models with no need for blocking clauses by integrating: Conflict-Driven Clause-Learning (CDCL), Chronological Backtracking (CB), and methods for shrinking models (Implicant Shrinking). Experiments clearly show the benefits of our novel approach.

SAT Conference 2024 Conference Paper

Dynamic Blocked Clause Elimination for Projected Model Counting

• Jean-Marie Lagniez
• Pierre Marquis
• Armin Biere

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X. Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.

JAIR Journal 2024 Journal Article

Satisfiability Modulo User Propagators

• Katalin Fazekas
• Aina Niemetz
• Mathias Preiner
• Markus Kirchweger
• Stefan Szeider
• Armin Biere

Modern SAT solvers are often integrated as sub-reasoning engines into more complex tools to address problems beyond the Boolean satisfiability problem. Consider, for example, solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration, and model counting. There, the SAT solver can often provide relevant information beyond the satisfiability answer and the domain knowledge of the embedding system, such as symmetry properties or theory axioms, may benefit the CDCL search. However, this knowledge can often not be efficiently represented in clausal form. This paper proposes a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. The aim is to capture the essential functionalities that simplify and improve use cases requiring a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, the state-of-the-art SAT solver CaDiCaL is extended with the proposed interface and evaluated on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL( T ) SAT engine of the SMT solver cvc5.

SAT Conference 2023 Conference Paper

CadiBack: Extracting Backbones with CaDiCaL

• Armin Biere
• Nils Christian Froleyks
• Wenxi Wang

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.

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.

SAT Conference 2023 Conference Paper

IPASIR-UP: User Propagators for CDCL

• Katalin Fazekas
• Aina Niemetz
• Mathias Preiner
• Markus Kirchweger
• Stefan Szeider
• Armin Biere

Modern SAT solvers are frequently embedded as sub-reasoning engines into more complex tools for addressing problems beyond the Boolean satisfiability problem. Examples include solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration and counting. In such use cases, the SAT solver is often able to provide relevant information beyond the satisfiability answer. Further, domain knowledge of the embedding system (e. g. , symmetry properties or theory axioms) can be beneficial for the CDCL search, but cannot be efficiently represented in clausal form. In this paper, we propose a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. Our goal is to capture the most essential functionalities that are sufficient to simplify and improve use cases that require a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, we extend CaDiCaL with our interface and evaluate it on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.

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 2022 Conference Paper

Migrating Solver State

• Armin Biere
• Md. Solimul Chowdhury
• Marijn J. H. Heule
• Benjamin Kiesl
• Michael W. Whalen

We present approaches to store and restore the state of a SAT solver, allowing us to migrate the state between different compute resources, or even between different solvers. This can be used in many ways, e. g. , to improve the fault tolerance of solvers, to schedule SAT problems on a restricted number of cores, or to use dedicated preprocessing tools for inprocessing. We identify a minimum viable subset of the solver state to migrate such that the loss of performance is small. We then present and implement two different approaches to state migration: one approach stores the state at the end of a solver run whereas the other approach stores the state continuously as part of the proof trace. We show that our approaches enable the generation of correct models and valid unsatisfiability proofs. Experimental results confirm that the overhead is reasonable and that in several cases solver performance actually improves.

IJCAI Conference 2021 Conference Paper

Decomposition Strategies to Count Integer Solutions over Linear Constraints

• Cunjing Ge
• Armin Biere

Counting integer solutions of linear constraints has found interesting applications in various fields. It is equivalent to the problem of counting integer points inside a polytope. However, state-of-the-art algorithms for this problem become too slow for even a modest number of variables. In this paper, we propose new decomposition techniques which target both the elimination of variables as well as inequalities using structural properties of counting problems. Experiments on extensive benchmarks show that our algorithm improves the performance of state-of-the-art counting algorithms, while the overhead is usually negligible compared to the running time of integer counting.

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.

SAT Conference 2021 Conference Paper

XOR Local Search for Boolean Brent Equations

• Wojciech Nawrocki
• Zhenjun Liu
• Andreas Fröhlich
• Marijn J. H. Heule
• Armin Biere

Abstract Combining clausal and XOR reasoning has been studied for almost two decades, in particular in the context of CDCL and look-ahead, but not in classical local search. To stimulate research in this direction, we propose to standardize a hybrid format, called XNF, which allows both clauses and XORs. We implemented a tool to extract XOR constraints from a CNF, simplify them, and produce an XNF formula. The usefulness of XNF formulas is demonstrated by focusing on the impact of combined clausal and XOR reasoning on local search. Native support for XOR facilitates satisfying any falsified long XOR using a single flip, similarly to satisfying a falsified clause. When combined with XOR-based heuristics, local search performance is significantly improved on matrix multiplication challenges which are hard for CDCL.

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.

SAT Conference 2020 Conference Paper

Four Flavors of Entailment

• Sibylle Möhle
• Roberto Sebastiani
• Armin Biere

Abstract We present a novel approach for enumerating partial models of a propositional formula, inspired by how theory solvers and the SAT solver interact in lazy SMT. Using various forms of dual reasoning allows our CDCL-based algorithm to enumerate partial models with no need for exploring and shrinking full models. Our focus is on model enumeration without repetition, with potential applications in weighted model counting and weighted model integration for probabilistic inference over Boolean and hybrid domains. Chronological backtracking renders the use of blocking clauses obsolete. We provide a formalization and examples. We further discuss important design choices for a future implementation related to the strength of dual reasoning, including unit propagation, using SAT or QBF oracles.

SAT Conference 2019 Conference Paper

Backing Backtracking

• Sibylle Möhle
• Armin Biere

Abstract Non-chronological backtracking was considered an important and necessary feature of conflict-driven clause learning (CDCL). However, a SAT solver combining CDCL with chronological backtracking succeeded in the main track of the SAT Competition 2018. In that solver, multiple invariants considered crucial for CDCL were violated. In particular, decision levels of literals on the trail were not necessarily increasing anymore. The corresponding paper presented at SAT 2018 described the algorithm and provided empirical evidence of its correctness, but a formalization and proofs were missing. Our contribution is to fill this gap. We further generalize the approach, discuss implementation details, and empirically confirm its effectiveness in an independent implementation.

SAT Conference 2019 Conference Paper

Incremental Inprocessing in SAT Solving

• Katalin Fazekas
• Armin Biere
• Christoph Scholl 0001

Abstract Incremental SAT is about solving a sequence of related SAT problems efficiently. It makes use of already learned information to avoid repeating redundant work. Also preprocessing and inprocessing are considered to be crucial. Our calculus uses the most general redundancy property and extends existing inprocessing rules to incremental SAT solving. It allows to automatically reverse earlier simplification steps, which are inconsistent with literals in new incrementally added clauses. Our approach to incremental SAT solving not only simplifies the use of inprocessing but also substantially improves solving time.

LPAR Conference 2017 Conference Paper

Blocked Clauses in First-Order Logic

• Benjamin Kiesl
• Martin Suda 0001
• Martina Seidl
• Hans Tompits
• Armin Biere

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses whose elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.

IJCAI Conference 2017 Conference Paper

Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?

• Benjamin Kiesl
• Martina Seidl
• Hans Tompits
• Armin Biere

Clause-elimination techniques that simplify formulas by removing redundant clauses play an important role in modern SAT solving. Among the types of redundant clauses, blocked clauses are particularly popular. For checking whether a clause C is blocked in a formula F, one only needs to consider the so-called resolution neighborhood of C, i. e. , the set of clauses that can be resolved with C. Because of this, blocked clauses are referred to as being locally redundant. In this paper, we discuss powerful generalizations of blocked clauses that are still locally redundant, viz. set-blocked clauses and super-blocked clauses. We furthermore present complexity results for deciding whether a clause is set-blocked or super-blocked.

AIJ Journal 2016 Journal Article

SAT Race 2015

• Tomáš Balyo
• Armin Biere
• Ashlin Iser
• Carsten Sinz

Boolean satisfiability (SAT) solving is one of the most competitive research areas of theoretical computer science. The performance of state-of-the-art SAT solvers has been continuously improving in the last decades and has reached a level where SAT solvers can be employed to solve real world problems in fields such as hardware and software verification, automated planning and many others. One of the important driving forces of this progress are the yearly organized (since 2002) SAT competitions. In this paper we describe the 2015 SAT Race that featured the traditional sequential and parallel tracks (with 64 core computers) and introduced the Incremental Library Track, which is particularly interesting for developers of SAT based applications. We describe the 2015 SAT Race and provide a detailed analysis of its results.

JAIR Journal 2015 Journal Article

Clause Elimination for SAT and QSAT

• Marijn Heule
• Matti Järvisalo
• Florian Lonsing
• Martina Seidl
• Armin Biere

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT---the standard input formats of SAT and QSAT solvers---have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.

LPAR Conference 2015 Conference Paper

Compositional Propositional Proofs

• Marijn J. H. Heule
• Armin Biere

Abstract Many hard-combinatorial problems have only be solved by SAT solvers in a massively parallel setting. This reduces the trust one has in the final result as errors might occur during parallel SAT solving or during partitioning of the original problem. We present a new framework to produce clausal proofs for cube-and-conquer, arguably the most effective parallel SAT solving paradigm for hard-combinatorial problems. The framework also provides an elegant approach to parallelize the validation of clausal proofs efficiently, both in terms of run time and memory usage. We evaluate the presented approach on some hard-combinatorial problems and validate constructed clausal proofs in parallel.

LPAR Conference 2015 Conference Paper

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination

• Florian Lonsing
• Fahiem Bacchus
• Armin Biere
• Uwe Egly
• Martina Seidl

Abstract Among preprocessing techniques for quantified Boolean formula (QBF) solving, quantified blocked clause elimination (QBCE) has been found to be extremely effective. We investigate the power of dynamically applying QBCE in search-based QBF solving with clause and cube learning (QCDCL). This dynamic application of QBCE is in sharp contrast to its typical use as a mere preprocessing technique. In our dynamic approach, QBCE is applied eagerly to the formula interpreted under the assignments that have been enumerated in QCDCL. The tight integration of QBCE in QCDCL results in a variant of cube learning which is exponentially stronger than the traditional method. We implemented our approach in the QBF solver DepQBF and ran experiments on instances from the QBF Gallery 2014. On application benchmarks, QCDCL with dynamic QBCE substantially outperforms traditional QCDCL. Moreover, our approach is compatible with incremental solving and can be combined with preprocessing techniques other than QBCE.

SAT Conference 2015 Conference Paper

Evaluating CDCL Variable Scoring Schemes

• Armin Biere
• Andreas Fröhlich

Abstract The VSIDS (variable state independent decaying sum) decision heuristic invented in the context of the CDCL (conflict-driven clause learning) SAT solver Chaff, is considered crucial for achieving high efficiency of modern SAT solvers on application benchmarks. This paper proposes ACIDS (average conflict-index decision score), a variant of VSIDS. The ACIDS heuristics is compared to the original implementation of VSIDS, its popular modern implementation EVSIDS (exponential VSIDS), the VMTF (variable move-to-front) scheme, and other related decision heuristics. They all share the important principle to select those variables as decisions, which recently participated in conflicts. The main goal of the paper is to provide an empirical evaluation to serve as a starting point for trying to understand the reason for the efficiency of these decision heuristics. In our experiments, it turns out that EVSIDS, VMTF, ACIDS behave very similarly, if implemented carefully.

AAAI Conference 2015 Conference Paper

Stochastic Local Search for Satisfiability Modulo Theories

• Andreas Fröhlich
• Armin Biere
• Christoph Wintersteiger
• Youssef Hamadi

Satisfiability Modulo Theories (SMT) is essential for many practical applications, e. g. , in hard- and software verification, and increasingly also in other scientific areas like computational biology. A large number of applications in these areas benefit from bit-precise reasoning over finite-domain variables. Current approaches in this area translate a formula over bit-vectors to an equisatisfiable propositional formula, which is then given to a SAT solver. In this paper, we present a novel stochastic local search (SLS) algorithm to solve SMT problems, especially those in the theory of bit-vectors, directly on the theory level. We explain how several successful techniques used in modern SLS solvers for SAT can be lifted to the SMT level. Experimental results show that our approach can compete with state-of-the-art bit-vector solvers on many practical instances and, sometimes, outperform existing solvers. This offers interesting possibilities in combining our approach with existing techniques, and, moreover, new insights into the importance of exploiting problem structure in SLS solvers for SAT. Our approach is modular and, therefore, extensible to support other theories, potentially allowing SLS to become part of the more general SMT framework.

SAT Conference 2014 Conference Paper

Detecting Cardinality Constraints in CNF

• Armin Biere
• Daniel Le Berre
• Emmanuel Lonca
• Norbert Manthey

Abstract We present novel approaches to detect cardinality constraints expressed in CNF. The first approach is based on a syntactic analysis of specific data structures used in SAT solvers to represent binary and ternary clauses, whereas the second approach is based on a semantic analysis by unit propagation. The syntactic approach computes an approximation of the cardinality constraints AtMost-1 and AtMost-2 constraints very fast, whereas the semantic approach has the property to be generic, i. e. it can detect cardinality constraints AtMost- k for any k, at a higher computation cost. Our experimental results suggest that both approaches are efficient at recovering AtMost-1 and AtMost-2 cardinality constraints.

SAT Conference 2014 Conference Paper

Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)

• Tomás Balyo
• Andreas Fröhlich
• Marijn J. H. Heule
• Armin Biere

Abstract Blocked clause elimination is a powerful technique in SAT solving. In recent work, it has been shown that it is possible to decompose any propositional formula into two subsets (blocked sets) such that both can be solved by blocked clause elimination. We extend this work in several ways. First, we prove new theoretical properties of blocked sets. We then present additional and improved ways to efficiently solve blocked sets. Further, we propose novel decomposition algorithms for faster decomposition or which produce blocked sets with desirable attributes. We use decompositions to reencode CNF formulas and to obtain circuits, such as AIGs, which can then be simplified by algorithms from circuit synthesis and encoded back to CNF. Our experiments demonstrate that these techniques can increase the performance of the SAT solver Lingeling on hard to solve application benchmarks.

SAT Conference 2014 Conference Paper

Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses

• Adrian Balint
• Armin Biere
• Andreas Fröhlich
• Uwe Schöning

Abstract Stochastic Local Search (SLS) solvers are considered one of the best solving technique for randomly generated problems and more recently also have shown great promise for several types of hard combinatorial problems. Within this work, we provide a thorough analysis of different implementation variants of SLS solvers on random and on hard combinatorial problems. By analyzing existing SLS implementations, we are able to discover new improvements inspired by CDCL solvers, which can speed up the search of all types of SLS solvers. Further, our analysis reveals that the multilevel break values of variables can be easily computed and used within the decision heuristic. By augmenting the probSAT solver with the new heuristic, we are able to reach new state-of-the-art performance on several types of SAT problems, especially on those with long clauses. We further provide a detailed analysis of the clause selection policy used in focused search SLS solvers.

LPAR Conference 2013 Conference Paper

Blocked Clause Decomposition

• Marijn J. H. Heule
• Armin Biere

Abstract We demonstrate that it is fairly easy to decompose any propositional formula into two subsets such that both can be solved by blocked clause elimination. Such a blocked clause decomposition is useful to cheaply detect backbone variables and equivalent literals. Blocked clause decompositions are especially useful when they are unbalanced, i. e. , one subset is much larger in size than the other one. We present algorithms and heuristics to obtain unbalanced decompositions efficiently. Our techniques have been implemented in the state-of-the-art solver Lingeling. Experiments show that the performance of Lingeling is clearly improved due to these techniques on application benchmarks of the SAT Competition 2013.

SAT Conference 2013 Conference Paper

Factoring Out Assumptions to Speed Up MUS Extraction

• Jean-Marie Lagniez
• Armin Biere

Abstract In earlier work on a limited form of extended resolution for CDCL based SAT solving, new literals were introduced to factor out parts of learned clauses. The main goal was to shorten clauses, reduce proof size and memory usage and thus speed up propagation and conflict analysis. Even though some reduction was achieved, the effectiveness of this technique was rather modest for generic SAT solving. In this paper we show that factoring out literals is particularly useful for incremental SAT solving, based on assumptions. This is the most common approach for incremental SAT solving and was pioneered by the authors of MINISAT. Our first contribution is to focus on factoring out only assumptions, and actually all eagerly. This enables the use of compact dedicated data structures, and naturally suggests a new form of clause minimization, our second contribution. As last main contribution, we propose to use these data structures to maintain a partial proof trace for learned clauses with assumptions, which gives us a cheap way to flush useless learned clauses. In order to evaluate the effectiveness of our techniques we implemented them within the version of MINISAT used in the publically available state-of-the-art MUS extractor MUSer. An extensive experimental evaluation shows that factoring out assumptions in combination with our novel clause minimization procedure and eager clause removal is particularly effective in reducing average clause size, improves running time and in general the state-of-the-art in MUS extraction.

SAT Conference 2012 Conference Paper

Concurrent Cube-and-Conquer - (Poster Presentation)

• Peter van der Tak
• Marijn J. H. Heule
• Armin Biere

Abstract Satisfiability solvers targeting industrial instances are currently almost always based on conflict-driven clause learning (CDCL) [5]. This technique can successfully solve very large instances. Yet on small, hard problems lookahead solvers [3] often perform better by applying much more reasoning in each search node and then recursively splitting the search space until a solution is found.

SAT Conference 2012 Conference Paper

Resolution-Based Certificate Extraction for QBF - (Tool Presentation)

• Aina Niemetz
• Mathias Preiner
• Florian Lonsing
• Martina Seidl
• Armin Biere

Abstract A certificate of (un)satisfiability for a quantified Boolean formula (QBF) represents sets of assignments to the variables, which act as witnesses for its truth value. Certificates are highly requested for practical applications of QBF like formal verification and model checking. We present an integrated set of tools realizing resolution-based certificate extraction for QBF in prenex conjunctive normal form. Starting from resolution proofs produced by the solver DepQBF, we describe the workflow consisting of proof checking, certificate extraction, and certificate checking. We implemented the steps of that workflow in stand-alone tools and carried out comprehensive experiments. Our results demonstrate the practical applicability of resolution-based certificate extraction.

SAT Conference 2011 Conference Paper

Efficient CNF Simplification Based on Binary Implication Graphs

• Marijn J. H. Heule
• Matti Järvisalo
• Armin Biere

Abstract This paper develops techniques for efficiently detecting redundancies in CNF formulas. We introduce the concept of hidden literals, resulting in the novel technique of hidden literal elimination. We develop a practical simplification algorithm that enables “ Unhiding ” various redundancies in a unified framework. Based on time stamping literals in the binary implication graph, the algorithm applies various binary clause based simplifications, including techniques that, when run repeatedly until fixpoint, can be too costly. Unhiding can also be applied during search, taking learnt clauses into account. We show that Unhiding gives performance improvements on real-world SAT competition benchmarks.

SAT Conference 2011 Conference Paper

Failed Literal Detection for QBF

• Florian Lonsing
• Armin Biere

Abstract Failed literal detection (FL) in SAT is a powerful approach for preprocessing. The basic idea is to assign a variable as assumption. If boolean constraint propagation (BCP) yields an empty clause then the negated assumption is necessary for satisfiability. Whereas FL is common in SAT, it cannot easily be applied to QBF due to universal quantification. We present two approaches for FL to preprocess prenex CNFs. The first one is based on abstraction where certain universal variables are treated as existentially quantified. Second we combine QBF-specific BCP (QBCP) in FL with Q-resolution to validate assignments learnt by FL. Finally we compare these two approaches to a third common approach based on SAT. It turns out that the three approaches are incomparable. Experimental evaluation demonstrates that FL for QBF can improve the performance of search- and elimination-based QBF solvers.

SAT Conference 2010 Conference Paper

Automated Testing and Debugging of SAT and QBF Solvers

• Robert Brummayer
• Florian Lonsing
• Armin Biere

Abstract Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.

SAT Conference 2010 Conference Paper

Integrating Dependency Schemes in Search-Based QBF Solvers

• Florian Lonsing
• Armin Biere

Abstract Many search-based QBF solvers implementing the DPLL algorithm for QBF (QDPLL) process formulae in prenex conjunctive normal form (PCNF). The quantifier prefix of PCNFs often results in strong variable dependencies which can influence solver performance negatively. A common approach to overcome this problem is to reconstruct quantifier structure e. g. by quantifier trees. Dependency schemes are a generalization of quantifier trees in the sense that more general dependency graphs can be obtained. So far, dependency graphs have not been applied in QBF solving. In this work we consider the problem of efficiently integrating dependency graphs in QDPLL. Thereby we generalize related work on integrating quantifier trees. By analyzing the core parts of QDPLL, we report on modifications necessary to profit from general dependency graphs. In comprehensive experiments we show that QDPLL using a particular dependency graph, despite of increased overhead, outperforms classical QDPLL relying on quantifier prefixes of PCNFs.

SAT Conference 2010 Conference Paper

Reconstructing Solutions after Blocked Clause Elimination

• Matti Järvisalo
• Armin Biere

Abstract Preprocessing has proven important in enabling efficient Boolean satisfiability (SAT) solving. For many real application scenarios of SAT it is important to be able to extract a full satisfying assignment for original SAT instances from a satisfying assignment for the instances after preprocessing. We show how such full solutions can be efficiently reconstructed from solutions to the conjunctive normal form (CNF) formulas resulting from applying a combination of various CNF preprocessing techniques implemented in the PrecoSAT solver—especially, blocked clause elimination combined with SatElite-style variable elimination and equivalence reasoning.

SAT Conference 2009 Conference Paper

A Compact Representation for Syntactic Dependencies in QBFs

• Florian Lonsing
• Armin Biere

Abstract Different quantifier types in Quantified Boolean Formulae (QBF) introduce variable dependencies which have to be taken into consideration when deciding satisfiability of a QBF. In this work, we focus on dependencies based on syntactically connected variables. We generalize our previous ideas for efficiently representing dependency sets of universal variables to existential ones. We obtain a dependency graph which is applicable to arbitrary QBF solvers. The core part of our work is the formulation and correctness proof of a static and compact, tree-shaped connection relation over equivalence classes of existential variables. In practice, this relation is constructed once from a given QBF and allows to share connection information among all variables. We report on practical aspects and demonstrate the effectiveness of our approach in experiments on structured formulae from QBF competitions. Further, we show by example that the common approach of quantifier scope analysis is not optimal among syntactic methods for dependency computation.

SAT Conference 2009 Conference Paper

Minimizing Learned Clauses

• Niklas Sörensson
• Armin Biere

Abstract Minimizing learned clauses is an effective technique to reduce memory usage and also speed up solving time. It has been implemented in MiniSat since 2005 and is now adopted by most modern SAT solvers in academia, even though it has not been described in the literature properly yet. With this paper we intend to close this gap and also provide a thorough experimental analysis of it’s effectiveness for the first time.

SAT Conference 2008 Conference Paper

Adaptive Restart Strategies for Conflict Driven SAT Solvers

• Armin Biere

Abstract As the SAT competition has shown, frequent restarts improve the speed of SAT solvers tremendously, particularly on satisfiable industrial instances. This paper presents a novel adaptive technique that measures the agility of the search process dynamically, which in turn is used to control the restart frequency. Experiments demonstrate, that this new dynamic restart strategy improves speed of our SAT solver PicoSAT on crafted instances considerably and on industrial instances slightly.

SAT Conference 2008 Conference Paper

Nenofex: Expanding NNF for QBF Solving

• Florian Lonsing
• Armin Biere

Abstract The topic of this paper is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form (NNF), which relies on expansion as the core technique for eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes the formula size to increase quadratically in the worst case, expansion on NNF is involved with only a linear increase of the formula size. This property motivates the use of NNF instead of CNF combined with expansion. In Nenofex, a formula in NNF is represented as a tree with structural restrictions in order to keep its size small and distances from nodes to the root short. Expansions of variables are scheduled based on estimated expansion cost. The variable with the smallest estimated cost is expanded first. In order to remove redundancy from the formula, limited versions of two approaches from the domain of circuit optimization have been integrated. Experimental results on latest benchmarks show that Nenofex indeed exceeds a given memory limit less frequently than a resolution-based QBF solver for CNF, but also that there is the need for runtime-related improvements.

SAT Conference 2007 Conference Paper

A First Step Towards a Unified Proof Checker for QBF

• Toni Jussila
• Armin Biere
• Carsten Sinz
• Daniel Kroening
• Christoph M. Wintersteiger

Abstract Compared to SAT, there is no simple concept of what a solution to a QBF problem is. Furthermore, as the series of QBF evaluations shows, the QBF solvers that are available often disagree. Thus, proof generation for QBF seems to be even more important than for SAT. In this paper we propose a new uniform proof format, which captures refutations and witnesses for a variety of QBF solvers, and is based on a novel extended resolution rule for QBF. Our experiments show the flexibility of this new format. We also identify shortcomings of our format and conjecture that a purely resolution based proof calculus is not powerful enough to trace the most efficient solvers.

SAT Conference 2006 Conference Paper

Extended Resolution Proofs for Symbolic SAT Solving with Quantification

• Toni Jussila
• Carsten Sinz
• Armin Biere

Abstract Symbolic SAT solving is an approach where the clauses of a CNF formula are represented using BDDs. These BDDs are then conjoined, and finally checking satisfiability is reduced to the question of whether the final BDD is identical to false. We present a method combining symbolic SAT solving with BDD quantification (variable elimination) and generation of extended resolution proofs. Proofs are fundamental to many applications, and our results allow the use of BDDs instead of—or in combination with—established proof generation techniques like clause learning. We have implemented a symbolic SAT solver with variable elimination that produces extended resolution proofs. We present details of our implementation, called EBDDRES, which is an extension of the system presented in [1], and also report on experimental results.

SAT Conference 2005 Conference Paper

Effective Preprocessing in SAT Through Variable and Clause Elimination

• Niklas Eén
• Armin Biere

Abstract Preprocessing SAT instances can reduce their size considerably. We combine variable elimination with subsumption and self-subsuming resolution, and show that these techniques not only shrink the formula further than previous preprocessing efforts based on variable elimination, but also decrease runtime of SAT solvers substantially for typical industrial SAT problems. We discuss critical implementation details that make the reduction procedure fast enough to be practical.

SAT Conference 2004 Conference Paper

Resolve and Expand

• Armin Biere

We present a novel expansion based decision procedure for quantified boolean formulas (QBF) in conjunctive normal form (CNF). The basic idea is to resolve existentially quantified variables and eliminate universal variables by expansion. This process is continued until the formula becomes propositional and can be solved by any SAT solver. On structured problems our implementation quantor is competitive with state-of-the-art QBF solvers based on DPLL. It is orders of magnitude faster on certain hard to solve instances.