Marijn Heule

Proceedings of the NASA Formal Methods - 15th International Symposium, 2023

Toward Optimal Radio Colorings of Hypercubes via SAT-solving.

[BibT_eX]

[DOI]

Bernardo Subercaseaux

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Exponential Separations Using Guarded Extension Variables.

[BibT_eX]

[DOI]

Emre Yolcu

Proceedings of the 14th Innovations in Theoretical Computer Science Conference, 2023

Without Loss of Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2023, 2023

Mariposa: Measuring SMT Instability in Automated Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2023

Verified Encodings for SAT Solvers.

[BibT_eX]

[DOI]

Cayden R. Codel

Jeremy Avigad

Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022

A Flexible Proof Format for SAT Solver-Elaborator Communication.

[BibT_eX]

[DOI]

Seulkee Baek

Mario Carneiro

Log. Methods Comput. Sci., 2022

The Resolution of Keller's Conjecture.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

Tighter Bounds on Directed Ramsey Number R(7).

[BibT_eX]

[DOI]

David Neiman

John Mackey

Graphs Comb., 2022

Towards the shortest DRAT proof of the Pigeonhole Principle.

[BibT_eX]

[DOI]

Isaac Grosof

Naifeng Zhang

CoRR, 2022

Moving Definition Variables in Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Joseph E. Reeves

Randal E. Bryant

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Clausal Proofs for Pseudo-Boolean Reasoning.

[BibT_eX]

[DOI]

Randal E. Bryant

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

The Packing Chromatic Number of the Infinite Square Grid Is at Least 14.

[BibT_eX]

[DOI]

Bernardo Subercaseaux

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

Relating Existing Powerful Proof Systems for QBF.

[BibT_eX]

[DOI]

Leroy Chew

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

Migrating Solver State.

[BibT_eX]

[DOI]

Md. Solimul Chowdhury

Michael W. Whalen

Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing, 2022

A programmable, energy-minimal dataflow compiler and architecture.

[BibT_eX]

[DOI]

Proceedings of the 55th IEEE/ACM International Symposium on Microarchitecture, 2022

Compact Symmetry Breaking for Tournaments.

[BibT_eX]

[DOI]

Evan Lohn

Chris Lambert

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

From Cliques to Colorings and Back Again.

[BibT_eX]

[DOI]

Anthony Karahalios

Willem-Jan van Hoeve

Proceedings of the 28th International Conference on Principles and Practice of Constraint Programming, 2022

2021

SAT-Inspired Eliminations for Superposition.

[BibT_eX]

[DOI]

Petar Vukmirovic

Jasmin Blanchette

Dataset, April, 2021

SAT-Inspired Eliminations for Superposition.

[BibT_eX]

[DOI]

Petar Vukmirovic

Jasmin Blanchette

Dataset, February, 2021

Look-Ahead Based SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

Proofs of Unsatisfiability.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

New ways to multiply 3 × 3-matrices.

[BibT_eX]

[DOI]

J. Symb. Comput., 2021

SAT Competition 2020.

[BibT_eX]

[DOI]

Artif. Intell., 2021

cake_lpr: Verified Propagation Redundancy Checking in CakeML.

[BibT_eX]

[DOI]

Yong Kiam Tan

Magnus O. Myreen

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Avoiding Monochromatic Rectangles Using Shift Patterns.

[BibT_eX]

[DOI]

Zhenjun Liu

Leroy Chew

Proceedings of the Fourteenth International Symposium on Combinatorial Search, 2021

XOR Local Search for Boolean Brent Equations.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Chinese Remainder Encoding for Hamiltonian Cycles.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Finding Invariants of Distributed Systems: It's a Small (Enough) World After All.

[BibT_eX]

[DOI]

Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation, 2021

Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver.

[BibT_eX]

[DOI]

Randal E. Bryant

Proceedings of the Automated Deduction - CADE 28, 2021

2020

The Resolution of Keller's Conjecture - Computation Logs.

[BibT_eX]

[DOI]

Dataset, April, 2020

Simulating Strong Practical Proof Systems with Extended Resolution.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Strong Extension-Free Proof Systems.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Mycielski Graphs and PR Proofs.

[BibT_eX]

[DOI]

Emre Yolcu

Xinyu Wu

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Sorting Parity Encodings by Reusing Variables.

[BibT_eX]

[DOI]

Leroy Chew

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Sensitivity Analysis of Locked Circuits.

[BibT_eX]

