Marijn Heule
#21,474
Most Influential Person Now
American computer scientist, known for developing SAT solving proofs to solve mathematical problems
Marijn Heule's AcademicInfluence.com Rankings
Marijn Heulecomputer-science Degrees
Computer Science
#1776
World Rank
#1840
Historical Rank
#847
USA Rank
Database
#8337
World Rank
#8720
Historical Rank
#1099
USA Rank
Download Badge
Computer Science
Marijn Heule's Degrees
- PhD Computer Science University of Texas at Austin
- Masters Computer Science University of Texas at Austin
- Bachelors Computer Science University of Texas at Austin
Similar Degrees You Can Earn
Why Is Marijn Heule Influential?
(Suggest an Edit or Addition)According to Wikipedia, Marienus Johannes Hendrikus Heule is a Dutch computer scientist at Carnegie Mellon University who studies SAT solvers. Heule has used these solvers to resolve mathematical conjectures such as the Boolean Pythagorean triples problem, Schur's theorem number 5, and Keller's conjecture in dimension seven.
Marijn Heule's Published Works
Published Works
- Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications (2009) (531)
- Handbook of satisfiability (2009) (485)
- Inprocessing Rules (2012) (203)
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer (2016) (190)
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (2014) (182)
- Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads (2011) (146)
- Blocked Clause Elimination (2010) (137)
- Trimming while checking clausal proofs (2013) (105)
- Exact DFA Identification Using SAT Solvers (2010) (101)
- March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver (2004) (96)
- SAT Competition 2016: Recent Developments (2017) (94)
- Clause Elimination Procedures for CNF Formulas (2010) (80)
- Automated Reencoding of Boolean Formulas (2012) (77)
- Efficient Certified RAT Verification (2016) (74)
- Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions (2017) (72)
- Verifying Refutations with Extended Resolution (2013) (70)
- Schur Number Five (2017) (67)
- Clause Elimination for SAT and QSAT (2015) (65)
- Efficient CNF Simplification Based on Binary Implication Graphs (2011) (65)
- The science of brute force (2017) (63)
- Look-Ahead Based SAT Solvers (2021) (60)
- Simulating Circuit-Level Simplifications on CNF (2012) (58)
- Software model synthesis using satisfiability solvers (2013) (52)
- Aligning CNF- and Equivalence-reasoning (2004) (47)
- A Unified Proof System for QBF Preprocessing (2014) (46)
- March_dl: Adding Adaptive Heuristics and a New Branching Strategy (2006) (43)
- Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions (2017) (38)
- Efficient extraction of Skolem functions from QRAT proofs (2014) (38)
- A New Method to Construct Lower Bounds for Van der Waerden Numbers (2007) (37)
- Expressing Symmetry Breaking in DRAT Proofs (2015) (36)
- Efficient, Verified Checking of Propositional Proofs (2017) (35)
- Proceedings of SAT Competition 2013 (2013) (34)
- Short Proofs Without New Variables (2017) (32)
- Solution Validation and Extraction for QBF Preprocessing (2016) (31)
- Mechanical Verification of SAT Refutations with Extended Resolution (2013) (31)
- Computing Small Unit-Distance Graphs with Chromatic Number 5 (2018) (29)
- Dynamic Symmetry Breaking by Simulating Zykov Contraction (2009) (29)
- SAT Competition 2018 (2019) (29)
- Proofs for Satisfiability Problems (2014) (27)
- The DRAT format and DRAT-trim checker (2016) (27)
- Between Restarts and Backjumps (2011) (26)
- Covered Clause Elimination (2010) (26)
- Extended Resolution Simulates DRAT (2018) (25)
- Guided Merging of Sequence Diagrams (2012) (25)
- PRuning Through Satisfaction (2017) (25)
- MUS Extraction Using Clausal Proofs (2014) (25)
- A SAT Approach to Clique-Width (2013) (25)
- The Resolution of Keller’s Conjecture (2019) (23)
- SAT Competition 2020 (2021) (23)
- What a Difference a Variable Makes (2018) (22)
- Uniform Sampling from Kconfig Feature Models (2019) (22)
- EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation (2011) (22)
- Bridging the gap between easy generation and efficient verification of unsatisfiability proofs (2014) (21)
- Strong Extension-Free Proof Systems (2019) (21)
- New ways to multiply 3 x 3-matrices (2019) (20)
- Reusing the Assignment Trail in CDCL Solvers (2011) (20)
- Symbiosis of Search and Heuristics for Random 3-SAT (2014) (20)
- Cube-and-Conquer for Satisfiability (2018) (19)
- Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method (2017) (19)
- Revisiting Hyper Binary Resolution (2013) (19)
- Blocked Clause Decomposition (2013) (19)
- SmArT solving: tools and techniques for satisfiability solvers (2008) (18)
- Finding Invariants of Distributed Systems: It's a Small (Enough) World After All (2021) (17)
- Effective Incorporation of Double Look-Ahead Procedures (2007) (15)
- Encoding Redundancy for Satisfaction-Driven Clause Learning (2019) (14)
- A Little Blocked Literal Goes a Long Way (2017) (14)
- Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask) (2014) (14)
- Sums of squares based approximation algorithms for MAX-SAT (2008) (13)
- Symmetry within Solutions (2010) (13)
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver (2021) (13)
- Compositional Propositional Proofs (2015) (12)
- Whose side are you on? Finding solutions in a biased search-tree (2008) (12)
- Solving games: Dependence of applicable solving procedures (2007) (12)
- Modeling Techniques for Logic Locking (2020) (12)
- Solving edge-matching problems with satisfiability solvers (2009) (12)
- Towards Ultra Rapid Restarts (2014) (12)
- Local Search for Fast Matrix Multiplication (2019) (11)
- Concurrent Cube-and-Conquer (2014) (11)
- Parallel SAT Solving using Bit-level Operations (2008) (11)
- cake_lpr: Verified Propagation Redundancy Checking in CakeML (2021) (11)
- Blocked Literals Are Universal (2015) (10)
- Clausal Proofs of Mutilated Chessboards (2019) (10)
- A SAT Approach to Clique-Width (2013) (9)
- Theory and Applications of Satisfiability Testing -- SAT 2015 (2015) (9)
- Symmetry in Gardens of Eden (2013) (8)
- Computing properties of stable configurations of thermodynamic binding networks (2017) (8)
- Trimming Graphs Using Clausal Proof Optimization (2019) (8)
- A Flexible Proof Format for SAT Solver-Elaborator Communication (2021) (8)
- Scalable Uniform Sampling for Real-World Software Product Lines (2020) (8)
- What's Hot in the SAT and ASP Competitions (2015) (8)
- Truth Assignments as Conditional Autarkies (2019) (7)
- Concurrent Cube-and-Conquer - (Poster Presentation) (2012) (7)
- Proceedings of SAT Race 2019: Solver and Benchmark Descriptions (2019) (7)
- Sorting Parity Encodings by Reusing Variables (2020) (7)
- SAT COMPETITION 2016 Solver and Benchmark Descriptions (7)
- Prototypes for Automated Architectural 3D-Layout (2007) (7)
- Clausal Proof Compression (2016) (7)
- The Effect of Scrambling CNFs (2019) (6)
- The Quest for Perfect and Compact Symmetry Breaking for Graph Problems (2016) (6)
- Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers (2014) (6)
- Clausal Proofs for Pseudo-Boolean Reasoning (2022) (6)
- Deep Bound Hardware Model Checking Instances , Quadratic Propagations Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017 (2017) (6)
- Edinburgh Research Explorer Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP (2015) (6)
- Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver (2021) (5)
- Sensitivity Analysis of Locked Circuits (2020) (5)
- Skolem Function Continuation for Quantified Boolean Formulas (2017) (5)
- Optimal Symmetry Breaking for Graph Problems (2019) (4)
- The Potential of Interference-Based Proof Systems (2017) (4)
- An Automated Approach to the Collatz Conjecture (2021) (4)
- The Implication Problem of Computing Policies (2015) (4)
- Symmetry in Solutions (2010) (4)
- Tighter Bounds on Directed Ramsey Number R(7) (2020) (4)
- Constructing Minimal Perfect Hash Functions Using SAT Technology (2019) (4)
- Avoiding triples in arithmetic progression (2017) (3)
- CNF Symmetry Breaking Options in Conflict Driven SAT Solving (2005) (3)
- Simulating Strong Practical Proof Systems with Extended Resolution (2020) (3)
- Computing Maximum Unavoidable Subgraphs Using SAT Solvers (2016) (3)
- Coloring Unit-Distance Strips using SAT (2020) (3)
- March eq : Implementing Efficiency and Additional Reasoning into a Lookahead SAT-Solver (2004) (3)
- From Idempotent Generalized Boolean Assignments to Multi-bit Search (2007) (3)
- Using a satisfiability solver to identify deterministic finite state automata (2009) (2)
- SAT-Inspired Eliminations for Superposition (2021) (2)
- Bipartite Perfect Matching Benchmarks (2021) (2)
- Analysis of Computing Policies Using SAT Solvers (2016) (2)
- Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions (2017) (1)
- Easier variants of notorious math problems (2021) (1)
- Compact Symmetry Breaking for Tournaments (2022) (1)
- Chinese Remainder Encoding for Hamiltonian Cycles (2021) (1)
- A Study of Divide and Distribute Fixed Weights and its Variants ∗ (2021) (1)
- Mycielski Graphs and PR Proofs (2020) (1)
- Analysis of Computing Policies Using SAT Solvers (Short Paper) (2016) (1)
- Moving Definition Variables in Quantified Boolean Formulas (2022) (1)
- Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML (2023) (1)
- From Cliques to Colorings and Back Again (2022) (1)
- Preprocessing of Propagation Redundant Clauses (2022) (1)
- Proofs of Unsatisfiability (2021) (1)
- The Packing Chromatic Number of the Infinite Square Grid Is at Least 14 (2022) (1)
- A programmable, energy-minimal dataflow compiler and architecture (2022) (1)
- Solution Validation and Extraction for QBF Preprocessing (2016) (0)
- Computing a Smaller Unit-Distance Graph with Chromatic Number 5 via Proof Trimming (2019) (0)
- CARD, a cardinality constraints based solver (2008) (0)
- Exponential separations using guarded extension variables (2022) (0)
- Propositional Proof Skeletons (2023) (0)
- Migrating Solver State (2022) (0)
- A Linear Weight Transfer Rule for Local Search (2023) (0)
- M ay 2 01 9 New ways to multiply 3 × 3-matrices 1 (2019) (0)
- Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming (2005) (0)
- An Impossible Asylum (2021) (0)
- 12345 efghi UNIVERSITY OF WALES SWANSEA REPORT SERIES Decomposing clause-sets : Integrating DLL algorithms , tree decompositions and hypergraph cuts for variable-and clause-based graph representations of CNF ’ s by Marijn Heule and Oliver Kullmann (2006) (0)
- Handbook of Satisfiability: Preface (2009) (0)
- XOR Local Search for Boolean Brent Equations (2021) (0)
- The Impact of Bounded Variable Elimination on Solving Pigeonhole Formulas (2021) (0)
- Introduction to Mathematics of Satisfiability, Victor W. Marek, Chapman & Hall/CRC, 2009. Hardback, ISBN-13: 978-143980167-3, $89.95 (2010) (0)
- Satisfiability Solvers (2014) (0)
- Reusing the Assignment Trail in CDCL Solvers system description (2011) (0)
- Optimal Symmetry Breaking for Graph Problems (2019) (0)
- Propositional Proof Skeletons (cid:63) (2023) (0)
- Mini-tutorial on conflict-driven clause learning (CDCL) (2014) (0)
- Towards the shortest DRAT proof of the Pigeonhole Principle (2022) (0)
- Avoiding Monochromatic Rectangles Using Shift Patterns (2020) (0)
- Exemplary Achievements Industrial Use of ACL 2 : Applications , Achievements , Challenges , and Directions (2017) (0)
- 44 55 v 1 [ cs . D S ] 18 F eb 2 01 4 Symbiosis of Search and Heuristics for Random 3SAT (2014) (0)
- A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications (2019) (0)
- Everything's Bigger in Texas: "The Largest Math Proof Ever" (2017) (0)
- Pragmatics of SAT 2015 and 2018 The Effect of Scrambling CNFs ∗ (2019) (0)
- Software model synthesis using satisfiability solvers (2012) (0)
- Blocked Clause Elimination and its Extensions (2010) (0)
- Strong Extension-Free Proof Systems (2019) (0)
- Simulating Circuit-Level Simplifications on CNF (2011) (0)
- Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers (2023) (0)
- The Packing Chromatic Number of the Infinite Square Grid is 15 (2023) (0)
- Mixed Base Rewriting for the Collatz Conjecture (2021) (0)
- L O ] 8 D ec 2 01 6 Efficient Certified RAT Verification (0)
This paper list is powered by the following services:
Other Resources About Marijn Heule
What Schools Are Affiliated With Marijn Heule?
Marijn Heule is affiliated with the following schools: