Theory and Applications of Satisfiability Testing - SAT 2013 [electronic resource] : 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings / edited by Matti Järvisalo, Allen Van Gelder.

Invited Talks -- The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-algebraic Proofs -- Turing's Computable Real Numbers and Why They Are Still Important Today -- There Are No CNF Problems -- Best Paper -- Soundness of Inprocessing in Clause Sharing SAT Solvers -- Technical Papers -- Propositional Proof Complexity I -- Exponential Separations in a Hierarchy of Clause Learning Proof Systems -- On the Resolution Complexity of Graph Non-isomorphism -- Quantified Boolean Formulas -- On Propositional QBF Expansions and Q-Resolution -- Recovering and Utilizing Partial Duality in QBF -- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation -- Parallel Solving -- Concurrent Clause Strengthening -- Parallel MUS Extraction -- Maximum Satisfiability -- A Modular Approach to MaxSAT Modulo Theories -- Exploiting the Power of mip Solvers in maxsat -- Community-Based Partitioning for MaxSAT Solving -- Encodings and Applications -- Experiments with Reduction Finding -- A Constraint Satisfaction Approach for Programmable Logic Detailed Placement -- Minimizing Models for Tseitin-Encoded SAT Instances -- Beyond SAT -- Solutions for Hard and Soft Constraints Using Optimized Probabilistic Satisfiability -- Quantified Maximum Satisfiability: A Core-Guided Approach -- Nested Boolean Functions as Models for Quantified Boolean Formulas -- Solver Techniques and Algorithms -- Factoring Out Assumptions to Speed Up MUS Extraction -- On the Interpolation between Product-Based Message Passing Heuristics for SAT -- Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction -- Clique-Width and SAT -- A SAT Approach to Clique-Width -- Cliquewidth and Knowledge Compilation -- Propositional Proof Complexity II -- A Rank Lower Bound for Cutting Planes Proofs of Ramsey's -- Theorem -- The Complexity of Theorem Proving in Autoepistemic Logic -- Parameterized Complexity -- Local Backbones -- Upper and Lower Bounds for Weak Backdoor Set Detection -- Tool Papers -- LearnSAT: A SAT Solver for Education -- MUStICCa: MUS Extraction with Interactive Choice of Candidates -- SCSat: A Soft Constraint Guided SAT Solver -- Snappy: A Simple Algorithm Portfolio -- Scarab: A Rapid Prototyping Tool for SAT-Based Constraint Programming Systems.