Chapter DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs 2014 • Lecture Notes in Computer Science • 8561:422-429 Wetzler N, Heule MJH, Hunt WAJ
Conference Efficient Extraction of Skolem Functions from QRAT Proofs 2014 • 2014 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD) • 107-114 Heule MJH, Seidl M, Biere A
Chapter Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask) 2014 • Lecture Notes in Computer Science • 8561:317-332 Balyo T, Froehlich A, Heule MJH, Biere A
Chapter MUS Extraction Using Clausal Proofs 2014 • Lecture Notes in Computer Science • 8561:48-57 Belov A, Heule MJH, Marques-Silva J
Conference Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers 2014 • EPiC series in computing • 27:12-13 Heule M, Manthey N, Philipp T
Chapter A SAT Approach to Clique-Width 2013 • Lecture Notes in Computer Science • 7962:318-334 Heule MJH, Szeider S
Chapter Automated Reencoding of Boolean Formulas 2013 • Lecture Notes in Computer Science • 7857:102-117 Manthey N, Heule MJH, Biere A
Chapter Blocked Clause Decomposition 2013 • Lecture Notes in Computer Science • 8312:423-438 Heule MJH, Biere A
Conference Covered Clause Elimination 2013 • EPiC series in computing • 13:41-34 Heule M, Järvisalo M, Biere A
Chapter Guided Merging of Sequence Diagrams 2013 • Lecture Notes in Computer Science • 7745:164-183 Widl M, Biere A, Brosch P, Egly U, Heule M, Kappel G, Seidl M, Tompits H
Chapter Mechanical Verification of SAT Refutations with Extended Resolution 2013 • Lecture Notes in Computer Science • 7998:229-244 Wetzler N, Heule MJH, Hunt WAJ
Chapter Revisiting Hyper Binary Resolution 2013 • Lecture Notes in Computer Science • 7874:77-93 Heule MJH, Järvisalo M, Biere A
Journal Article Software model synthesis using satisfiability solvers 2013 • Empirical Software Engineering • 18(4):825-856 Heule MJH, Verwer S
Journal Article Symmetry in Gardens of Eden 2013 • Electronic Journal of Combinatorics • 20(3): Hartman C, Heule MJH, Kwekkeboom K, Noels A
Conference Trimming while Checking Clausal Proofs 2013 • 2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD) • 181-188 Heule MJH, Hunt WAJ, Wetzler N
Chapter Verifying Refutations with Extended Resolution 2013 • Lecture Notes in Computer Science • 7898:345-359 Heule MJH, Hunt WA, Wetzler N
Chapter Concurrent Cube-and-Conquer 2012 • Lecture Notes in Computer Science • 7317:475-476 van der Tak P, Heule MJH, Biere A
Conference Concurrent cube-and-conquer (Poster presentation) 2012 • Lecture Notes in Computer Science • 7317 LNCS:475-476 Van Der Tak P, Heule MJH, Biere A
Chapter Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads 2012 • Lecture Notes in Computer Science • 7261:50-65 Heule MJH, Kullmann O, Wieringa S, Biere A
Chapter Inprocessing Rules 2012 • Lecture Notes in Computer Science • 7364:355-370 Järvisalo M, Heule MJH, Biere A
Journal Article Simulating Circuit-Level Simplifications on CNF 2012 • Journal of Automated Reasoning • 49(4):583-619 Jarvisalo M, Biere A, Heule MJH
Chapter Between Restarts and Backjumps 2011 • Lecture Notes in Computer Science • 6695:216-229 Ramos A, van der Tak P, Heule MJH
Chapter EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation 2011 • Lecture Notes in Computer Science • 6695:367-368 Gableske O, Heule MJH
Chapter Efficient CNF Simplification Based on Binary Implication Graphs 2011 • Lecture Notes in Computer Science • 6695:201-215 Heule MJH, Jarvisalo M, Biere A
Journal Article Introduction to Mathematics of Satisfiability, Victor W. Marek, Chapman & Hall/CRC, 2009. Hardback, ISBN-13: 978-143980167-3, $89.95. 2011 • Theory and Practice of Logic Programming • 11(1):126-130 Heule M
