SAT PROGRAM
Days: Monday, July 9th Tuesday, July 10th Wednesday, July 11th Thursday, July 12th
Monday, July 9th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 46: FLoC Plenary Lecture: Peter O'Hearn
Chair:
Location: Maths LT1
| 09:00 | Continuous Reasoning: Scaling the Impact of Formal Methods (abstract) |
10:30-11:00Coffee Break
11:00-12:15 Session 47F: SAT Invited Talk: Christoph Scholl
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 11:00 | Welcome to SAT 2018 (abstract) |
| 11:05 | Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 49F: MaxSAT
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 14:00 | Approximately Propagation Complete and Conflict Propagating Constraint Encodings (abstract) |
| 14:30 | Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (abstract) |
| 15:00 | Solving MaxSAT with Bit-Vector Optimization (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 51F: CDCL
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 16:00 | Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (abstract)  |
| 16:30 | Machine Learning-based Restart Policy for CDCL SAT Solvers (abstract) |
| 17:00 | Chronological Backtracking (abstract) |
| 17:30 | Centrality-Based Improvements to CDCL Heuristics (abstract) |
19:00-21:30 FLoC reception at Ashmolean Museum
FLoC reception at Ashmolean Museum. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Ashmolean Museum
Tuesday, July 10th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 52E: Model Counting
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 09:00 | Fast Sampling of Perfectly Uniform Satisfying Assignments (abstract) |
| 09:30 | Fast and Flexible Probabilistic Model Counting (abstract) |
| 10:00 | Exploiting Treewidth for Projected Model Counting and its Limits (abstract) |
10:30-11:00Coffee Break
11:00-12:00 Session 54F: SAT Invited Talk: Rahul Santhanam
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 11:00 | Modelling SAT (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 55F: QBF I
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 14:00 | Circuit-based Search Space Pruning in QBF (abstract) |
| 14:30 | Symmetries for QBF (abstract) |
| 15:00 | Local Soundness for QBF Calculi (abstract)  |
15:30-16:00Coffee Break
16:00-17:00 Session 58C: QBF II
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 16:00 | QBF as an Alternative to Courcelle's Theorem (abstract) |
| 16:30 | Polynomial-Time Validation of QCDCL Certificates (abstract) |
17:00-18:30 Session 59: FLoC Public Lecture: Stuart Russell
Doors open at 4:30 pm; please be seated by 4:50 pm (attendance is free of charge and all are welcome; please register).
Chair:
Location: Sheldonian Theatre
| 17:00 | Unifying Logic and Probability: the BLOG Language (abstract) |
Wednesday, July 11th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 60F: Theory
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 09:00 | Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT (abstract) |
| 09:30 | In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving (abstract) |
| 10:00 | Cops-Robber games and the resolution of Tseitin formulas (abstract) |
10:30-11:00Coffee Break
11:00-12:00 Session 64F: SAT Invited Talk: Marijn Heule
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 11:00 | Computable Short Proofs (abstract) |
12:00-12:20 Session 65B: Industry Presentation
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 12:00 | Satalia's SolveEngine (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 66A: FLoC Keynote Lecture: Shafi Goldwasser
Chair:
Location: Maths LT1
| 14:00 | Pseudo deterministic algorithms and proofs (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 67E: MUS
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 16:00 | Minimal unsatisfiability and minimal strongly connected digraphs (abstract) |
| 16:30 | Finding all Minimal Safe Inductive Sets (abstract) |
19:00-21:30 FLoC banquet at Examination Schools
FLoC banquet at Examination Schools. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Examination Schools
Thursday, July 12th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
10:30-11:00Coffee Break
11:00-12:00 Session 74E: SMT
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 11:00 | Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition (abstract) |
| 11:30 | Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization (abstract) |
12:00-12:30 Session 75B: Tools & Applications I
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 12:00 | XORSAT Set Membership Filters (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 76G: Tools & Applications II
Chair:
Location: Blavatnik Seminar Rooms 1 & 2
| 14:00 | ALIAS: A Modular Tool for Finding Backdoors for SAT (abstract) |
| 14:30 | PySAT: A Python Toolkit for Prototyping with SAT Oracles (abstract) |
| 15:00 | Constrained Image Generation Using Binarized Neural Networks with Decision Procedures (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 78D: Awards & Competitions
Chairs:
Location: Blavatnik Seminar Rooms 1 & 2
| 16:00 | Award Ceremony (abstract) |
| 16:05 | MaxSAT Evaluation 2018 (abstract) |
| 16:33 | QBFEVAL’18 (abstract) |
| 17:01 | Sparkle SAT Challenge 2018 (abstract) |
| 17:29 | SAT Competition 2018 (abstract) |