Marijn Heule

AAAI Conference 2026 Conference Paper

On the Edge of Core (Non-)Emptiness: An Automated Reasoning Approach to Approval-Based Multi-Winner Voting

• Ratip Emin Berker
• Emanuel Tewolde
• Vincent Conitzer
• Mingyu Guo
• Marijn Heule
• Lirong Xia

Core stability is a natural and well-studied notion for group fairness in multi-winner voting, where the task is to select a committee from a pool of candidates. We study the setting where voters either approve or disapprove of each candidate; here, it remains a major open problem whether a core-stable committee always exists. In this work, we develop an approach based on mixed-integer linear programming for deciding whether and when core-stable committees are guaranteed to exist. In contrast to SAT-based approaches popular in computational social choice, our method can produce proofs for a specific number of candidates independent of the number of voters. In addition to these computational gains, our program lends itself to a novel duality-based reformulation of the core stability problem, from which we obtain new existence results in special cases. Further, we use our framework to reveal previously unknown relationships between core stability and other desirable properties, such as notions of priceability.

AIJ Journal 2021 Journal Article

SAT Competition 2020

• Nils Froleyks
• Marijn Heule
• Ashlin Iser
• Matti Järvisalo
• Martin Suda

AAAI Conference 2020 Conference Paper

Constructing Minimal Perfect Hash Functions Using SAT Technology

• Sean Weaver
• Marijn Heule

Minimal perfect hash functions (MPHFs) are used to provide efficient access to values of large dictionaries (sets of keyvalue pairs). Discovering new algorithms for building MPHFs is an area of active research, especially from the perspective of storage efficiency. The information-theoretic limit for MPHFs is 1 ln 2 ≈ 1. 44 bits per key. The current best practical algorithms range between 2 and 4 bits per key. In this article, we propose two SAT-based constructions of MPHFs. Our first construction yields MPHFs near the informationtheoretic limit. For this construction, current state-of-the-art SAT solvers can handle instances where the dictionaries contain up to 40 elements, thereby outperforming the existing (brute-force) methods. Our second construction uses XOR- SAT filters to realize a practical approach with long-term storage of approximately 1. 83 bits per key.

TCS Journal 2019 Journal Article

Computing properties of stable configurations of thermodynamic binding networks

• Keenan Breik
• Chris Thachuk
• Marijn Heule
• David Soloveichik

AAAI Conference 2018 Conference Paper

Schur Number Five

• Marijn Heule

We present the solution of a century-old problem known as Schur Number Five: What is the largest (natural) number n such that there exists a five-coloring of the positive numbers up to n without a monochromatic solution of the equation a + b = c? We obtained the solution, n = 160, by encoding the problem into propositional logic and applying massively parallel satisfiability solving techniques on the resulting formula. We constructed and validated a proof of the solution to increase trust in the correctness of the multi-CPU-year computations. The proof is two petabytes in size and was certified using a formally verified proof checker, demonstrating that any result by satisfiability solvers—no matter how large—can now be validated using highly trustworthy systems.

AAAI Conference 2017 Conference Paper

SAT Competition 2016: Recent Developments

• Tomas Balyo
• Marijn Heule
• Matti Jarvisalo

We give an overview of SAT Competition 2016, the 2016 edition of the famous competition for Boolean satisfiability (SAT) solvers with over 20 years of history. A key aim is to point out “what’s hot” in SAT competitions in 2016, i. e. , new developments in the competition series, including new competition tracks and new solver techniques implemented in some of the award-winning solvers.

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.

AAAI Conference 2015 Conference Paper

What’s Hot in the SAT and ASP Competitions

• Marijn Heule
• Torsten Schaub

During the Vienna Summer of Logic, the first FLoC Olympic Games were organized, bringing together a dozen competitions related to logic. Here we present the highlights of the Satisfiability (SAT) and Answer Set Programming (ASP) competitions.

AAAI Conference 2010 Conference Paper

Symmetry in Solutions

• Marijn Heule
• Toby Walsh

We define the concept of an internal symmetry. This is a symmety within a solution of a constraint satisfaction problem. We compare this to solution symmetry, which is a mapping between different solutions of the same problem. We argue that we may be able to exploit both types of symmetry when finding solutions. We illustrate the potential of exploiting internal symmetries on two benchmark domains: Van der Waerden numbers and graceful graphs. By identifying internal symmetries we are able to extend the state of the art in both cases.