Marijn J. H. Heule

TACAS Conference 2026 Conference Paper

Orbitopal Fixing in SAT

• Markus Anders
• Cayden Codel
• Marijn J. H. Heule

JAIR Journal 2025 Journal Article

Certified Knowledge Compilation with Application to Formally Verified Model Counting

• Randal E. Bryant
• Wojciech Nawrocki
• Jeremy Avigad
• Marijn J. H. Heule

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision decomposable negation normal form (decision-DNNF). Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from decision-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.

SAT Conference 2025 Conference Paper

Certifying Projected Knowledge Compilation

• Randal E. Bryant
• Yong Kiam Tan
• Marijn J. H. Heule

Knowledge compilers convert Boolean formulas, given in conjunctive normal form (CNF), into representations that enable efficient evaluation of unweighted and weighted model counts, as well as a variety of other useful properties. With projected knowledge compilation, the generated representation describes the restriction of the formula to a designated set of data variables, with the remaining ones eliminated by existential quantification. Projected knowledge compilation has applications in a variety of domains, including formal verification and synthesis. This paper describes a formally verified proof framework for certifying the output of a projected knowledge compiler. It builds on an earlier clausal proof framework for certifying the output of a standard knowledge compiler. Extending the framework to projected compilation requires a method to represent Skolem assignments, describing how the quantified variables can be assigned, given an assignment for the data variables. We do so by extending the representation generated by the knowledge compiler to also encode Skolem assignments. We also refine the earlier framework, moving beyond purely clausal proofs to enable scaling certification to larger formulas. We present experimental results obtained by making small modifications to the D4 projected knowledge compiler and extensions of our earlier proof generator. We detail a soundness argument stating that a compiler output that passes our certifier is logically equivalent to the quantified input formula; the soundness argument has been formally validated using the HOL4 proof assistant. The checker also ensures that the compiler output satisfies the properties required for efficient unweighted and weighted model counting. We have developed two proof checkers for the certification framework: one written in C and designed for high performance and one written in CakeML and formally verified in HOL4.

SAT Conference 2025 Conference Paper

Problem Partitioning via Proof Prefixes

• Zachary Battleman
• Joseph E. Reeves
• Marijn J. H. Heule

Satisfiability solvers have been instrumental in tackling hard problems, including mathematical challenges that require years of computation. A key obstacle in efficiently solving such problems lies in effectively partitioning them into many, frequently millions of subproblems. Existing automated partitioning techniques, primarily based on lookahead methods, perform well on some instances but fail to generate effective partitions for many others. This paper introduces a powerful partitioning approach that leverages prefixes of proofs derived from conflict-driven clause-learning solvers. This method enables non-experts to harness the power of massively parallel SAT solving for their problems. We also propose a semantically-driven partitioning technique tailored for problems with large cardinality constraints, which frequently arise in optimization tasks. We evaluate our methods on diverse benchmarks, including combinatorial problems and formulas from SAT and MaxSAT competitions. Our results demonstrate that these techniques outperform existing partitioning strategies in many cases, offering improved scalability and efficiency.

SAT Conference 2025 Conference Paper

Reencoding Unique Literal Clauses

• Aeacus Sheng
• Joseph E. Reeves
• Marijn J. H. Heule

We present a lightweight reencoding technique that augments propositional formulas containing implicit or explicit exactly-one constraints with auxiliary variables derived from the order encoding. Our approach is based on the observation that many formulas contain clauses where each literal appears only in that clause, and that these unique literal clauses can be replaced by the corresponding sequential counter encoding of exactly-one constraints, which introduces the same variables as the order encoding. We implemented the reencoding in the state-of-the-art SAT solver CaDiCaL with support for proof logging and solution reconstruction. Experiments on SAT Competition benchmarks demonstrate that our technique enables solving dozens of additional formulas. We found that shuffling a formula before reencoding harms performance. To mitigate this issue, we introduce a method that sorts literals within clauses based on the formula structure before applying our reencoding. The same technique also predicts whether reencoding is likely to yield improvements.

AAAI Conference 2025 Conference Paper

The Impact of Literal Sorting on Cardinality Constraint Encodings

• Joseph E. Reeves
• João Filipe
• Min-Chien Hsu
• Ruben Martins
• Marijn J. H. Heule

