Journal Article The Science of Brute Force 2017 • Communications of the ACM • 60(8):70-79 Heule MJH, Kullmann O
Conference Analysis of computing policies using sat solvers 2016 • Lecture Notes in Computer Science • 10083 LNCS:190-194 Heule MJH, Reaz R, Acharya HB, Gouda MG
Chapter Analysis of Computing Policies Using SAT Solvers (Short Paper) 2016 • Lecture Notes in Computer Science • 10083:190-194 Heule MJH, Reaz R, Acharya HB, Gouda MG
Chapter Computing Maximum Unavoidable Subgraphs Using SAT Solvers 2016 • Lecture Notes in Computer Science • 9710:196-211 Cuong CK, Heule MJH
Chapter Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer 2016 • Lecture Notes in Computer Science • 9710:228-245 Heule MJH, Kullmann O, Marek VW
Journal Article A SAT Approach to Clique-Width 2015 • ACM Transactions on Computational Logic • 16(3): Heule MJH, Szeider S
Chapter Blocked Literals Are Universal 2015 • Lecture Notes in Computer Science • 9058:436-442 Heule MJH, Seidl M, Biere A
Journal Article Clause Elimination for SAT and QSAT 2015 • The journal of artificial intelligence research • 53:127-168 Heule M, Jarvisalo M, Lonsing F, Seidl M, Biere A
Chapter Compositional Propositional Proofs 2015 • Lecture Notes in Computer Science • 9450:444-459 Heule MJH, Biere A
Chapter Expressing Symmetry Breaking in DRAT Proofs 2015 • Lecture Notes in Computer Science • 9195:591-606 Heule MJH, Hunt WAJ, Wetzler N
Chapter The implication problem of computing policies 2015 • Lecture Notes in Computer Science • 9212:109-123 Reaz R, Ali M, Gouda MG, Heule MJH, Elmallah ES
Conference Theory and Applications of Satisfiability Testing - SAT 2015: 18th International Conference Austin, TX, USA, September 24-27, 2015 Proceedings 2015 • Lecture Notes in Computer Science • 9340: Heule M, Weaver S
Conference What's Hot in the SAT and ASP Competitions 2015 • Proceedings of the ... AAAI Conference on Artificial Intelligence. AAAI Conference on Artificial Intelligence • 4322-4323 Heule MJH, Schaub T
Chapter A Unified Proof System for QBF Preprocessing 2014 • Lecture Notes in Computer Science • 8562:91-106 Heule MJH, Seidl M, Biere A
Journal Article Bridging the gap between easy generation and efficient verification of unsatisfiability proofs 2014 • Software Testing Verification and Reliability • 24(8):593-607 Heule MJH, Hunt WAJ, Wetzler N
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 LNCS:318-334 Heule MJH, Szeider S
Chapter Automated reencoding of Boolean formulas 2013 • Lecture Notes in Computer Science • 7857 LNCS:102-117 Manthey N, Heule MJH, Biere A
Chapter Blocked clause decomposition 2013 • Lecture Notes in Computer Science • 8312 LNCS:423-438 Heule MJH, Biere A