SAT — PROGRAM

Days: Monday, 20 July 2026 Tuesday, 21 July 2026 Wednesday, 22 July 2026 Thursday, 23 July 2026

Monday, 20 July 2026
10:00-10:30 Coffee Break SAT
Location: JJ Laginha
10:30-12:00 Session A: Encodings & Preprocessing SAT
Location: JJ Laginha
10:30-11:00
Backtrackable Inprocessing (abstract) 30 min
Alexander Nadel1
1 Technion, NVIDIA
11:00-11:30
Near-Optimal Encodings of Cardinality Constraints (abstract) 30 min
Andrew Krapivin1, Benjamin Przybocki1, Bernardo Subercaseaux1
1 Carnegie Mellon University
11:30-12:00
Automated Reencoding Meets Graph Theory (abstract) 30 min
Benjamin Przybocki1, Bernardo Subercaseaux1, Marijn Heule1
1 Carnegie Mellon University
12:00-13:30 Lunch SAT
Location: JJ Laginha
13:30-15:30 Session B: Proof Systems & Complexity SAT
Location: JJ Laginha
13:30-14:00
Factoring Learned Clauses (abstract) 30 min
Florian Pollitt1, Zachary Battleman2, Mathias Fleury1, Yakir Vizel3, Marijn Heule2, Armin Biere1, Randal E. Bryant2
1 University Freiburg
2 Carnegie Mellon University
3 Israel Institute of Technology
14:00-14:30
An Exponential Separation between Deterministic CDCL and DPLL Solvers (abstract) 30 min
Sahil Samar1, Marc Vinyals2, Vijay Ganesh1
1 Georgia Institute of Technology
2 University of Auckland
14:30-15:00
Conditional Autarkies: Hard Formulas Made Easy (abstract) 30 min
Ilario Bonacina1, Maria Luisa Bonet1, Antonina Kolokolova2, Massimo Lauria3
1 UPC Universitat Politècnica de Catalunya
2 Memorial University of Newfoundland
3 Sapienza - Università di Roma
15:00-15:30
Proof Systems Based on Structured Circuits (abstract) 30 min
Matthäus Micun1, Christoph Berkholz1
1 Technical University Ilmenau
15:30-16:00 Coffee Break SAT
Location: JJ Laginha
16:00-17:15 Session C: Solver Tools & Explanations SAT
Location: JJ Laginha
16:00-16:15
WhyUnsat: a practical explanation tool (abstract) 15 min
Robert Nieuwenhuis1, Albert Oliveras1, Enric Rodríguez Carbonell1
1 Technical University Catalonia (BarcelonaTech)
16:15-16:30
Shapley-Shubik Attribution from Minimal Subsets (abstract) 15 min
Pablo Martínez-Naredo1, Raúl Mencía1, Joao Marques-Silva2, Carlos Mencía1
1 University of Oviedo
2 ICREA & University of Lleida
16:30-16:45
Unified Programmatic Access to CO Benchmarks, to Connect Constraint Solving Communities (abstract) 15 min
Thomas Sergeys1, Tias Guns1, Ignace Bleukx1
1 KU Leuven
16:45-17:00
Sustainable Benchmarking Tool (abstract) 15 min
Ashlin Iser1, Marie Anastacio2, Théo Matricon3, Laurent Simon4, Holger H. Hoos2
1 Karlsruhe Institute of Technology
2 RWTH Aachen University
3 Rennes University
4 Bordeaux University
17:00-17:15
decdnnf_rs: A framework for Querying d-DNNF (abstract) 15 min
Jean-Marie Lagniez1, Emmanuel Lonca1
1 CRIL
Tuesday, 21 July 2026
09:00-10:00 Invited Talk 1 SAT
Location: JJ Laginha
10:00-10:30 Coffee Break SAT
Location: JJ Laginha
10:30-12:00 Session D: MaxSAT & PB Optimization SAT
Location: JJ Laginha
10:30-11:00
Beyond Core-Guided MaxSAT (abstract) 30 min
Ilario Bonacina1, Jordi Levy2, Ion Mikel Liberal2
1 UPC
2 IIIA-CSIC
11:00-11:15
Scuttle: A System for Multi-Objective MaxSAT (abstract) 15 min
Christoph Jabs1, Jeremias Berg1, Matti Järvisalo1
1 University of Helsinki
11:15-11:30
Hermax: A Unified MaxSAT library (abstract) 15 min
Josep Maria Salvia Hornos1, Cèsar Fernández Camón1, Carles Mateu Piñol1
1 University of Lleida
11:30-11:45
HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization (abstract) 15 min
Hannes Ihalainen1, Dieter Vandesande2, Andre Schidler3, Jeremias Berg1, Matti Järvisalo1
1 University of Helsinki
2 Vrije Universiteit Brussel, KU Leuven
3 University of Freiburg
11:45-12:00
NLIPSat: Satisfiability-based Nonlinear Integer Programing Encoding Toolkit (abstract) 15 min
Zhengling Yangli1, Zhifei Zheng2, Sami Cherif3, Rui Sá Shibasaki3, Chu-Min Li3
1 Yunnan University
2 Gaoling School of AI, Renmin University of China
3 Laboratoire MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
12:00-13:30 Lunch SAT
Location: JJ Laginha
13:30-14:30 Session E1: Best Papers SAT
Location: JJ Laginha
13:30-14:00
Simplify, Order, Break, Repeat (abstract) 30 min
Markus Anders1, Cayden Codel2, Marijn J. H. Heule2
1 RPTU Kaiserslautern-Landau
2 Carnegie Mellon University
14:00-14:30
New Algorithms for Parity-SAT and Its Bounded-Occurrence Versions (abstract) 30 min
Sanjay Jain1, Junqiang Peng2, Frank Stephan3,1, Haoyun Tang1, Mingyu Xiao2
1 School of Computing, National University of Singapore, Singapore
2 University of Electronic Science and Technology of China, China
3 Department of Mathematics, National University of Singapore, Singapore
14:30-15:30 Session E2: Knowledge Compilation SAT
Location: JJ Laginha
14:30-15:00
The Compilability Thresholds of 2-CNF to OBDD (abstract) 30 min
Alexis de Colnet1, Alfons Laarman1, Joon Hyung Lee1
1 Leiden University
15:00-15:30
A canonical generalization of OBDD (abstract) 30 min
Florent Capelli1, YooJung Choi2, Stefan Mengel3, Martin Munoz3, Guy Van den Broeck4
1 Université d'Artois, CRIL
2 Arizona State University
3 CNRS, CRIL
4 University of California
15:30-16:00 Coffee Break SAT
Location: JJ Laginha
16:00-18:00 Session F: CDCL & Parallel Solving SAT
Location: JJ Laginha
16:00-16:30
PASSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving (abstract) 30 min
Mingming Jin1, Zhijie Kuang1, Jiongzhi Zheng2, Kun Mao2, Kun He1
1 Huazhong University of Science and Technology
2 Huawei OptVerse Solver,China
16:30-17:00
Generalizing CDCL with Graph Backtracking (abstract) 30 min
Robin Coutelier1, Thomas Hader1, Laura Kovács1
1 TU Wien
17:00-17:30
A Natively Parallel Proof Framework for Clause-Sharing SAT Solving (abstract) 30 min
Ruben Götz1, Michael Dörr1, Dominik Schreiber1
1 Karlsruhe Institute of Technology (KIT)
17:30-17:45
CaDiCaL 3.0 (abstract) 15 min
Florian Pollitt1, Mathias Fleury1, Katalin Fazekas2, Nils Froleyks3, André Schidler1, Dominik Schreiber4, Armin Biere1
1 University of Freiburg
2 Vienna University of Technology
3 KU Leuven
4 Karlsruhe Institute of Technology
17:45-18:00
Efficient Identification of Isomorphic SAT Instances (abstract) 15 min
Frederick Gehm1, Ashlin Iser1
1 KIT
18:00-19:00 Session M: SAT Association Awards SAT
Location: JJ Laginha
Wednesday, 22 July 2026
10:00-10:30 Coffee Break SAT
Location: JJ Laginha
10:30-12:00 Session G: QBF Algorithms SAT
Location: JJ Laginha
10:30-11:00
Bilateral Treewidth for QBF: Where Strategies and Resolution Meet (abstract) 30 min
Robert Ganian1, Marlene Gründel1
1 TU Wien
11:00-11:30
CAQE: Strong as Solver, Weak as Proof System (abstract) 30 min
Benjamin Böhm1, Olaf Beyersdorff1
1 Friedrich Schiller University Jena
11:30-12:00
d-QBF with Few Existential Variables Revisited (abstract) 30 min
Andreas Grigorjew1, Michael Lampis1
1 LAMSADE, Université Paris Dauphine-PSL
12:00-13:30 Lunch SAT
Location: JJ Laginha
13:30-15:30 Session H: QBF Proofs & Dependencies SAT
Location: JJ Laginha
13:30-14:00
Definition-based dependency schemes (abstract) 30 min
David Kattermann1, Martina Seidl1, Clemens Hofstadler1
1 Johannes Kepler University Linz
14:00-14:30
Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking (abstract) 30 min
Leroy Chew1, Tomáš Peitl2
1 Czech Institute of Informatics Robotics and Cybernetics
2 TU Wien
14:30-15:00
Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions (abstract) 30 min
S. Akshay1, Olaf Beyersdorff2, Supratik Chakraborty1, Lea Kasche2, Meena Mahajan3, Luc Nicolas Spachmann2
1 IIT Bombay
2 Friedrich Schiller University Jena
3 IMSc Chennai
15:00-15:15
On Proof Systems for #QBF (abstract) 15 min
Sravanthi Chede1, Leroy Chew2, Vaibhav Krishan1, Anil Shukla3
1 Institute of Mathematical Sciences Chennai
2 Czech Technical University in Prague, Czech Republic
3 Indian Institute of Technology Ropar
15:15-15:30
Long-Distance Q(D^{std})Consensus is sound (abstract) 15 min
Abhimanyu Choudhury1, Meena Mahajan1, Friedrich Slivovsky2
1 Institute of Mathematical Sciences, HBNI, Chennai
2 University of Liverpool, UK
15:30-16:00 Coffee Break SAT
Location: JJ Laginha
16:00-18:00 Session I: Beyond Propositional SAT SAT
Location: JJ Laginha
16:00-16:30
On Knowledge Compilation For Two-Variable First-Order Logic (abstract) 30 min
Qiaolan Meng1, Juhua Pu1, Hongting Niu1, Yuyi Wang2, Yuanhong Wang3, Ondřej Kuželka4
1 Beihang University
2 CRRC Zhuzhou Insitute
3 Jilin University
4 Czech Technical University in Prague
16:30-17:00
SAT Modulo Well-Founded Semantics (abstract) 30 min
Thomas Eiter1, Tobias Nießen1, Davide Soldà1
1 TU Wien
17:00-17:30
Dsat: A Native SAT Solver for Discrete Logic (abstract) 30 min
Yaofang Zhang1, Ken Zhou1, Adnan Darwiche1
1 University of California, Los Angeles
17:30-18:00
Extending CDCL to disjunctions of parity equations (abstract) 30 min
Paul Beame1, Glenn Sun1
1 University of Washington
Thursday, 23 July 2026
09:00-10:00 Invited Talk 2 SAT
Location: JJ Laginha
10:00-10:30 Coffee Break SAT
Location: JJ Laginha
10:30-12:00 Session J: SMT & Theory Reasoning SAT
Location: JJ Laginha
10:30-11:00
Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition (abstract) 30 min
Jung-Cheng Lin1, Chia-Hsuan Su1, Jie-Hong R. Jiang1, Hiroshi Unno2
1 National Taiwan University
2 Tohoku University
11:00-11:30
d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries (abstract) 30 min
Gabriele Masina1, Emanuele Civini1, Massimo Michelutti, Giuseppe Spallitta2, Roberto Sebastiani1
1 University of Trento
2 Rice University
11:30-12:00
SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology (abstract) 30 min
Ondřej Huvar1, Martin Jonáš1, Samuel Pastva1
1 Masaryk University
12:00-13:30 Lunch SAT
Location: JJ Laginha
13:30-15:30 Session K SAT
Location: JJ Laginha
15:30-16:00 Coffee Break SAT
Location: JJ Laginha
16:00-18:00 Session L SAT
Location: JJ Laginha
Designed and Developed by EventKey | Copyright 2026 EventKey Last updated:
🔍 ↑