PoS 2026
Pragmatics of SAT 2026

Table of Contents

• Preface
  Summary: PoS 2026 received a total of 24 submissions, thereof 15 original papers (to be considered for the proceedings) and 9 presentation-only submissions. Ten submissions were accepted for inclusion in the proceedings; for one of them, the authors opted out of submitting a proceedings version. As such, 9 papers are included in this volume. In terms of presentations, we decided to admit seven short presentations in addition to four full presentations.

• Extending CDCL-Based Model Enumeration with Weights 1 - 18
  Giuseppe Spallitta , Moshe Vardi
• Revising the Implicit Hitting Set Solver MaxHS 19 - 29
  Edgar Justus , Jakob Berg , André Schidler , Mathias Fleury , Tobias Paxian , Armin Biere
• SAT-IT: An Online Interactive SAT Tracer 30 - 44
  Wilber Bermeo , Jordi Coll , Pau Ferrer , Mateu Villaret
• The Multi-Skill Project Scheduling Problem: To SAT, or to PB, That is the Question 45 - 57
  Wilber Bermeo , Jordi Coll , Mateu Villaret
• Improving Local Search and Adding DDFW to CaDiCaL 58 - 70
  Florian Pollitt , Mathias Fleury , André Schidler , Armin Biere , Johannes Gröber , Jakob Peterson , Rico Andris , Lea Hohl
• Proof-Guided SAT Encoding Selection for Bit-Vector Multiplication 71 - 88
  Armin Biere , Martin Brain , Daniel Kroening , Norbert Manthey , Michael Tautschnig
• PBLean: Pseudo-Boolean Proof Certificates for Lean 4 89 - 98
  Stefan Szeider
• Reverse-Engineering Constraint Models from CNFs: An Agentic Approach 99 - 109
  Johannes K. Fichte , Stefan Szeider
• Certified Variable Reordering in Cardinality Encodings 110 - 119
  Joseph E. Reeves , Marijn J. H. Heule , Randal E. Bryant