Awards

Distinguished Service Award

2025

The SAT Association conferred a Distinguished Service Award on Hans Kleine Büning in honour of his long-lasting and foundational contributions to the series of International Conferences on Theory and Applications of Satisfiability Testing (SAT) and the SAT Association.

2023

The SAT Association conferred a Distinguished Service Award on John Franco in honour of his long-lasting and foundational contributions to the series of International Conferences on Theory and Applications of Satisfiability Testing (SAT), the SAT association, and the Journal on Satisfiability, Boolean Modeling and Computation (JSAT).

Fahiem Bacchus Ph.D. Award in Satisfiability

2025

Winner: “Hybrid Algorithms for SAT and SMT and Their Applications” by Xindi Zhang, University of the Chinese Academy of Sciences

2024

Winner: “Scalable SAT Solving and its Applications”, by Dominik Schreiber from Karlsruhe Institute of Technology

Runner-up: “Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning”, by Stephan Gocht from Lund University

Runner-up: “Scalability for SAT-based Combinatorial Problem Solving” (Ph.D. thesis), by André Schidler from Technische Universität Wien

Best Paper Award

• 2025: “Streamlining Distributed SAT Solver Design”, by Dominik Schreiber, Niccolò Rigi-Luperti and Armin Biere

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2025.27

• 2024: “The Strength of the Dominance Rule”, by Leszek Aleksander Kołodziejczyk and Neil Thapen

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2024.20

• 2023: no best paper award, but three highlighted papers:

  • “Polynomial Calculus for MaxSAT”, by Ilario Bonacina, María-Luisa Bonet and Jordi Levy

    DOI: https://doi.org/10.4230/LIPIcs.SAT.2023.5

  • “Certified Knowledge Compilation with Application to Verified Model Counting”, by Randal Bryant, Wojciech Nawrocki, Jeremy Avigad and Marijn Heule

    DOI: https://doi.org/10.4230/LIPIcs.SAT.2023.6

  • “IPASIR-UP: User Propagators for CDCL”, by Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere

    DOI: https://doi.org/10.4230/LIPIcs.SAT.2023.8

• 2022: “A generalization of the Satisfiability Coding Lemma and its applications”, by Milan Mosse, Harry Sha and Li-Yang Tan

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2022.9

• 2022: “Certified CNF Translations for Pseudo-Boolean Solving”, by Stephan Gocht, Ruben Martins, Jakob Nordström and Andy Oertel

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2022.16

• 2021: “Deep Cooperation of CDCL and Local Search for SAT”, by Shaowei Cai and Xindi Zhang

  DOI: https://doi.org/10.1007/978-3-030-80223-3_6

• 2020: “Abstract Cores in Implicit Hitting Set MaxSat Solving”, by Jeremias Berg, Fahiem Bacchus and Alex Poole

  DOI: https://doi.org/10.1007/978-3-030-51825-7_20

• 2019: “On Super Strong ETH”, by Nikhil Vyas and Ryan Williams

  DOI: https://doi.org/10.1007/978-3-030-24258-9_28

• 2018: “Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT”, by Tobias Friedrich and Ralf Rothenberger

  DOI: https://doi.org/10.1007/978-3-319-94144-8_17

• 2017: “Shortening QBF Proofs with Dependency Schemes“, by Joshua Blinkhorn and Olaf Beyersdorff

  DOI: https://doi.org/10.1007/978-3-319-66263-3_17

• 2016: “Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer“, by Marijn Heule, Oliver Kullmann and Victor Marek

  DOI: https://doi.org/10.1007/978-3-319-40970-2_15

• 2013: “Soundness of Inprocessing in Clause Sharing SAT Solvers“, by Norbert Manthey, Tobias Philipp, and Christoph Wernhard

  DOI: https://doi.org/10.1007/978-3-642-39071-5_4

• 2011: “On Freezing and Reactivating Learnt Clauses“, by Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure and Lakhdar Sais

  DOI: https://doi.org/10.1007/978-3-642-21581-0_16

  additional candidates:

  • 2011: “Parameterized Complexity of DPLL Search Procedures“, by Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria

    DOI: https://doi.org/10.1007/978-3-642-21581-0_3

  • 2011: “Satisfiability Certificates Verifiable in Subexponential Time“, by Evgeny Dantsin and Edward A. Hirsch

    DOI: https://doi.org/10.1007/978-3-642-21581-0_4

Best Student Paper Award

• 2025: “Enumerating All Boolean Matches”, by Alexander Nadel and Yogev Shalmon

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2025.22

• 2024: “Speeding-up Pseudo-Boolean Propagation”, by Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez Carbonell and Rui Zhao

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2024.22

• 2023: “QCDCL vs QBF Resolution: Further Insights”, by Benjamin Böhm and Olaf Beyersdorff

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2023.4

• 2022: “SAT Preprocessors and Symmetry”, by Markus Anders

  DOI: https://doi.org/10.4230/LIPIcs.SAT.2022.1

• 2021: “Characterizing Tseitin-Formulas with Short Regular Resolution Refutations”, by Alexis de Colnet and Stefan Mengel

  DOI: https://doi.org/10.1007/978-3-030-80223-3_9

• 2020: “Mycielski graphs and PR proofs“, by Emre Yolcu, Xinyu Wu, and Marijn J. H. Heule

  DOI: https://doi.org/10.1007/978-3-030-51825-7_15

• 2019: “Incremental Inprocessing in SAT Solving”, by Katalin Fazekas, Armin Biere, and Christoph Scholl

  DOI: https://doi.org/10.1007/978-3-030-24258-9_9

• 2018: “Fast Sampling of Perfectly Uniform Satisfying Assignments”, by Dimitris Achlioptas, Zayd Hammoudeh, and Panos Theodoropoulos

  DOI: https://doi.org/10.1007/978-3-319-94144-8_9

• 2017: “Introducing Pareto Minimal Correction Subsets“, by Miguel Terra-Neves, Inês Lynce, and Vasco Manquinho

  DOI: https://doi.org/10.1007/978-3-319-66263-3_13

  Best Student Paper Honourable Mention

  • “An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate“, by Jia Liang, Vijay Ganesh, Krzysztof Czarnecki, Pascal Poupart, and Hari Govind V K

    DOI: https://doi.org/10.1007/978-3-319-66263-3_8

• 2016: “A SAT Approach to Branchwidth“, by Neha Lodha, Sebastian Ordyniak and Stefan Szeider

  DOI: https://doi.org/10.1007/978-3-319-40970-2_12

• 2014: “Impact of Community Structure on SAT Solver Performance“, by Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard and Laurent Simon

  DOI: https://doi.org/10.1007/978-3-319-09284-3_20

Test-of-Time Award

The Test-of-Time Award is given by the SAT Association for the most influential paper published in the SAT Conference 20 ± 1 years ago.

2025

“Effective Preprocessing in SAT Through Variable and Clause Elimination” by Niklas Eén and Armin Biere, presented at SAT 2005

DOI: https://doi.org/10.1007/11499107_5

2024

“Combining Component Caching and Clause Learning for Effective Model Counting” by Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi, presented at SAT 2004

2023

“Resolve and Expand” by Armin Biere, presented at SAT 2004

DOI: https://doi.org/10.1007/11527695_5

2022

“An Extensible SAT-solver”, by Niklas Eén and Niklas Sörensson, presented at SAT 2003

DOI: https://doi.org/10.1007/978-3-540-24605-3_37