[DOI]

Joseph Sweeney

Lawrence T. Pileggi

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

Coloring Unit-Distance Strips using SAT.

[BibT_eX]

[DOI]

Peter Oostema

Ruben Martins

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

Modeling Techniques for Logic Locking.

[BibT_eX]

[DOI]

Joseph Sweeney

Lawrence T. Pileggi

Proceedings of the IEEE/ACM International Conference On Computer Aided Design, 2020

Constructing Minimal Perfect Hash Functions Using SAT Technology.

[BibT_eX]

[DOI]

Sean A. Weaver

Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

2019

Computing properties of stable configurations of thermodynamic binding networks.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2019

Optimal Symmetry Breaking for Graph Problems.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2019

SAT Competition 2018.

[BibT_eX]

[DOI]

Martin Suda

J. Satisf. Boolean Model. Comput., 2019

The Resolution of Keller's Conjecture.

[BibT_eX]

[DOI]

Joshua Brakensiek

John Mackey

CoRR, 2019

New ways to multiply 3 x 3-matrices.

[BibT_eX]

[DOI]

CoRR, 2019

A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2019

Encoding Redundancy for Satisfaction-Driven Clause Learning.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Local Search for Fast Matrix Multiplication.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Clausal Proofs of Mutilated Chessboards.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Trimming Graphs Using Clausal Proof Optimization.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2019

Truth Assignments as Conditional Autarkies.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2019

2018

What a Difference a Variable Makes.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

The Effect of Scrambling CNFs.

[BibT_eX]

[DOI]

Proceedings of Pragmatics of SAT 2015, 2018

Extended Resolution Simulates DRAT.

[BibT_eX]

[DOI]

Adrián Rebola-Pardo

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Schur Number Five.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

Cube-and-Conquer for Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017

Solution Validation and Extraction for QBF Preprocessing.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Computing properties of stable configurations of thermodynamic binding networks.

[BibT_eX]

[DOI]

CoRR, 2017

Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2017

The science of brute force.

[BibT_eX]

[DOI]

Commun. ACM, 2017

Skolem Function Continuation for Quantified Boolean Formulas.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 11th International Conference, 2017

Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

A Little Blocked Literal Goes a Long Way.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

Efficient, Verified Checking of Propositional Proofs.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method.

[BibT_eX]

[DOI]

Victor W. Marek

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

PRuning Through Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2017

Everything's Bigger in Texas: "The Largest Math Proof Ever".

[BibT_eX]

[DOI]

Proceedings of the GCAI 2017, 2017

Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions.

[BibT_eX]

[DOI]

J Strother Moore

Proceedings of the ARCADE 2017, 2017

Short Proofs Without New Variables.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

The Potential of Interference-Based Proof Systems.

[BibT_eX]

[DOI]

Proceedings of the ARCADE 2017, 2017

Efficient Certified RAT Verification.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

SAT Competition 2016: Recent Developments.

[BibT_eX]

[DOI]

Tomás Balyo

Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 2017

2016

The DRAT format and DRAT-trim checker.

[BibT_eX]

[DOI]

CoRR, 2016

The Quest for Perfect and Compact Symmetry Breaking for Graph Problems.

[BibT_eX]

[DOI]

Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2016

Analysis of Computing Policies Using SAT Solvers (Short Paper).

[BibT_eX]

[DOI]

Rezwana Reaz

Hrishikesh B. Acharya

Mohamed G. Gouda

Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2016

Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer.

[BibT_eX]

[DOI]

Victor W. Marek

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Computing Maximum Unavoidable Subgraphs Using SAT Solvers.

[BibT_eX]

[DOI]

C. K. Cuong

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

2015

A SAT Approach to Clique-Width.

[BibT_eX]

[DOI]

Stefan Szeider

ACM Trans. Comput. Log., 2015

Clause Elimination for SAT and QSAT.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2015

The Implication Problem of Computing Policies.

[BibT_eX]

[DOI]

Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2015

Blocked Literals Are Universal.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Clausal Proof Compression.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2015, 2015

Compositional Propositional Proofs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Expressing Symmetry Breaking in DRAT Proofs.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

What's Hot in the SAT and ASP Competitions.

[BibT_eX]

[DOI]

Torsten Schaub

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014

Bridging the gap between easy generation and efficient verification of unsatisfiability proofs.

[BibT_eX]

[DOI]

Softw. Test. Verification Reliab., 2014

Concurrent Cube-and-Conquer.

