| Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications A Biere, MJH Heule, H van Maaren, T Walsh IOS Press, 2009 | 3209 | 2009 |
| DRAT-trim: Efficient checking and trimming using expressive clausal proofs N Wetzler, MJH Heule, WA Hunt Jr International Conference on Theory and Applications of Satisfiability …, 2014 | 383 | 2014 |
| Solving and verifying the boolean pythagorean triples problem via cube-and-conquer MJH Heule, O Kullmann, VW Marek International Conference on Theory and Applications of Satisfiability …, 2016 | 382 | 2016 |
| Inprocessing rules M Järvisalo, MJH Heule, A Biere Conference on Automated Deduction (CADE), 355-370, 2012 | 320 | 2012 |
| Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads MJH Heule, O Kullmann, S Wieringa, A Biere Haifa Verification Conference 2011, 2012 | 285 | 2012 |
| Blocked clause elimination M Järvisalo, A Biere, MJH Heule Tools and Algorithms for the Construction and Analysis of Systems, 129-144, 2010 | 205 | 2010 |
| Trimming while checking clausal proofs MJH Heule, WA Hunt, N Wetzler 2013 Formal Methods in Computer-Aided Design, 181-188, 2013 | 191 | 2013 |
| Exact DFA identification using SAT solvers MJH Heule, S Verwer International Colloquium on Grammatical Inference, 66-79, 2010 | 187 | 2010 |
| Schur number five M Heule Proceedings of the AAAI Conference on Artificial Intelligence 32 (1), 2018 | 174 | 2018 |
| Efficient certified RAT verification L Cruz-Filipe, MJH Heule, WA Hunt Jr, M Kaufmann, P Schneider-Kamp International Conference on Automated Deduction, 220-236, 2017 | 165 | 2017 |
| The science of brute force MJH Heule, O Kullmann Communications of the ACM 60 (8), 70-79, 2017 | 154 | 2017 |
| Verifying refutations with extended resolution MJH Heule, WA Hunt Jr, N Wetzler International Conference on Automated Deduction, 345-359, 2013 | 132 | 2013 |
| SAT competition 2016: Recent developments T Balyo, M Heule, M Jarvisalo Proceedings of the AAAI Conference on Artificial Intelligence 31 (1), 2017 | 129 | 2017 |
| March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver M Heule, M Dufour, J Van Zwieten, H Van Maaren Theory and Applications of Satisfiability Testing, 345–359, 2005 | 129 | 2005 |
| The sat competition 2014 A Belov, D Diepold, M Heule, M Järvisalo Proc. SAT COMPETITION, 45, 2014 | 123* | 2014 |
| SAT competition 2020 N Froleyks, M Heule, M Iser, M Järvisalo, M Suda Artificial Intelligence 301, 103572, 2021 | 121 | 2021 |
| Automated reencoding of boolean formulas N Manthey, MJH Heule, A Biere Haifa Verification Conference, 102-117, 2012 | 121 | 2012 |
| Clause Elimination Procedures for CNF Formulas. MJH Heule, M Järvisalo, A Biere LPAR (Yogyakarta) 6397, 357-371, 2010 | 113 | 2010 |
| Look-ahead based SAT solvers MJH Heule, H van Maaren Handbook of satisfiability, 155-184, 2009 | 109 | 2009 |
| Clause elimination for SAT and QSAT MJH Heule, M Järvisalo, F Lonsing, M Seidl, A Biere Journal of Artificial Intelligence Research 53, 127-168, 2015 | 105 | 2015 |
Armin BiereProfessor of Computer Science, University of FreiburgVerified email at informatik.uni-freiburg.de
