Bryant, Randal E.; Heule, Marijn J. H. Generating extended resolution proofs with a BDD-based SAT solver. (English) Zbl 07760992 ACM Trans. Comput. Log. 24, No. 4, Paper No. 31, 28 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{R. E. Bryant} and \textit{M. J. H. Heule}, ACM Trans. Comput. Log. 24, No. 4, Paper No. 31, 28 p. (2023; Zbl 07760992) Full Text: DOI
Reeves, Joseph E.; Heule, Marijn J. H.; Bryant, Randal E. Preprocessing of propagation redundant clauses. (English) Zbl 07753650 J. Autom. Reasoning 67, No. 3, Paper No. 31, 26 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{J. E. Reeves} et al., J. Autom. Reasoning 67, No. 3, Paper No. 31, 26 p. (2023; Zbl 07753650) Full Text: DOI OA License
Yolcu, Emre; Aaronson, Scott; Heule, Marijn J. H. An automated approach to the Collatz conjecture. (English) Zbl 07702721 J. Autom. Reasoning 67, No. 2, Paper No. 15, 44 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{E. Yolcu} et al., J. Autom. Reasoning 67, No. 2, Paper No. 15, 44 p. (2023; Zbl 07702721) Full Text: DOI
Avigad, Jeremy; Baek, Seulkee; Bentkamp, Alexander; Heule, Marijn; Nawrocki, Wojciech An impossible asylum. (English) Zbl 07684392 Am. Math. Mon. 130, No. 5, 446-453 (2023). MSC: 03-01 03B35 68V15 PDFBibTeX XMLCite \textit{J. Avigad} et al., Am. Math. Mon. 130, No. 5, 446--453 (2023; Zbl 07684392) Full Text: DOI arXiv
Vukmirović, Petar; Blanchette, Jasmin; Heule, Marijn J. H. SAT-inspired eliminations for superposition. (English) Zbl 07650603 ACM Trans. Comput. Log. 24, No. 1, Paper No. 7, 25 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{P. Vukmirović} et al., ACM Trans. Comput. Log. 24, No. 1, Paper No. 7, 25 p. (2023; Zbl 07650603) Full Text: DOI
Reeves, Joseph E.; Heule, Marijn J. H.; Bryant, Randal E. Preprocessing of propagation redundant clauses. (English) Zbl 07628184 Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 106-124 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{J. E. Reeves} et al., Lect. Notes Comput. Sci. 13385, 106--124 (2022; Zbl 07628184) Full Text: DOI
Brakensiek, Joshua; Heule, Marijn; Mackey, John; Narváez, David The resolution of Keller’s conjecture. (English) Zbl 07606340 J. Autom. Reasoning 66, No. 3, 277-300 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{J. Brakensiek} et al., J. Autom. Reasoning 66, No. 3, 277--300 (2022; Zbl 07606340) Full Text: DOI arXiv
Baek, Seulkee; Carneiro, Mario; Heule, Marijn J. H. A flexible proof format for SAT solver-elaborator communication. (English) Zbl 07566059 Log. Methods Comput. Sci. 18, No. 2, Paper No. 3, 21 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{S. Baek} et al., Log. Methods Comput. Sci. 18, No. 2, Paper No. 3, 21 p. (2022; Zbl 07566059) Full Text: arXiv Link
Nawrocki, Wojciech; Liu, Zhenjun; Fröhlich, Andreas; Heule, Marijn J. H.; Biere, Armin XOR local search for Boolean Brent equations. (English) Zbl 07495589 Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 417-435 (2021). MSC: 68Q25 68R07 68T20 PDFBibTeX XMLCite \textit{W. Nawrocki} et al., Lect. Notes Comput. Sci. 12831, 417--435 (2021; Zbl 07495589) Full Text: DOI
Heule, Marijn J. H. Chinese remainder encoding for Hamiltonian cycles. (English) Zbl 07495575 Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 216-224 (2021). MSC: 68Q25 68R07 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule}, Lect. Notes Comput. Sci. 12831, 216--224 (2021; Zbl 07495575) Full Text: DOI
Froleyks, Nils; Heule, Marijn; Iser, Markus; Järvisalo, Matti; Suda, Martin SAT competition 2020. (English) Zbl 1478.68320 Artif. Intell. 301, Article ID 103572, 25 p. (2021). MSC: 68T20 68R07 PDFBibTeX XMLCite \textit{N. Froleyks} et al., Artif. Intell. 301, Article ID 103572, 25 p. (2021; Zbl 1478.68320) Full Text: DOI
Yolcu, Emre; Aaronson, Scott; Heule, Marijn J. H. An automated approach to the Collatz conjecture. (English) Zbl 07437095 Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 468-484 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{E. Yolcu} et al., Lect. Notes Comput. Sci. 12699, 468--484 (2021; Zbl 07437095) Full Text: DOI arXiv
Bryant, Randal E.; Heule, Marijn J. H. Dual proof generation for quantified Boolean formulas with a BDD-based solver. (English) Zbl 07437093 Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 433-449 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{R. E. Bryant} and \textit{M. J. H. Heule}, Lect. Notes Comput. Sci. 12699, 433--449 (2021; Zbl 07437093) Full Text: DOI
Tan, Yong Kiam; Heule, Marijn J. H.; Myreen, Magnus O. cake_lpr: verified propagation redundancy checking in CakeML. (English) Zbl 1474.68194 Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 223-241 (2021). MSC: 68Q60 68V15 PDFBibTeX XMLCite \textit{Y. K. Tan} et al., Lect. Notes Comput. Sci. 12652, 223--241 (2021; Zbl 1474.68194) Full Text: DOI
Bryant, Randal E.; Heule, Marijn J. H. Generating extended resolution proofs with a BDD-based SAT solver. (English) Zbl 1467.68203 Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 76-93 (2021). MSC: 68V15 68R07 68T20 PDFBibTeX XMLCite \textit{R. E. Bryant} and \textit{M. J. H. Heule}, Lect. Notes Comput. Sci. 12651, 76--93 (2021; Zbl 1467.68203) Full Text: DOI arXiv
Baek, Seulkee; Carneiro, Mario; Heule, Marijn J. H. A flexible proof format for SAT solver-elaborator communication. (English) Zbl 1467.68159 Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 59-75 (2021). MSC: 68T20 68R07 PDFBibTeX XMLCite \textit{S. Baek} et al., Lect. Notes Comput. Sci. 12651, 59--75 (2021; Zbl 1467.68159) Full Text: DOI arXiv
Heule, Marijn J. H.; Kauers, Manuel; Seidl, Martina New ways to multiply \(3 \times 3\)-matrices. (English) Zbl 1491.68276 J. Symb. Comput. 104, 899-916 (2021). Reviewer: Elaine Wong (Linz) MSC: 68W30 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., J. Symb. Comput. 104, 899--916 (2021; Zbl 1491.68276) Full Text: DOI arXiv
Biere, Armin (ed.); Heule, Marijn (ed.); Van Maaren, Hans (ed.); Walsh, Toby (ed.) Handbook of satisfiability. In 2 parts. 2nd updated and revised edition. (English) Zbl 1456.68001 Frontiers in Artificial Intelligence and Applications 336. Amsterdam: IOS Press (ISBN 978-1-64368-160-3/pbk; 978-1-64368-161-0/ebook). xvii, 1465 p. (2021). MSC: 68-00 68Q60 68R07 68T20 68T27 00B15 PDFBibTeX XMLCite \textit{A. Biere} (ed.) et al., Handbook of satisfiability. In 2 parts. 2nd updated and revised edition. Amsterdam: IOS Press (2021; Zbl 1456.68001) Full Text: Link
Brakensiek, Joshua; Heule, Marijn; Mackey, John; Narváez, David The resolution of Keller’s conjecture. (English) Zbl 07614506 Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12166, 48-65 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{J. Brakensiek} et al., Lect. Notes Comput. Sci. 12166, 48--65 (2020; Zbl 07614506) Full Text: DOI
Yolcu, Emre; Wu, Xinyu; Heule, Marijn J. H. Mycielski graphs and PR proofs. (English) Zbl 07331022 Pulina, Luca (ed.) et al., Theory and applications of satisfiability testing – SAT 2020. 23rd international conference, Alghero, Italy, July 3–10, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12178, 201-217 (2020). MSC: 68Q25 68R07 68T20 PDFBibTeX XMLCite \textit{E. Yolcu} et al., Lect. Notes Comput. Sci. 12178, 201--217 (2020; Zbl 07331022) Full Text: DOI
Chew, Leroy; Heule, Marijn J. H. Sorting parity encodings by reusing variables. (English) Zbl 07331008 Pulina, Luca (ed.) et al., Theory and applications of satisfiability testing – SAT 2020. 23rd international conference, Alghero, Italy, July 3–10, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12178, 1-10 (2020). MSC: 68Q25 68R07 68T20 PDFBibTeX XMLCite \textit{L. Chew} and \textit{M. J. H. Heule}, Lect. Notes Comput. Sci. 12178, 1--10 (2020; Zbl 07331008) Full Text: DOI
Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin Simulating strong practical proof systems with extended resolution. (English) Zbl 1468.68293 J. Autom. Reasoning 64, No. 7, 1247-1267 (2020). MSC: 68V15 03B05 03F20 68R07 68T20 PDFBibTeX XMLCite \textit{B. Kiesl} et al., J. Autom. Reasoning 64, No. 7, 1247--1267 (2020; Zbl 1468.68293) Full Text: DOI
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin Strong extension-free proof systems. (English) Zbl 1468.03011 J. Autom. Reasoning 64, No. 3, 533-554 (2020). MSC: 03B35 03F20 68V15 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., J. Autom. Reasoning 64, No. 3, 533--554 (2020; Zbl 1468.03011) Full Text: DOI
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin Encoding redundancy for satisfaction-driven clause learning. (English) Zbl 1527.68212 Vojnar, Tomáš (ed.) et al., Tools and algorithms for the construction and analysis of systems. 25th international conference, TACAS 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 11427, 41-58 (2019). MSC: 68T20 68V15 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 11427, 41--58 (2019; Zbl 1527.68212) Full Text: DOI
Heule, Marijn; Kauers, Manuel; Seidl, Martina A family of schemes for multiplying \(3 \times 3\) matrices with 23 coefficient multiplications. (English) Zbl 07640863 ACM Commun. Comput. Algebra 53, No. 3, 118-121 (2019). MSC: 68W30 PDFBibTeX XMLCite \textit{M. Heule} et al., ACM Commun. Comput. Algebra 53, No. 3, 118--121 (2019; Zbl 07640863) Full Text: DOI
Kiesl, Benjamin; Heule, Marijn J. H.; Biere, Armin Truth assignments as conditional autarkies. (English) Zbl 1437.68132 Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 48-64 (2019). MSC: 68R07 PDFBibTeX XMLCite \textit{B. Kiesl} et al., Lect. Notes Comput. Sci. 11781, 48--64 (2019; Zbl 1437.68132) Full Text: DOI
Heule, Marijn J. H.; Kauers, Manuel; Seidl, Martina Local search for fast matrix multiplication. (English) Zbl 1441.68225 Janota, Mikoláš (ed.) et al., Theory and applications of satisfiability testing – SAT 2019. 22nd international conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11628, 155-163 (2019). MSC: 68T20 68R07 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 11628, 155--163 (2019; Zbl 1441.68225) Full Text: DOI arXiv
Heule, Marijn J. H. Optimal symmetry breaking for graph problems. (English) Zbl 1474.68225 Math. Comput. Sci. 13, No. 4, 533-548 (2019). MSC: 68R10 68R07 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule}, Math. Comput. Sci. 13, No. 4, 533--548 (2019; Zbl 1474.68225) Full Text: DOI
Breik, Keenan; Thachuk, Chris; Heule, Marijn; Soloveichik, David Computing properties of stable configurations of thermodynamic binding networks. (English) Zbl 1423.68164 Theor. Comput. Sci. 785, 17-29 (2019). MSC: 68Q05 68Q17 92C45 PDFBibTeX XMLCite \textit{K. Breik} et al., Theor. Comput. Sci. 785, 17--29 (2019; Zbl 1423.68164) Full Text: DOI arXiv
Heule, Marijn J. H.; Biere, Armin What a difference a variable makes. (English) Zbl 1423.68419 Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 10806, 75-92 (2018). MSC: 68T15 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{A. Biere}, Lect. Notes Comput. Sci. 10806, 75--92 (2018; Zbl 1423.68419) Full Text: DOI
Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H. Extended resolution simulates \({\mathsf{DRAT}}\). (English) Zbl 1441.68278 Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 516-531 (2018). MSC: 68V15 68R07 PDFBibTeX XMLCite \textit{B. Kiesl} et al., Lect. Notes Comput. Sci. 10900, 516--531 (2018; Zbl 1441.68278) Full Text: DOI
Fazekas, Katalin; Heule, Marijn J. H.; Seidl, Martina; Biere, Armin Skolem function continuation for quantified Boolean formulas. (English) Zbl 1491.68192 Gabmeyer, Sebastian (ed.) et al., Tests and proofs. 11th international conference, TAP 2017, held as part of STAF 2017, Marburg, Germany, July 19–20, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10375, 129-138 (2017). MSC: 68T20 03B70 68V15 PDFBibTeX XMLCite \textit{K. Fazekas} et al., Lect. Notes Comput. Sci. 10375, 129--138 (2017; Zbl 1491.68192) Full Text: DOI Link
Wüstholz, Valentin; Olivo, Oswaldo; Heule, Marijn J. H.; Dillig, Isil Static detection of DoS vulnerabilities in programs that use regular expressions. (English) Zbl 1452.68060 Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part II. Berlin: Springer. Lect. Notes Comput. Sci. 10206, 3-20 (2017). MSC: 68N30 68Q45 PDFBibTeX XMLCite \textit{V. Wüstholz} et al., Lect. Notes Comput. Sci. 10206, 3--20 (2017; Zbl 1452.68060) Full Text: DOI arXiv
Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan Efficient, verified checking of propositional proofs. (English) Zbl 1483.68483 Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 269-284 (2017). MSC: 68V15 68T20 PDFBibTeX XMLCite \textit{M. Heule} et al., Lect. Notes Comput. Sci. 10499, 269--284 (2017; Zbl 1483.68483) Full Text: DOI
Kiesl, Benjamin; Heule, Marijn J. H.; Seidl, Martina A little blocked literal goes a long way. (English) Zbl 1496.68370 Gaspers, Serge (ed.) et al., Theory and applications of satisfiability testing – SAT 2017. 20th international conference, Melbourne, VIC, Australia, August 28 – September 1, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10491, 281-297 (2017). MSC: 68V15 68T20 PDFBibTeX XMLCite \textit{B. Kiesl} et al., Lect. Notes Comput. Sci. 10491, 281--297 (2017; Zbl 1496.68370) Full Text: DOI
Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt, Warren A. jun.; Kaufmann, Matt; Schneider-Kamp, Peter Efficient certified RAT verification. (English) Zbl 1494.68284 de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10395, 220-236 (2017). MSC: 68V15 68T20 PDFBibTeX XMLCite \textit{L. Cruz-Filipe} et al., Lect. Notes Comput. Sci. 10395, 220--236 (2017; Zbl 1494.68284) Full Text: DOI arXiv
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin Short proofs without new variables. (English) Zbl 1468.03010 de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10395, 130-147 (2017). MSC: 03B35 03F20 68V15 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 10395, 130--147 (2017; Zbl 1468.03010) Full Text: DOI
Heule, Marijn J. H. Avoiding triples in arithmetic progression. (English) Zbl 1370.05212 J. Comb. 8, No. 3, 391-422 (2017). MSC: 05D10 68R05 PDFBibTeX XMLCite \textit{M. J. H. Heule}, J. Comb. 8, No. 3, 391--422 (2017; Zbl 1370.05212) Full Text: DOI
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin Solution validation and extraction for QBF preprocessing. (English) Zbl 1409.68258 J. Autom. Reasoning 58, No. 1, 97-125 (2017). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., J. Autom. Reasoning 58, No. 1, 97--125 (2017; Zbl 1409.68258) Full Text: DOI
Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. (English) Zbl 1403.68226 Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40969-6/pbk; 978-3-319-40970-2/ebook). Lecture Notes in Computer Science 9710, 228-245 (2016). MSC: 68T15 05D10 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 9710, 228--245 (2016; Zbl 1403.68226) Full Text: DOI arXiv Link
Cuong, C. K.; Heule, M. J. H. Computing maximum unavoidable subgraphs using SAT solvers. (English) Zbl 1475.68236 Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 196-211 (2016). MSC: 68R10 68R07 68T20 PDFBibTeX XMLCite \textit{C. K. Cuong} and \textit{M. J. H. Heule}, Lect. Notes Comput. Sci. 9710, 196--211 (2016; Zbl 1475.68236) Full Text: DOI
Heule, Marijn J. H.; Biere, Armin Proofs for satisfiability problems. (English) Zbl 1431.03024 Woltzenlogel Paleo, Bruno (ed.) et al., All about proofs, proofs for all. London: College Publications. Stud. Log. (Lond.) 55, 1-22 (2015). MSC: 03B35 03F07 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{A. Biere}, Stud. Log. (Lond.) 55, 1--22 (2015; Zbl 1431.03024)
Reaz, Rezwana; Ali, Muqeet; Gouda, Mohamed G.; Heule, Marijn J. H.; Elmallah, Ehab S. The implication problem of computing policies. (English) Zbl 1428.68088 Pelc, Andrzej (ed.) et al., Stabilization, safety, and security of distributed systems. 17th international symposium, SSS 2015, Edmonton, AB, Canada, August 18–21, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9212, 109-123 (2015). MSC: 68M25 68Q25 PDFBibTeX XMLCite \textit{R. Reaz} et al., Lect. Notes Comput. Sci. 9212, 109--123 (2015; Zbl 1428.68088) Full Text: DOI
Heule, Marijn J. H.; Biere, Armin Compositional propositional proofs. (English) Zbl 1471.68310 Davis, Martin (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 20th international conference, LPAR-20 2015, Suva, Fiji, November 24–28, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9450, 444-459 (2015). MSC: 68V15 03B70 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{A. Biere}, Lect. Notes Comput. Sci. 9450, 444--459 (2015; Zbl 1471.68310) Full Text: DOI
Heule, Marijn J. H.; Hunt, Warren A. jun.; Wetzler, Nathan Expressing symmetry breaking in DRAT proofs. (English) Zbl 1465.68285 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 591-606 (2015). MSC: 68V15 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 9195, 591--606 (2015; Zbl 1465.68285) Full Text: DOI
Heule, Marijn J. H.; Szeider, Stefan A SAT approach to clique-width. (English) Zbl 1354.68240 ACM Trans. Comput. Log. 16, No. 3, Article No. 24, 27 p. (2015). MSC: 68T20 05C69 05C75 05C78 05C85 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{S. Szeider}, ACM Trans. Comput. Log. 16, No. 3, Article No. 24, 27 p. (2015; Zbl 1354.68240) Full Text: DOI arXiv
Heule, Marijn (ed.); Weaver, Sean (ed.) Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. (English) Zbl 1323.68009 Lecture Notes in Computer Science 9340. Cham: Springer (ISBN 978-3-319-24317-7/pbk; 978-3-319-24318-4/pbk). xix, 436 p. (2015). MSC: 68-06 68Q25 68T20 00B25 PDFBibTeX XMLCite \textit{M. Heule} (ed.) and \textit{S. Weaver} (ed.), Theory and applications of satisfiability testing -- SAT 2015. 18th international conference, Austin, TX, USA, September 24--27, 2015. Proceedings. Cham: Springer (2015; Zbl 1323.68009) Full Text: DOI
Heule, Marijn; Järvisalo, Matti; Lonsing, Florian; Seidl, Martina; Biere, Armin Clause elimination for SAT and QSAT. (English) Zbl 1336.68231 J. Artif. Intell. Res. (JAIR) 53, 127-168 (2015). MSC: 68T15 PDFBibTeX XMLCite \textit{M. Heule} et al., J. Artif. Intell. Res. (JAIR) 53, 127--168 (2015; Zbl 1336.68231) Full Text: DOI
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin A unified proof system for QBF preprocessing. (English) Zbl 1409.68257 Demri, Stéphane (ed.) et al., Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19–22, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8562, 91-106 (2014). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 8562, 91--106 (2014; Zbl 1409.68257) Full Text: DOI
Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A. jun. DRAT-trim: efficient checking and trimming using expressive clausal proofs. (English) Zbl 1423.68475 Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 422-429 (2014). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{N. Wetzler} et al., Lect. Notes Comput. Sci. 8561, 422--429 (2014; Zbl 1423.68475) Full Text: DOI
Balyo, Tomáš; Fröhlich, Andreas; Heule, Marijn J. H.; Biere, Armin Everything you always wanted to know about blocked sets (but were afraid to ask). (English) Zbl 1423.68435 Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 317-332 (2014). MSC: 68T20 PDFBibTeX XMLCite \textit{T. Balyo} et al., Lect. Notes Comput. Sci. 8561, 317--332 (2014; Zbl 1423.68435) Full Text: DOI
Belov, Anton; Heule, Marijn J. H.; Marques-Silva, Joao MUS extraction using clausal proofs. (English) Zbl 1423.68436 Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 48-57 (2014). MSC: 68T20 68Q25 68T15 PDFBibTeX XMLCite \textit{A. Belov} et al., Lect. Notes Comput. Sci. 8561, 48--57 (2014; Zbl 1423.68436) Full Text: DOI
Hartman, Christiaan; Heule, Marijn J. H.; Kwekkeboom, Kees; Noels, Alain Symmetry in Gardens of Eden. (English) Zbl 1295.68164 Electron. J. Comb. 20, No. 3, Research Paper P16, 19 p. (2013). MSC: 68Q80 PDFBibTeX XMLCite \textit{C. Hartman} et al., Electron. J. Comb. 20, No. 3, Research Paper P16, 19 p. (2013; Zbl 1295.68164) Full Text: Link
Heule, Marijn J. H.; Biere, Armin Blocked clause decomposition. (English) Zbl 1407.68451 McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8312, 423-438 (2013). MSC: 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{A. Biere}, Lect. Notes Comput. Sci. 8312, 423--438 (2013; Zbl 1407.68451) Full Text: DOI
Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A. jun. Mechanical verification of SAT refutations with extended resolution. (English) Zbl 1317.68236 Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 229-244 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{N. Wetzler} et al., Lect. Notes Comput. Sci. 7998, 229--244 (2013; Zbl 1317.68236) Full Text: DOI
Heule, Marijn J. H.; Szeider, Stefan A SAT approach to clique-width. (English) Zbl 1390.68501 Järvisalo, Matti (ed.) et al., Theory and applications of satisfiability testing – SAT 2013. 16th international conference, Helsinki, Finland, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39070-8/pbk). Lecture Notes in Computer Science 7962, 318-334 (2013). MSC: 68R10 05C35 05C69 05C70 05C85 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{S. Szeider}, Lect. Notes Comput. Sci. 7962, 318--334 (2013; Zbl 1390.68501) Full Text: DOI arXiv
Heule, Marijn J. H.; Hunt, Warren A. jun.; Wetzler, Nathan Verifying refutations with extended resolution. (English) Zbl 1381.68270 Bonacina, Maria Paola (ed.), Automated deduction – CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9–14, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38573-5/pbk). Lecture Notes in Computer Science 7898. Lecture Notes in Artificial Intelligence, 345-359 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 7898, 345--359 (2013; Zbl 1381.68270) Full Text: DOI
Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin Revisiting hyper binary resolution. (English) Zbl 1382.68223 Gomes, Carla (ed.) et al., Integration of AI and OR techniques in constraint programming for combinatorial optimization problems. 10th international conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18–22, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38170-6/pbk). Lecture Notes in Computer Science 7874, 77-93 (2013). MSC: 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 7874, 77--93 (2013; Zbl 1382.68223) Full Text: DOI
Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H. Simulating circuit-level simplifications on CNF. (English) Zbl 1267.94144 J. Autom. Reasoning 49, No. 4, 583-619 (2012). MSC: 94C10 68T15 68T20 PDFBibTeX XMLCite \textit{M. Järvisalo} et al., J. Autom. Reasoning 49, No. 4, 583--619 (2012; Zbl 1267.94144) Full Text: DOI
Järvisalo, Matti; Heule, Marijn J. H.; Biere, Armin Inprocessing rules. (English) Zbl 1358.68256 Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 355-370 (2012). MSC: 68T15 68T20 PDFBibTeX XMLCite \textit{M. Järvisalo} et al., Lect. Notes Comput. Sci. 7364, 355--370 (2012; Zbl 1358.68256) Full Text: DOI
van der Tak, Peter; Ramos, Antonio; Heule, Marijn Reusing the assignment trail in CDCL solvers. (English) Zbl 1331.68214 J. Satisf. Boolean Model. Comput. 7, No. 4, 133-138 (2011). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{P. van der Tak} et al., J. Satisf. Boolean Model. Comput. 7, No. 4, 133--138 (2011; Zbl 1331.68214)
Ramos, Antonio; van der Tak, Peter; Heule, Marijn J. H. Between restarts and backjumps. (English) Zbl 1330.68276 Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 216-229 (2011). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{A. Ramos} et al., Lect. Notes Comput. Sci. 6695, 216--229 (2011; Zbl 1330.68276) Full Text: DOI
Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin Efficient CNF simplification based on binary implication graphs. (English) Zbl 1330.68269 Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 201-215 (2011). MSC: 68T20 03B05 68T15 PDFBibTeX XMLCite \textit{M. J. H. Heule} et al., Lect. Notes Comput. Sci. 6695, 201--215 (2011; Zbl 1330.68269) Full Text: DOI
Heule, Marijn; Järvisalo, Matti; Biere, Armin Clause elimination procedures for CNF formulas. (English) Zbl 1306.68144 Fermüller, Christian G. (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-16241-1/pbk). Lecture Notes in Computer Science 6397, 357-371 (2010). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{M. Heule} et al., Lect. Notes Comput. Sci. 6397, 357--371 (2010; Zbl 1306.68144) Full Text: DOI
Heule, Marijn J. H.; Verwer, Sicco Exact DFA identification using SAT solvers. (English) Zbl 1291.68192 Sempere, José M. (ed.) et al., Grammatical inference: Theoretical results and applications. 10th international colloquium, ICGI 2010, Valencia, Spain, September 13–16, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-15487-4/pbk). Lecture Notes in Computer Science 6339. Lecture Notes in Artificial Intelligence, 66-79 (2010). MSC: 68Q32 68Q45 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{S. Verwer}, Lect. Notes Comput. Sci. 6339, 66--79 (2010; Zbl 1291.68192) Full Text: DOI
Järvisalo, Matti; Biere, Armin; Heule, Marijn Blocked clause elimination. (English) Zbl 1284.03208 Esparza, Javier (ed.) et al., Tools and algorithms for the construction and analysis of systems. 16th international conference, TACAS 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-12001-5/pbk). Lecture Notes in Computer Science 6015, 129-144 (2010). MSC: 03B70 03B05 68T15 94C10 PDFBibTeX XMLCite \textit{M. Järvisalo} et al., Lect. Notes Comput. Sci. 6015, 129--144 (2010; Zbl 1284.03208) Full Text: DOI
Schaafsma, Bas; Heule, Marijn J. H.; van Maaren, Hans Dynamic symmetry breaking by simulating Zykov contraction. (English) Zbl 1247.68260 Kullmann, Oliver (ed.), Theory and applications of satisfiability testing – SAT 2009. 12th international conference, SAT 2009, Swansea, UK, June 30–July 3, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02776-5/pbk). Lecture Notes in Computer Science 5584, 223-236 (2009). MSC: 68T20 05C15 05C80 PDFBibTeX XMLCite \textit{B. Schaafsma} et al., Lect. Notes Comput. Sci. 5584, 223--236 (2009; Zbl 1247.68260) Full Text: DOI
Biere, Armin (ed.); Heule, Marijn (ed.); van Maaren, Hans (ed.); Walsh, Toby (ed.) Handbook of satisfiability. (English) Zbl 1183.68568 Frontiers in Artificial Intelligence and Applications 185. Amsterdam: IOS Press (ISBN 978-1-58603-929-5/hbk). xiii, 966 p. (2009). MSC: 68T20 68Q60 68-00 68T27 PDFBibTeX XMLCite \textit{A. Biere} (ed.) et al., Handbook of satisfiability. Amsterdam: IOS Press (2009; Zbl 1183.68568) Full Text: Link
Heule, Marijn J. H.; van Maaren, Hans Whose side are you on? Finding solutions in a biased search-tree. (English) Zbl 1170.68595 J. Satisf. Boolean Model. Comput. 4, No. 2-4, 117-148 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{H. van Maaren}, J. Satisf. Boolean Model. Comput. 4, No. 2--4, 117--148 (2008; Zbl 1170.68595)
Heule, Marijn J. H.; van Maaren, Hans Parallel SAT solving using bit-level operations. (English) Zbl 1170.68594 J. Satisf. Boolean Model. Comput. 4, No. 2-4, 99-116 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{H. van Maaren}, J. Satisf. Boolean Model. Comput. 4, No. 2--4, 99--116 (2008; Zbl 1170.68594)
van Maaren, H.; van Norden, L.; Heule, M. J. H. Sums of squares based approximation algorithms for MAX-SAT. (English) Zbl 1152.68058 Discrete Appl. Math. 156, No. 10, 1754-1779 (2008). MSC: 68W25 68T20 90C22 PDFBibTeX XMLCite \textit{H. van Maaren} et al., Discrete Appl. Math. 156, No. 10, 1754--1779 (2008; Zbl 1152.68058) Full Text: DOI
Heule, Marijn; van Maaren, Hans Effective incorporation of double look-ahead procedures. (English) Zbl 1214.68356 Marques-Silva, João (ed.) et al., Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72787-3/pbk). Lecture Notes in Computer Science 4501, 258-271 (2007). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Heule} and \textit{H. van Maaren}, Lect. Notes Comput. Sci. 4501, 258--271 (2007; Zbl 1214.68356) Full Text: DOI
Heule, Marijn; van Maaren, Hans From idempotent generalized Boolean assignments to multi-bit search. (English) Zbl 1214.68355 Marques-Silva, João (ed.) et al., Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72787-3/pbk). Lecture Notes in Computer Science 4501, 134-147 (2007). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Heule} and \textit{H. van Maaren}, Lect. Notes Comput. Sci. 4501, 134--147 (2007; Zbl 1214.68355) Full Text: DOI
Heule, Marijn J. H.; van Maaren, Hans March_dl: adding adaptive heuristics and a new branching strategy. (English) Zbl 1116.68085 J. Satisf. Boolean Model. Comput. 2, No. 1-4, 47-59 (2006). MSC: 68T20 PDFBibTeX XMLCite \textit{M. J. H. Heule} and \textit{H. van Maaren}, J. Satisf. Boolean Model. Comput. 2, No. 1--4, 47--59 (2006; Zbl 1116.68085)
Heule, Marijn; Dufour, Mark; van Zwieten, Joris; van Maaren, Hans March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. (English) Zbl 1122.68599 Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 345-359 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Heule} et al., Lect. Notes Comput. Sci. 3542, 345--359 (2005; Zbl 1122.68599) Full Text: DOI
Heule, Marijn; van Maaren, Hans Aligning CNF- and equivalence-reasoning. (English) Zbl 1122.68600 Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 145-156 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Heule} and \textit{H. van Maaren}, Lect. Notes Comput. Sci. 3542, 145--156 (2005; Zbl 1122.68600) Full Text: DOI
Heule, Marijn; van Maaren, Hans Observed lower bounds for random 3-SAT phase transition density using linear programming. (English) Zbl 1128.68466 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 122-134 (2005). MSC: 68T20 90C05 68Q25 PDFBibTeX XMLCite \textit{M. Heule} and \textit{H. van Maaren}, Lect. Notes Comput. Sci. 3569, 122--134 (2005; Zbl 1128.68466) Full Text: DOI