TY - BOOK AU - Järvisalo,Matti AU - Van Gelder,Allen TI - Theory and Applications of Satisfiability Testing - SAT 2013: 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings SN - 9783642390715 PY - 2013/// CY - Berlin, Heidelberg PB - Springer Berlin Heidelberg KW - Computer science KW - Computers KW - Algorithms KW - Computer logic KW - Mathematical logic KW - Artificial intelligence KW - Information theory N1 - 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 UR - http://dx.doi.org/10.1007/978-3-642-39071-5 ER -