Intro
Preface
Organization
Contents
OptiLog: A Framework for SAT-based Systems
1 Introduction
2 OptiLog Framework Architecture
2.1 Formula Module
2.2 SAT Solver Module
2.3 PB Encoder Module
2.4 Automatic Configuration (AC) Module
2.5 Adding SAT Solvers to OptiLog Through iSAT Interface
3 Example: The Linear MaxSAT Algorithm with OptiLog
4 Conclusions and Future Work
References
PyDGGA: Distributed GGA for Automatic Configuration
1 Introduction
2 Preliminaries
3 PyDGGA
3.1 Distributed Architecture
3.2 Simulation

3.3 Scheduling and Canceling
3.4 Instance Selection
3.5 Elite Mini-Tournament
3.6 Other Tool Enhancements
4 Using PyDGGA
5 Experiments with SAT
6 Conclusions and Future Work
References
QBFFam: A Tool for Generating QBF Families from Proof Complexity
1 Introduction
2 Related Work
3 Formula Families
4 Case Study
5 Conclusion
References
Davis and Putnam Meet Henkin: Solving DQBF with Resolution
1 Introduction
2 Preliminaries
3 Davis-Putnam Resolution for H-Form DQBF
3.1 Strategy Operations
3.2 Definition of the Construction

3.3 Correctness and Completeness
3.4 Representing Strategies
4 NEXP-completeness of CNF H-Form DQBF
5 Conclusion
References
Lower Bounds for QCDCL via Formula Gauge
1 Introduction
2 Preliminaries
3 QCDCL as a Formal Proof System
4 Quasi Level-Ordered Proofs
5 A Lower Bound Technique via Gauge
6 Applications of the Lower Bound Technique
7 Conclusion
References
Deep Cooperation of CDCL and Local Search for SAT
1 Introduction
2 Preliminaries
2.1 Preliminary Definitions and Notations
2.2 CDCL Solvers
2.3 Local Search Solvers

2.4 Experiment Preliminaries
3 Exploring Promising Branches by Local Search
4 Phase Resetting with Local Search Assignments
5 Branching with Conflict Frequency in Local Search
6 Experiments
7 Related Works
8 Conclusions
References
Hash-Based Preprocessing and Inprocessing Techniques in SAT Solvers
1 Introduction
2 Preliminaries
3 Hash-Based Methods
4 Probabilistic Analysis
5 Evaluation
6 Conclusions
References
Hardness and Optimality in QBF Proof Systems Modulo NP
1 Introduction
1.1 Organisation
2 Preliminaries
2.1 Proof Complexity

2.2 Propositional Logic
2.3 Quantified Boolean Formulas
3 Simulations with Extension Variables
4 Extended Q-Res Modulo NP
5 Weaker QBF Systems
6 Conclusion
References
Characterizing Tseitin-Formulas with Short Regular Resolution Refutations
1 Introduction
2 Preliminaries
3 Reduction from Unsatisfiable to Satisfiable Formulas
3.1 Well-Structured Branching Programs for SearchVertex(G, c)
3.2 Constructing DNNF from Well-Structured Branching Programs
4 Adversarial Rectangle Bounds
5 Splitting Parity Constraints