Theoretical Foundations of Applied SAT Solving

Videos from BIRS Workshop 14w5101

, University of Texas at Austin
- 09:59
Mini-tutorial on conflict-driven clause learning (CDCL)
Watch video | Download video: 201401200903-Heule.mp4 (121M)
, University of Helsinki
- 12:07
Mini-tutorial on preprocessing
Watch video | Download video: 201401201117-Jarvisalo.mp4 (123M)
, KTH Royal Institute of Technology
- 15:34
Mini-tutorial on weak proof systems and connections to SAT solving
Watch video | Download video: 201401201438-Nordstrom.mp4 (121M)
, Labri, Bordeaux Institute of Technology, France
- 16:33
Understanding the power of glue clauses
Watch video | Download video: 201401201602-Simon.mp4 (70M)
, Johannes Kepler University
- 17:24
Where does SAT not work?
Watch video | Download video: 201401201634-Biere.mp4 (115M)
, University of Michigan
- 20:18
Anatomy and Empirical Evaluation of Modern SAT Solvers
Watch video | Download video: 201401202003-Sakallah.mp4 (45M)
, KTH Royal Institute of Technology
- 21:10
Open Problem Session Discussion
Watch video | Download video: 201401202056-Lauria.mp4 (42M)
, University of Washington
- 21:20
Caching more than just bad partial assignments (clauses)?
Watch video | Download video: 201401202110-Beame.mp4 (47M)
, University of Utah
- 10:01
Leveraging Groebner bases and SAT for hardware/software verification
Watch video | Download video: 201401210905-Kalla.mp4 (106M)
, Universite d'Artois
- 10:59
Survey on integrating cutting planes in CDCL solvers
Watch video | Download video: 201401211002-LeBerre.mp4 (106M)
, Universitat Politecnica de Catalunya
- 12:06
Mini-tutorial on semialgebraic proof systems
Watch video | Download video: 201401211115-Atserias.mp4 (98M)
, University of Texas at Austin
- 16:34
Inprocessing rules
Watch video | Download video: 201401211601-Heule.mp4 (112M)
, IST/INESC-ID
- 10:01
Problem solving with SAT oracles
Watch video | Download video: 201401220903-Marques-Silva.mp4 (137M)
, Universitat Politecnica de Catalunya
- 11:04
Survey of satisfiability modulo theories (SMT)
Watch video | Download video: 201401221037-Oliveras.mp4 (54M)
, TU Dresden
- 11:53
Recent developments in parallel SAT solving
Watch video | Download video: 201401221121-Manthey.mp4 (73M)
, IBM Watson Research Center
- 12:22
Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers
Watch video | Download video: 201401221154-Sabharwal.mp4 (80M)
, Johannes Kepler University
- 09:56
Recent trends in QBF solving
Watch video | Download video: 201401230905-Seidl.mp4 (128M)
, University of Toronto
- 10:27
Reactive synthesis via QBF solving
Watch video | Download video: 201401230957-Narodytska.mp4 (68M)
, University of Oxford
- 10:58
Beating brute force search for QBF satisfiability
Watch video | Download video: 201401231028-Santhanam.mp4 (68M)
, Rice University
- 11:50
Phase transitions and computational complexity
Watch video | Download video: 201401231116-Vardi.mp4 (70M)
, US Department of Defense
- 12:16
Satisfiability-based set membership filters
Watch video | Download video: 201401231150-Weaver.mp4 (89M)
, University of Michigan
- 15:04
Saucy3: Fast Symmetry Discovery in Graphs
Watch video | Download video: 201401231433-Sakallah.mp4 (77M)
, University of Washington
- 15:32
Exact model counting: SAT-solver based methods versus lifted inference
Watch video | Download video: 201401231504-Beame.mp4 (76M)
, Università degli Studi di Roma La Sapienza
- 16:33
Space complexity in algebraic proof systems
Watch video | Download video: 201401231602-Galesi.mp4 (56M)
, KTH Royal Institute of Technology
- 17:02
Narrow proofs may be maximally long
Watch video | Download video: 201401231634-Lauria.mp4 (50M)
, LMU Munich
- 17:32
Lower bounds for width-restricted clause learning
Watch video | Download video: 201401231703-Johannsen.mp4 (68M)
, KTH Royal Institute of Technology
- 20:59
From theoretical potential to applied impact — could/should we get more interaction between practitioners and theoreticians and if so how?
Watch video | Download video: 201401231938-Nordstrom.mp4 (249M)
, Karlsruhe Institute of Technology
- 09:32
Abstraction and multi-encodings in SAT
Watch video | Download video: 201401240904-Sinz.mp4 (57M)
, Swansea University
- 10:02
Unit-clause propagation and monotone circuits
Watch video | Download video: 201401240932-Kullmann.mp4 (81M)
, Princeton University
- 10:33
Strong ETH holds for regular resolution
Watch video | Download video: 201401241007-Beck.mp4 (53M)
, University of Michigan
- 11:26
Detecting traditional packing, decisively
Watch video | Download video: 201401241103-Bueno.mp4 (43M)
, University of Waterloo
- 12:00
Timed PageRank and branching heuristics in CDCL SAT solvers
Watch video | Download video: 201401241129-Ganesh.mp4 (64M)