• Click on the titles of individual talks for abstract, slides and archived video. All talks listed in Pacific Time.

–
Coffee & Check In
–
Opening Remarks
–
Proofs, Circuits, and Total Search Problems
Susanna de Rezende (Czech Academy of Sciences)
–
On Proof Complexity of Resolution Over Polynomial Calculus
Erfan Khaniki (Charles University)
–
Break
–
Separations in Proof Complexity and TFNP
Robert Robere (McGill University)
–
Lunch
–
Functional Synthesis: An Ideal Meeting Ground for Formal Methods and Machine Learning
Kuldeep Singh Meel (National University of Singapore)
–
Break
–
Towards Characterizing Efficient Boolean Functional Synthesis
Supratik Chakraborty (IIT Bombay)
–
Program Synthesis as Dependency Quantified Formula Modulo Theory
Priyanka Golia (National University of Singapore)
–
Reception
–
Coffee & Check In
–
TBD
Antonina Kolokolova (Memorial University of Newfoundland)
–
On Quantitative Testing of Samplers
Mate Soos (National University of Singapore)
–
Break
–
Proof Logging for Combinatorial Optimization Using Pseudo-Boolean Reasoning
Jakob Nordström (University of Copenhagen & Lund University)
–
Lunch
–
Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
Stephan Gocht (Lund University)
–
Break
–
Bringing Proof Logging to Things That Aren't SAT
Ciaran McCreesh (University of Glasgow)
–
Solving SAT Translating It To Max2XOR
Jordi Levy (Artificial Intelligence Research Institute, Spanish National Resear…
–
Coffee & Check In
–
Consistent Query Answering via SAT Solving
Phokion Kolaitis (UC Santa Cruz and IBM Research)
–
Searching for Kochen–Specker Systems with Satisfiability Solving and Orderly Generation
Curtis Bright (University of Windsor)
–
Break
–
MAJORITY kSAT is in P
Ryan Williams (Massachusetts Institute of Technology)
–
Lunch
–
On CDCL vs. Resolution in QBF
Olaf Beyersdorff (Friedrich-Schiller University of Jena)
–
Break
–
SAT-Powered Heuristics for Very Large Instances
André Schidler (TU Wien)
–
MaxSat Resolution and SubCube Sums.
Meena Mahajan (Institute of Mathematical Sciences)
–
Coffee & Check In
–
CDCL Versus Resolution
Marc Vinyals (Saint Petersburg State University)
–
A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion
Dmitry Sokolov (Steklov Institute of Mathematics, Russia)
–
Break
–
What Are We Trying to Optimize by Restarting (A Real - And Fun - Experimental Set Up)
Laurent Simon (Bordeaux INP)
–
Lunch
–
Extremely Deep Proofs
Noah Fleming (University of Toronto)
–
Break
–
Towards Algebraic Methods in Descriptive Complexity
Evgenia Ternovska (Simon Fraser University)