SAT 2015: 18TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
SAT 2015 PROGRAM

Days: Thursday, September 24th Friday, September 25th Saturday, September 26th Sunday, September 27th

Thursday, September 24th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:00 Session 21: Invited Talk

   

09:00
Pragmatic Approach to Formal Verification ( abstract )
10:00-10:15Coffee Break
10:15-12:15 Session 22: Parallel SAT and #SAT Solving
10:15
Projected Model Counting ( abstract )
10:45
Search-Space Partitioning for Parallelizing SMT Solvers ( abstract )
11:15
HordeSat: A Massively Parallel Portfolio SAT Solver ( abstract )
11:45
Laissez-Faire Caching for Parallel #SAT Solving ( abstract )
12:15-13:45Lunch Break
13:45-15:15 Session 23: CDCL Solving
13:45
Hints Revealed ( abstract )
14:15
Between SAT and UNSAT: The Fundamental Difference in CDCL SAT ( abstract )
14:45
Evaluating CDCL Variable Scoring Schemes ( abstract )
15:15-15:30Coffee Break
15:30-16:15 Session 24: Competitions and Evaluations
15:30
SAT Race 2015 ( abstract )
15:45
Pseudo-Boolean Evaluation 2015 ( abstract )
16:00
Max-SAT Evaluation 2015 ( abstract )
Friday, September 25th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:00 Session 25: Invited Talk
09:00
Applying Satisfiability to the Analysis of Cryptography ( abstract )
10:00-10:15Coffee Break
10:30-12:00 Session 26: Structure
10:30
Using Community Structure to Detect Relevant Learnt Clauses ( abstract )
11:00
Community Structure Inspired Algorithms for SAT and #SAT ( abstract )
11:30
Recognition of Nested Gates in CNF Formulas ( abstract )
12:00-13:30Lunch Break
13:30-14:40 Session 27: Tool Presentations
13:30
SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers ( abstract )
13:40
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ( abstract )
13:50
SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers ( abstract )
14:00
PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF ( abstract )
14:10
CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability ( abstract )
14:20
Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances ( abstract )
14:30
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ( abstract )
14:40-15:30Tool Demonstrations and Coffee Break
15:30-17:00 Session 28: MaxSAT and Maximal Autarkies
15:30
Exploiting Resolution-based Representations for MaxSAT Solving ( abstract )
16:00
Computing maximal autarkies with few and simple oracle queries ( abstract )
16:30
Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP ( abstract )
Saturday, September 26th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:30 Session 30: Invited Talk
09:00
Random Formulas are Irrelevant, Right? ( abstract )
10:00
Constructing SAT filters with a quantum annealer ( abstract )
10:30-10:45Coffee Break
10:45-12:00 Session 31: Reformulation
10:45
On Compiling CNFs into Structured Deterministic DNNFs ( abstract )
11:15
Mining Implied Literals for Incremental SAT ( abstract )
11:45
SAT-Based Formula Simplification ( abstract )
12:00-13:30Lunch Break
13:30-15:15 Session 32: Minimal Unsatisfiable Cores
13:30
A New Approach to Partial MUS Enumeration ( abstract )
14:00
Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing ( abstract )
14:30
Speeding up MUS Extraction with Preprocessing and Chunking ( abstract )
15:00
SAT-Based Horn Least Upper Bounds ( abstract )
15:15-15:30Coffee Break
15:30-16:30 Session 33: Quantified Boolean Formulas
Chair:
15:30
QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving ( abstract )
16:00
Preprocessing for DQBF ( abstract )
Sunday, September 27th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

10:15-10:30Coffee Break
10:30-11:45 Session 35: Tutorial by Priyank Kalla (joint with FMCAD15)
10:30
Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation ( abstract )
11:45-13:45Lunch Break
15:15-15:45Coffee Break
15:45-17:15 Session 37: Tutorial by Isil Dillig (joint with FMCAD15)
15:45
Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis ( abstract )