Travelled to:
1 × Cyprus
1 × Finland
1 × Portugal
2 × Austria
2 × Canada
2 × Germany
2 × USA
3 × United Kingdom
Collaborated with:
H.v.Maaren A.Biere W.A.H.Jr. N.Wetzler M.Järvisalo S.Szeider O.Gableske M.Seidl A.Belov J.Marques-Silva A.Ramos P.v.d.Tak B.Schaafsma T.Balyo A.Fröhlich M.Dufour J.v.Zwieten M.Widl P.Brosch U.Egly G.Kappel H.Tompits
Talks about:
proof (4) use (4) sat (4) reason (3) effici (3) cnf (3) symmetri (2) express (2) equival (2) clausal (2)
Person: Marijn Heule
DBLP: Heule:Marijn
Facilitated 1 volumes:
Contributed to:
Wrote 21 papers:
- CADE-2015-HeuleHW #proving #symmetry
- Expressing Symmetry Breaking in DRAT Proofs (MH, WAHJ, NW), pp. 591–606.
- IJCAR-2014-HeuleSB #preprocessor #proving
- A Unified Proof System for QBF Preprocessing (MH, MS, AB), pp. 91–106.
- SAT-2014-BalyoFHB #afraid to ask #set
- Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask) (TB, AF, MH, AB), pp. 317–332.
- SAT-2014-BelovHM #proving #using
- MUS Extraction Using Clausal Proofs (AB, MH, JMS), pp. 48–57.
- SAT-2014-WetzlerHH #named #performance #proving #using
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (NW, MH, WAHJ), pp. 422–429.
- CADE-2013-HeuleHW #verification
- Verifying Refutations with Extended Resolution (MH, WAHJ, NW), pp. 345–359.
- SAT-2013-HeuleS #approach #clique #satisfiability
- A SAT Approach to Clique-Width (MH, SS), pp. 318–334.
- IJCAR-2012-JarvisaloHB
- Inprocessing Rules (MJ, MH, AB), pp. 355–370.
- SLE-2012-WidlBBEHKST #diagrams #sequence chart
- Guided Merging of Sequence Diagrams (MW, AB, PB, UE, MH, GK, MS, HT), pp. 164–183.
- SAT-2011-GableskeH #named #random #satisfiability #using
- EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation (OG, MH), pp. 367–368.
- SAT-2011-HeuleJB #graph #performance
- Efficient CNF Simplification Based on Binary Implication Graphs (MH, MJ, AB), pp. 201–215.
- SAT-2011-RamosTH
- Between Restarts and Backjumps (AR, PvdT, MH), pp. 216–229.
- TACAS-2010-JarvisaloBH
- Blocked Clause Elimination (MJ, AB, MH), pp. 129–144.
- SAT-2009-SchaafsmaHM #simulation #symmetry
- Dynamic Symmetry Breaking by Simulating Zykov Contraction (BS, MH, HvM), pp. 223–236.
- SAT-2007-HeuleM #multi
- From Idempotent Generalized Boolean Assignments to Multi-bit Search (MH, HvM), pp. 134–147.
- SAT-2007-HeuleM07a #effectiveness
- Effective Incorporation of Double Look-Ahead Procedures (MH, HvM), pp. 258–271.
- SAT-2005-HeuleM #bound #linear #programming #random #satisfiability #using
- Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming (MH, HvM), pp. 122–134.
- SAT-2004-HeuleM
- Aligning CNF- and Equivalence-reasoning (MH, HvM), pp. 174–180.
- SAT-J-2004-HeuleDZM05 #implementation #named #performance #reasoning #satisfiability
- March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver (MH, MD, JvZ, HvM), pp. 345–359.
- SAT-J-2004-HeuleM05
- Aligning CNF- and Equivalence-Reasoning (MH, HvM), pp. 145–156.