The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form. Cardinality constraints are prevalent in numerous problems, prompting the development and study of various types of encoding. We present a novel approach to optimizing cardinality constraint encodings by exploring the impact of literal orderings within the constraints. By strategically placing related literals nearby each other, the encoding generates auxiliary variables in a hierarchical structure, enabling the solver to reason more abstractly about groups of related literals. Unlike conventional metrics such as formula size or propagation strength, our method leverages structural properties of the formula to redefine the roles of auxiliary variables to enhance the solver's learning capabilities. The experimental evaluation on benchmarks from the maximum satisfiability competition demonstrates that literal orderings can be more influential than the choice of the encoding type. Our literal ordering technique improves solver performance across various encoding techniques, underscoring the robustness of our approach.

SAT Conference 2024 Conference Paper

Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving

• Jiong Yang 0002
• Yaroslav A. Kharkov
• Yunong Shi
• Marijn J. H. Heule
• Bruno Dutertre

Quantum Computing (QC) is a new computational paradigm that promises significant speedup over classical computing in various domains. However, near-term QC faces numerous challenges, including limited qubit connectivity and noisy quantum operations. To address the qubit connectivity constraint, circuit mapping is required for executing quantum circuits on quantum computers. This process involves performing initial qubit placement and using the quantum SWAP operations to relocate non-adjacent qubits for nearest-neighbor interaction. Reducing the SWAP count in circuit mapping is essential for improving the success rate of quantum circuit execution as SWAPs are costly and error-prone. In this work, we introduce a novel circuit mapping method by combining incremental and parallel solving for Boolean Satisfiability (SAT). We present an innovative SAT encoding for circuit mapping problems, which significantly improves solver-based mapping methods and provides a smooth trade-off between compilation quality and compilation time. Through comprehensive benchmarking of 78 instances covering 3 quantum algorithms on 2 distinct quantum computer topologies, we demonstrate that our method is 26× faster than state-of-the-art solver-based methods, reducing the compilation time from hours to minutes for important quantum applications. Our method also surpasses the existing heuristics algorithm by 26% in SWAP count.

SAT Conference 2023 Conference Paper

Certified Knowledge Compilation with Application to Verified Model Counting

• Randal E. Bryant
• Wojciech Nawrocki
• Jeremy Avigad
• Marijn J. H. Heule

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision-decomposable, negation normal form (dec-DNNF). Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from dec-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.

SAT Conference 2023 Conference Paper

Effective Auxiliary Variables via Structured Reencoding

• Andrew Haberlandt
• Harrison Green
• Marijn J. H. Heule

Extended resolution shows that auxiliary variables are very powerful in theory. However, attempts to exploit this potential in practice have had limited success. One reasonably effective method in this regard is bounded variable addition (BVA), which automatically reencodes formulas by introducing new variables and eliminating clauses, often significantly reducing formula size. We find motivating examples suggesting that the performance improvement caused by BVA stems not only from this size reduction but also from the introduction of effective auxiliary variables. Analyzing specific packing-coloring instances, we discover that BVA is fragile with respect to formula randomization, relying on variable order to break ties. With this understanding, we augment BVA with a heuristic for breaking ties in a structured way. We evaluate our new preprocessing technique, Structured BVA (SBVA), on more than 29 000 formulas from previous SAT competitions and show that it is robust to randomization. In a simulated competition setting, our implementation outperforms BVA on both randomized and original formulas, and appears to be well-suited for certain families of formulas.

LPAR Conference 2023 Conference Paper

Toward Optimal Radio Colorings of Hypercubes via SAT-solving

• Bernardo Subercaseaux
• Marijn J. H. Heule

Radio 2-colorings of graphs are a generalization of vertex colorings motivated by the problem of assigning frequency channels in radio networks. In a radio 2-coloring of a graph, vertices are assigned integer colors so that the color of two vertices u and v differ by at least 2 if u and v are neighbors, and by at least 1 if u and v have a common neighbor. Our work improves the best-known bounds for optimal radio 2-colorings of small hypercube graphs, a combinatorial problem that has received significant attention in the past. We do so by using automated reasoning techniques such as symmetry breaking and Cube and Conquer, obtaining that for n = 7 and n = 8, the coding-theory upper bounds of Whittlesey et al. (1995) are not tight. Moreover, we prove the answer for n = 7 to be either 12 or 13, thus making a substantial step towards answering an open problem by Knuth (2015). Finally, we include several combinatorial observations that might be useful for further progress, while also arguing that fully determining the answer for n = 7 will require new techniques.

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.