[BibT_eX]

[DOI]

CoRR, 2014

Symbiosis of Search and Heuristics for Random 3-SAT.

[BibT_eX]

[DOI]

Sid Mijnders

Boris de Wilde

CoRR, 2014

Towards Ultra Rapid Restarts.

[BibT_eX]

[DOI]

Shai Haim

CoRR, 2014

DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers.

[BibT_eX]

[DOI]

Norbert Manthey

Tobias Philipp

Proceedings of the POS-14. Fifth Pragmatics of SAT workshop, 2014

MUS Extraction Using Clausal Proofs.

[BibT_eX]

[DOI]

Anton Belov

João Marques-Silva

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask).

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

Efficient extraction of Skolem functions from QRAT proofs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

A Unified Proof System for QBF Preprocessing.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Software model synthesis using satisfiability solvers.

[BibT_eX]

[DOI]

Sicco Verwer

Empir. Softw. Eng., 2013

Symmetry in Gardens of Eden.

[BibT_eX]

[DOI]

Electron. J. Comb., 2013

Blocked Clause Decomposition.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Mechanical Verification of SAT Refutations with Extended Resolution.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Trimming while checking clausal proofs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Revisiting Hyper Binary Resolution.

[BibT_eX]

[DOI]

Proceedings of the Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 2013

Verifying Refutations with Extended Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

2012

Simulating Circuit-Level Simplifications on CNF.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

Guided Merging of Sequence Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Software Language Engineering, 5th International Conference, 2012

Concurrent Cube-and-Conquer - (Poster Presentation).

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Automated Reencoding of Boolean Formulas.

[BibT_eX]

[DOI]

Norbert Manthey

Proceedings of the Hardware and Software: Verification and Testing, 2012

Inprocessing Rules.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

<i>Introduction to Mathematics of Satisfiability</i>, Victor W. Marek, Chapman & Hall/CRC, 2009. Hardback, ISBN-13: 978-143980167-3, $89.95.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2011

Reusing the Assignment Trail in CDCL Solvers.

[BibT_eX]

[DOI]

Antonio Ramos

J. Satisf. Boolean Model. Comput., 2011

Between Restarts and Backjumps.

[BibT_eX]

[DOI]

Antonio Ramos

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Efficient CNF Simplification Based on Binary Implication Graphs.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation.

[BibT_eX]

[DOI]

Oliver Gableske

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

2010

Symmetry within Solutions

[BibT_eX]

[DOI]

Toby Walsh

CoRR, 2010

Blocked Clause Elimination.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Covered Clause Elimination.

[BibT_eX]

[DOI]

Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

Clause Elimination Procedures for CNF Formulas.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Exact DFA Identification Using SAT Solvers.

[BibT_eX]

[DOI]

Sicco Verwer

Proceedings of the Grammatical Inference: Theoretical Results and Applications, 2010

Symmetry in Solutions.

[BibT_eX]

[DOI]

Toby Walsh

Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, 2010

2009

Look-Ahead Based SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Satisfiability, 2009

Dynamic Symmetry Breaking by Simulating Zykov Contraction.

[BibT_eX]

[DOI]

Bas Schaafsma

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

2008

SmArT solving: tools and techniques for satisfiability solvers.

[BibT_eX]

[DOI]

PhD thesis, 2008

Whose side are you on? Finding solutions in a biased search-tree.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2008

Parallel SAT Solving using Bit-level Operations.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2008

Sums of squares based approximation algorithms for MAX-SAT.

[BibT_eX]

[DOI]

Linda van Norden

Discret. Appl. Math., 2008

2007

Solving games: Dependence of applicable solving procedures.

[BibT_eX]

[DOI]

Léon J. M. Rothkrantz

Sci. Comput. Program., 2007

A New Method to Construct Lower Bounds for Van der Waerden Numbers.

[BibT_eX]

[DOI]

Electron. J. Comb., 2007

Prototypes for Automated Architectural 3D-Layout.

[BibT_eX]

[DOI]

Proceedings of the Virtual Systems and Multimedia, 13th International Conference, 2007

Effective Incorporation of Double Look-Ahead Procedures.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

From Idempotent Generalized Boolean Assignments to Multi-bit Search.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

2006

March_dl: Adding Adaptive Heuristics and a New Branching Strategy.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2006

2005

Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

2004

Aligning CNF- and Equivalence-reasoning.

[BibT_eX]

[DOI]