POS — PROGRAM
Days: Sunday, 19 July 2026
Sunday, 19 July 2026
08:45-09:00
Opening
PoS
Location:
C4.08
| 08:45-09:00 |
Opening (abstract) 15 min
1 KU Leuven
2 Karlsruhe Institute of Technology
|
09:00-10:30
Session 1: Proofs
PoS
Location:
C4.08
| 09:00-09:20 |
Proof-Guided SAT Encoding Selection for Bit-Vector Multiplication (abstract) 20 min
1 Amazon Web Services
2 City St George’s, University of London
|
| 09:20-09:40 |
Certified Variable Reordering in Cardinality Encodings (abstract) 20 min
1 Carnegie Mellon University
|
| 09:40-10:00 |
Trimming Pseudo-Boolean Proofs (abstract) 20 min
1 Vrije Universiteit Brussel
2 KU Leuven, Belgium
3 University of Copenhagen, Denmark
4 University of Basel, Switzerland
5 University of Glasgow, United Kingdom
6 Lund University, Sweden
7 Vienna University of Technology, Austria
|
| 10:00-10:20 |
PBLean: Pseudo-Boolean Proof Certificates for Lean 4 (abstract) 20 min
1 TIUWien
|
| 10:20-10:30 |
Scaling Zero Knowledge UNSAT Verification via Normalized Chaining (abstract) 10 min
1 University of Toronto
2 Independent
3 Georgia Institute of Technology, University of Toronto
|
10:30-11:00
Coffee Break
PoS
Location:
C4.08
11:00-11:50
Session 2: Optimization
PoS
Location:
C4.08
| 11:00-11:20 |
Revising the Implicit Hitting Set Solver MaxHS (abstract) 20 min
1 University of Freiburg
|
| 11:20-11:40 |
Aperture: an Anytime, Complete, and Incremental Solver for MaxSAT and Beyond (Work-in-Progress) (abstract) 20 min
1 Faculty of Data and Decision Sciences, Technion
|
| 11:40-11:50 |
Smallest MUS Extraction via Branch-and-Cut (abstract) 10 min
1 Delft University of Technology
|
11:50-12:20
Session 3: Enumeration & Counting
PoS
Location:
C4.08
| 11:50-12:10 |
Extending CDCL-based Model Enumeration with Weights (abstract) 20 min
1 Rice University
|
| 12:10-12:20 |
Formalization of Component-Based Projected Model Counting (abstract) 10 min
1 University of Yamanashi
2 Kagawa University
3 Nagoya University
|
12:20-14:00
Lunch
PoS
Location:
C4.08
14:00-15:10
Session 4: Exploring Solvers and Instances
PoS
Location:
C4.08
| 14:00-14:20 |
SAT-IT: an Online Interactive SAT Tracer (abstract) 20 min
1 Universitat de Girona
|
| 14:20-14:40 |
Exploring 3-CNF Formulas Generated From Partial Steiner Triple Systems (abstract) 20 min
1 Dakota State University
|
| 14:40-15:00 |
The Multi-Skill Project Scheduling Problem: To SAT, or to PB, that is the question. (abstract) 20 min
1 Universitat de Girona
|
| 15:00-15:10 |
Orthologic for SAT Solving (abstract) 10 min
1 EPFL
2 ENS Paris-Saclay
|
15:10-15:50
Coffee Break
PoS
Location:
C4.08
15:50-16:50
Session 5: SAT Solver Technology
PoS
Location:
C4.08
| 15:50-16:10 |
Improving Local Search and adding DDFW to Kissat and CaDiCaL (abstract) 20 min
1 University of Freiburg
|
| 16:10-16:30 |
NobleCount: Revisiting a Forgotten Data Structure for Local Search in SAT (abstract) 20 min
1 Faculty of Data and Decision Sciences, Technion
|
| 16:30-16:40 |
ams-dist: A Scalable Distributed Hybrid Solver for Hard Combinatorial Problems (abstract) 10 min
1 Georgia Institute of Technology
|
| 16:40-16:50 |
MIGSat: A Majority Inverter Graph SAT Solver (abstract) 10 min
1 Georgia Institute of Technology
|
16:50-17:00
Short Break
PoS
Location:
C4.08
17:00-17:50
Session 6: Encodings
PoS
Location:
C4.08
| 17:00-17:20 |
Reverse-Engineering Constraint Models from CNFs: An Agentic Approach (abstract) 20 min
1 Linköping University
2 TU Wien
|
| 17:20-17:40 |
Coloring Queens with Thousands of Encodings (abstract) 20 min
1 Carnegie Mellon University
|
| 17:40-17:50 |
Power Term Polynomial Algebra for Boolean Logic (abstract) 10 min
1 KU Leuven
2 MIT
|
17:50-18:00
Closing
PoS
Location:
C4.08
| 17:50-18:00 |
Closing Remarks (abstract) 10 min
1 KU Leuven
2 Karlsruhe Institute of Technology
|