SAT Conference 2022 Conference Paper

Relating Existing Powerful Proof Systems for QBF

• Leroy Chew
• Marijn J. H. Heule

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not have strategy extraction. Because EUR heavily uses resolution paths our technique also brings resolution path dependency and sequent systems closer together. While we do not recommend G for practical applications this work can potentially show what features are needed for a new QBF checking format stronger than QRAT.

SAT Conference 2022 Conference Paper

The Packing Chromatic Number of the Infinite Square Grid Is at Least 14

• Bernardo Subercaseaux
• Marijn J. H. Heule

A packing k-coloring of a graph G = (V, E) is a mapping from V to {1, .. ., k} such that any pair of vertices u, v that receive the same color c must be at distance greater than c in G. Arguably the most fundamental problem regarding packing colorings is to determine the packing chromatic number of the infinite square grid. A sequence of previous works has proved this number to be between 13 and 15. Our work improves the lower bound to 14. Moreover, we present a new encoding that is asymptotically more compact than the previously used ones.

SoCS Conference 2021 Conference Paper

Avoiding Monochromatic Rectangles Using Shift Patterns

• Zhenjun Liu
• Leroy Chew
• Marijn J. H. Heule

We show that enforcing shift patterns significantly reduces the cost to construct grids without monochromatic rectangles. Additionally, we prove that all valid 3-colorings of a 10 by 10 grid are isomorphic.

SAT Conference 2021 Conference Paper

Chinese Remainder Encoding for Hamiltonian Cycles

• Marijn J. H. Heule

Abstract The Hamiltonian Cycle Problem (HCP) consists of two constraints: i) each vertex contributes exactly two edges to the cycle; and ii) there is exactly one cycle. The former can be encoded naturally and compactly, while the encodings of the latter either lack arc consistency or require an exponential number of clauses. We present a new, small encoding for HCP based on the Chinese remainder theorem. We demonstrate the effectiveness of the encoding on challenging HCP instances.

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.

LPAR Conference 2020 Conference Paper

Coloring Unit-Distance Strips using SAT

• Peter Oostema
• Ruben Martins
• Marijn J. H. Heule

Satisfiability (SAT) solving has become an important technology in computer-aided mathematics with various successes in number and graph theory. In this paper we apply SAT solvers to color infinitely long strips in the plane with a given height and number of colors. The coloring is constrained as follows: two points that are exactly unit distance apart must be colored differently. To finitize the problem, we tile the strips and all points on a tile have the same color. We evaluated our approach using two different tile shapes: squares and hexagons. The visualization of bounded height strips using 3 to 6 colors reveal patterns that are similar to the best known lower bounds for infinite strips. Our method can be a useful tool for mathematicians to search for patterns that can be generalized to infinite strips and allowed us to increase the lower bound for the strip height with 5 colors to an improved height of 1. 700084.

SAT Conference 2020 Conference Paper

Mycielski Graphs and PR Proofs

• Emre Yolcu
• Xinyu Wu
• Marijn J. H. Heule

Abstract Mycielski graphs are a family of triangle-free graphs \(M_k\) with arbitrarily high chromatic number. \(M_k\) has chromatic number k and there is a short informal proof of this fact, yet finding proofs of it via automated reasoning techniques has proved to be a challenging task. In this paper, we study the complexity of clausal proofs of the uncolorability of \(M_k\) with \(k-1\) colors. In particular, we consider variants of the \(\mathrm {PR}\) (propagation redundancy) proof system that are without new variables, and with or without deletion. These proof systems are of interest due to their potential uses for proof search. As our main result, we present a sublinear-length and constant-width \(\mathrm {PR}\) proof without new variables or deletion. We also implement a proof generator and verify the correctness of our proof. Furthermore, we consider formulas extended with clauses from the proof until a short resolution proof exists, and investigate the performance of CDCL in finding the short proof. This turns out to be difficult for CDCL with the standard heuristics. Finally, we describe an approach inspired by SAT sweeping to find proofs of these extended formulas.

