MH

Marijn Heule

View Pure Profile

Authored

20 records found

Aligning CNF- and equivalence-reasoning
Conference paper - M.J.H. Heule, H. van Maaren
Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the parity-family. Large instances of such CNF formulas cannot be solved in reasonable time if no detection of, ...

March-eq - Implementing additional reasoning into efficient look-ahead SAT solver
This paper discusses several techniques to make the look- ahead architecture for satisfiability (Sat) solvers more competitive. Our contribution consists of reduction of the computational costs to perform look-ahead and a cheap integration of both equivalence reasoning and local ...

Using a satisfiability solver to identify deterministic finite state automata
Conference paper - M.J.H. Heule, S.E. Verwer

Clause Elimination Procedures for CNF Formula
Conference paper - M.J.H. Heule, M Jarvisalo, A Biere

Effective Incorporation of Double Look-Ahead Procedures
Conference paper - M.J.H. Heule, H. van Maaren

Automated Reencoding of Boolean Formulas
Conference paper - N Manthey, M.J.H. Heule, A Biere

Covered Clause Elimination
Conference paper - M.J.H. Heule, M Järvisalo, A Biere

From Idempotent Generalized Boolean Assignments to Multi-bit Search
Conference paper - M.J.H. Heule, H. van Maaren

March_dl: Adding adaptive heuristics and a new branding strategy
Journal article - M.J.H. Heule, H. van Maaren

Sums of squares based approximation algorithms for MAX-SAT

Prototypes for Automated Architectural 3D-Layout

Whose side are you on? Finding solutions in a biased search-tree
Conference paper - M.J.H. Heule, H. van Maaren

A New Method to Construct Lower Bounds for Van der Waerden Numbers

Look-Ahead Based SAT Solvers
Book chapter - M.J.H. Heule, H. van Maaren

Symbiosis of Search and Heuristics for Random 3-SAT
Conference paper - S Mijnders, B. De Wilde, M.J.H. Heule

Inprocessing Rules
Conference paper - M Järvisalo, M.J.H. Heule, A Biere

SmArT solving: Tools and techniques for satisfiability solvers
Doctoral thesis - M.J.H. Heule

Observed lower bounds for random 3-sat phase transition density using linear programming
Conference paper - M.J.H. Heule, H. van Maaren

Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads
Conference paper - M.J.H. Heule, O Kullmann, S. Wieringa, A Biere

Blocked Clause Elimination
Conference paper - M Jarvisalo, A Biere, M.J.H. Heule