Theoretical Foundations of Applied SAT Solving
Videos from BIRS Workshop
Marijn Heule, University of Texas at Austin
Monday Jan 20, 2014 09:03 - 09:59
Mini-tutorial on conflict-driven clause learning (CDCL)
Matti Järvisalo, University of Helsinki
Monday Jan 20, 2014 11:17 - 12:07
Mini-tutorial on preprocessing
Jakob Nordström, University of Copenhagen
Monday Jan 20, 2014 14:38 - 15:34
Mini-tutorial on weak proof systems and connections to SAT solving
Laurent Simon, LaBRI / University of Bordeaux
Monday Jan 20, 2014 16:02 - 16:33
Understanding the power of glue clauses
Armin Biere, Johannes Kepler University
Monday Jan 20, 2014 16:34 - 17:24
Where does SAT not work?
Karem Sakallah, University of Michigan
Monday Jan 20, 2014 20:03 - 20:18
Anatomy and Empirical Evaluation of Modern SAT Solvers
Massimo Lauria, KTH Royal Institute of Technology
Monday Jan 20, 2014 20:56 - 21:10
Open Problem Session Discussion
Paul Beame, University of Washington
Monday Jan 20, 2014 21:10 - 21:20
Caching more than just bad partial assignments (clauses)?
Priyank Kalla, University of Utah
Tuesday Jan 21, 2014 09:05 - 10:01
Leveraging Groebner bases and SAT for hardware/software verification
Daniel Le Berre, Universite d'Artois
Tuesday Jan 21, 2014 10:02 - 10:59
Survey on integrating cutting planes in CDCL solvers
Albert Atserias, Universitat Politecnica de Catalunya
Tuesday Jan 21, 2014 11:15 - 12:06
Mini-tutorial on semialgebraic proof systems
Marijn Heule, University of Texas at Austin
Tuesday Jan 21, 2014 16:01 - 16:34
Inprocessing rules
Joao Marques-Silva, LASIGE, Faculty of Sciences, University of Lisbon
Wednesday Jan 22, 2014 09:03 - 10:01
Problem solving with SAT oracles
Albert Oliveras, Universitat Politecnica de Catalunya
Wednesday Jan 22, 2014 10:37 - 11:04
Survey of satisfiability modulo theories (SMT)
Norbert Manthey, TU Dresden
Wednesday Jan 22, 2014 11:21 - 11:53
Recent developments in parallel SAT solving
Ashish Sabharwal, IBM Watson Research Center
Wednesday Jan 22, 2014 11:54 - 12:22
Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers
Martina Seidl, Johannes Kepler University
Thursday Jan 23, 2014 09:05 - 09:56
Recent trends in QBF solving
Nina Narodytska, University of Toronto
Thursday Jan 23, 2014 09:57 - 10:27
Reactive synthesis via QBF solving
Rahul Santhanam, University of Oxford
Thursday Jan 23, 2014 10:28 - 10:58
Beating brute force search for QBF satisfiability
Moshe Vardi, Rice University
Thursday Jan 23, 2014 11:16 - 11:50
Phase transitions and computational complexity
Sean Weaver, US Department of Defense
Thursday Jan 23, 2014 11:50 - 12:16
Satisfiability-based set membership filters
Karem Sakallah, University of Michigan
Thursday Jan 23, 2014 14:33 - 15:04
Saucy3: Fast Symmetry Discovery in Graphs
Paul Beame, University of Washington
Thursday Jan 23, 2014 15:04 - 15:32
Exact model counting: SAT-solver based methods versus lifted inference
Nicola Galesi, Università degli Studi di Roma La Sapienza
Thursday Jan 23, 2014 16:02 - 16:33
Space complexity in algebraic proof systems
Massimo Lauria, KTH Royal Institute of Technology
Thursday Jan 23, 2014 16:34 - 17:02
Narrow proofs may be maximally long
Jan Johannsen, LMU Munich
Thursday Jan 23, 2014 17:03 - 17:32
Lower bounds for width-restricted clause learning
Jakob Nordström, University of Copenhagen
Thursday Jan 23, 2014 19:38 - 20:59
From theoretical potential to applied impact — could/should we get more interaction between practitioners and theoreticians and if so how?
Carsten Sinz, Karlsruhe Institute of Technology
Friday Jan 24, 2014 09:04 - 09:32
Abstraction and multi-encodings in SAT
Oliver Kullmann, Swansea University
Friday Jan 24, 2014 09:32 - 10:02
Unit-clause propagation and monotone circuits
Chris Beck, Princeton University
Friday Jan 24, 2014 10:07 - 10:33
Strong ETH holds for regular resolution
Denis Bueno, University of Michigan
Friday Jan 24, 2014 11:03 - 11:26
Detecting traditional packing, decisively
Vijay Ganesh, University of Waterloo
Friday Jan 24, 2014 11:29 - 12:00
Timed PageRank and branching heuristics in CDCL SAT solvers