LPAR Conference 2020 Conference Paper

Sensitivity Analysis of Locked Circuits

• Joseph Sweeney
• Marijn J. H. Heule
• Lawrence T. Pileggi

Globalization of integrated circuits manufacturing has led to increased security con- cerns, notably theft of intellectual property. In response, logic locking techniques have been developed for protecting designs, but many of these techniques have been shown to be vulnerable to SAT-based attacks. In this paper, we explore the use of Boolean sensi- tivity to analyze these locked circuits. We show that in typical circuits there is an inverse relationship between input width and sensitivity. We then demonstrate the utility of this relationship for deobfuscating circuits locked with a class of “provably secure” logic lock- ing techniques. We conclude with an example of how to resist this attack, although the resistance is shown to be highly circuit dependent.

SAT Conference 2020 Conference Paper

Sorting Parity Encodings by Reusing Variables

• Leroy Chew
• Marijn J. H. Heule

Abstract Parity reasoning is challenging for CDCL solvers: Refuting a formula consisting of two contradictory, differently ordered parity constraints of modest size is hard. Two alternative methods can solve these reordered parity formulas efficiently: binary decision diagrams and Gaussian Elimination (which requires detection of the parity constraints). Yet, implementations of these techniques either lack support of proof logging or introduce many extension variables. The compact, commonly-used encoding of parity constraints uses Tseitin variables. We present a technique for short clausal proofs that exploits these Tseitin variables to reorder the constraints within the DRAT system. The size of our refutations of reordered parity formulas is \(\mathcal {O}(n\log n)\).

SAT Conference 2019 Conference Paper

Local Search for Fast Matrix Multiplication

• Marijn J. H. Heule
• Manuel Kauers
• Martina Seidl

Abstract Laderman discovered a scheme for computing the product of two \(3\times 3\) matrices using only 23 multiplications in 1976. Since then, some more such schemes were proposed, but nobody knows how many such schemes there are and whether there exist schemes with fewer than 23 multiplications. In this paper we present two independent SAT-based methods for finding new schemes using 23 multiplications. Both methods allow computing a few hundred new schemes individually, and many thousands when combined. Local search SAT solvers outperform CDCL solvers consistently in this application.

SAT Conference 2017 Conference Paper

A Little Blocked Literal Goes a Long Way

• Benjamin Kiesl
• Marijn J. H. Heule
• Martina Seidl

Abstract Q-resolution is a generalization of propositional resolution that provides the theoretical foundation for search-based solvers of quantified Boolean formulas (QBFs). Recently, it has been shown that an extension of Q-resolution, called long-distance resolution, is remarkably powerful both in theory and in practice. However, it was unknown how long-distance resolution is related to \(\mathsf {QRAT}\), a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that \(\mathsf {QRAT}\) polynomially simulates long-distance resolution. Two simple rules of \(\mathsf {QRAT}\) are crucial for our simulation— blocked-literal addition and blocked-literal elimination. Based on the simulation, we implemented a tool that transforms long-distance-resolution proofs into \(\mathsf {QRAT}\) proofs. In a case study, we compare long-distance-resolution proofs of the well-known Kleine Büning formulas with corresponding \(\mathsf {QRAT}\) proofs.

IJCAI Conference 2017 Conference Paper

Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method

• Marijn J. H. Heule
• Oliver Kullmann
• Victor W. Marek

A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem [Heule et al. , 2016], delivering the largest proof yet, of 200 terabytes in size. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, based on integrating the “old” and “new” methods of SAT solving.

SAT Conference 2016 Conference Paper

Computing Maximum Unavoidable Subgraphs Using SAT Solvers

• C. K. Cuong
• Marijn J. H. Heule

Abstract Unavoidable subgraphs have been widely studied in the context of Ramsey Theory. The research in this area focuses on highly structured graphs such as cliques, cycles, paths, stars, trees, and wheels. We propose to study maximum unavoidable subgraphs measuring the size in the number of edges. We computed maximum unavoidable subgraphs for graphs up to order nine via SAT solving and observed that these subgraphs are less structured, although all are bipartite. Additionally, we found large unavoidable bipartite subgraphs up to order twelve. We also present the concept of multi-component unavoidable subgraphs and show that large multi-component subgraphs are unavoidable in small graphs. We envision that maximum unavoidable subgraphs can be exploited using an alternative approach to breaking graph symmetries.

SAT Conference 2016 Conference Paper

Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer

• Marijn J. H. Heule
• Oliver Kullmann
• V. Wiktor Marek

Abstract The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set \(\mathbb {N}= \{1, 2, \dots \}\) of natural numbers be divided into two parts, such that no part contains a triple ( a, b, c ) with \(a^2 + b^2 = c^2\)? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.

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.

SAT Conference 2014 Conference Paper

DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs

• Nathan Wetzler
• Marijn J. H. Heule
• Warren A. Hunt Jr.

Abstract The DRAT-trim tool is a satisfiability proof checker based on the new DRAT proof format. Unlike its predecessor, DRUP-trim, all presently known SAT solving and preprocessing techniques can be validated using DRAT-trim. Checking time of a proof is comparable to the running time of the proof-producing solver. Memory usage is also similar to solving memory consumption, which overcomes a major hurdle of resolution-based proof checkers. The DRAT-trim tool can emit trimmed formulas, optimized proofs, and new TraceCheck + dependency graphs. We describe the output that is produced, what optimizations have been made to check RAT clauses, and potential applications of the tool.

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

MUS Extraction Using Clausal Proofs

• Anton Belov
• Marijn J. H. Heule
• João Marques-Silva 0001

Abstract Recent work introduced an effective method for extraction of reduced unsatisfiable cores of CNF formulas as a by-product of validation of clausal proofs emitted by conflict-driven clause learning SAT solvers. In this paper, we demonstrate that this method for trimming CNF formulas can also benefit state-of-the-art tools for the computation of a Minimal Unsatisfiable Subformula (MUS). Furthermore, we propose a number of techniques that improve the quality of trimming, and demonstrate a significant positive impact on the performance of MUS extractors from the improved trimming.

SAT Conference 2013 Conference Paper

A SAT Approach to Clique-Width

• Marijn J. H. Heule
• Stefan Szeider

Abstract Clique-width is a graph invariant that has been widely studied in combinatorics and computer science. However, computing the clique-width of a graph is an intricate problem, the exact clique-width is not known even for very small graphs. We present a new method for computing the clique-width of graphs based on an encoding to propositional satisfiability (SAT) which is then evaluated by a SAT solver. Our encoding is based on a reformulation of clique-width in terms of partitions that utilizes an efficient encoding of cardinality constraints. Our SAT-based method is the first to discover the exact clique-width of various small graphs, including famous graphs from the literature as well as random graphs of various density. With our method we determined the smallest graphs that require a small pre-described clique-width.

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

Between Restarts and Backjumps

• Antonio Ramos
• Peter van der Tak
• Marijn J. H. Heule

Abstract This paper introduces a novel technique that significantly reduces the computational costs to perform a restart in conflict-driven clause learning (CDCL) solvers. Our technique exploits the observation that CDCL solvers make many redundant propagations after a restart. It efficiently predicts which decisions will be made after a restart. This prediction is used to backtrack to the first level at which heuristics may select a new decision rather than performing a complete restart. In general, the number of conflicts that are encountered while solving a problem can be reduced by increasing the restart frequency, even though the solving time may increase. Our technique counters the latter effect. As a consequence CDCL solvers will favor more frequent restarts.

SAT Conference 2011 Conference Paper

EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation

• Oliver Gableske
• Marijn J. H. Heule

Abstract While the application of unit propagation (UP) is of vital importance in systematic search solvers to solve structured problems of the SAT competitions [8], its application in stochastic local search (SLS) solvers is rare. Examples for combining UP with SLS solvers are UnitWalk [4] and QingTing [6] and both solvers show strong performance on structured instances.

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

Dynamic Symmetry Breaking by Simulating Zykov Contraction

• Bas Schaafsma
• Marijn J. H. Heule
• Hans van Maaren

Abstract We present a new method to break symmetry in graph coloring problems. While most alternative techniques add symmetry breaking predicates in a pre-processing step, we developed a learning scheme that translates each encountered conflict into one conflict clause which covers equivalent conflicts arising from any permutation of the colors. Our technique introduces new Boolean variables during the search. For many problems the size of the resolution refutation can be significantly reduced by this technique. Although this is shown for various hand-made refutations, it is rarely used in practice, because it is hard to determine which variables to introduce defining useful predicates. In case of graph coloring, the reason for each conflicting coloring can be expressed as a node in the Zykov-tree, that stems from merging some vertices and adding some edges. So, we focus on variables that represent the Boolean expression that two vertices can be merged (if set to true), or that an edge can be placed between them (if set to false). Further, our algorithm reduces the number of introduced variables by reusing them. We implemented our technique in the state-of-the-art solver minisat. It is competitive with alternative SAT based techniques for graph coloring problems. Moreover, our technique can be used on top of other symmetry breaking techniques. In fact, combined with adding symmetry breaking predicates, huge performance gains are realized.

SAT Conference 2007 Conference Paper

Effective Incorporation of Double Look-Ahead Procedures

• Marijn J. H. Heule
• Hans van Maaren

Abstract We introduce an adaptive algorithm to control the use of the double look-ahead procedure. This procedure sometimes enhances the performance of look-ahead based satisfiability solvers. Current use of this procedure is driven by static heuristics. Experiments show that over a wide variety of instances, different parameter settings result in optimal performance. Moreover, a strategy that yields fast performance on one particular class of instances may cause a significant slowdown on other families. Using a single adaptive strategy, we accomplish performances close to the optimal performances reached by the various static settings. On some families, we clearly outperform even the fastest performance based on static heuristics. This paper provides a description of the algorithm and a comparison with the static strategies. This method is incorporated in march_dl, satz, and kcnfs. Also, the dynamic behavior of the algorithm is illustrated by adaptation plots on various benchmarks.

SAT Conference 2007 Conference Paper

From Idempotent Generalized Boolean Assignments to Multi-bit Search

• Marijn J. H. Heule
• Hans van Maaren

Abstract This paper shows that idempotents in finite rings of integers can act as Generalized Boolean Assignments (GBA’s) by providing a completeness theorem. We introduce the notion of a generic Generalized Boolean Assignment. The mere propagation of such an assignment reveals feasibility (existence of a solution) of a formula in propositional logic. Then, we demystify this general concept by formulating the process on the bit-level: It turns out that propagation of a GBA only simulates bitwise (non-communicating) parallel computing. We capitalize on this by modifying the state-of-the-art local search Sat solver UnitWalk accordingly. This modification involves a more complicated parallelism.

SAT Conference 2005 Conference Paper

Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming

• Marijn J. H. Heule
• Hans van Maaren

Abstract We introduce two incomplete polynomial time algorithms to solve satisfiability problems which both use Linear Programming (LP) techniques. First, the FlipFlop LP attempts to simulate a Quadratic Program which would solve the CNF at hand. Second, the WeightedLinearAutarky LP is an extended variant of the LinearAutarky LP as defined by Kullmann [6] and iteratively updates its weights to find autarkies in a given formula. Besides solving satisfiability problems, this LP could also be used to study the existence of autark assignments in formulas. Results within the experimental domain (up to 1000 variables) show a considerably sharper lower bound for the uniform random 3- Sat phase transition density than the proved lower bound of the myopic algorithm (> 3. 26) by Achlioptas [1] and even than that of the greedy algorithm (> 3. 52) proposed by Kaporis [5].

SAT Conference 2004 Conference Paper

Aligning CNF- and Equivalence-reasoning

• Marijn J. H. Heule
• Hans van Maaren

Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translating to CNF. The best known example of this feature is probably provided by the parity-family. The larger such CNF formulas cannot be solved in reasonable time if no extra reasoning with - and detection of - these clauses is incorporated. That is, in solving these formulas, there is a more or less separated algorithmic device in dealing with these equivalence clauses, called equivalence reasoning, and another dealing with the remaining clauses. In this paper we propose a way to align these two reasoning devices by introducing parameters for which we establish optimal settings over a variety of existing benchmarks. We obtain a truly convincing speed up in solving such formulas with respect to the best solving methods existing so far.