Theory and Applications of Satisfiability Testing - SAT 2010: 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010, Proceedings (Lecture Notes in Computer Science)

Annotation. This Book Constitutes The Refereed Proceedings Of The 13th International Conference On Theory And Applications Of Satisfiability Testing, Sat 2010, Held In Edinburgh, Uk, In July 2010 As Part Of The Federated Logic Conference, Floc 2010. The 21 Revised Full Papers Presented Together With 14 Revised Short Papers And 2 Invited Talks Were Carefully Selected From 75 Submissions. The Papers Cover A Broad Range Of Topics Such As Proof Systems And Proof Complexity; Search Algorithms And Heuristics; Analysis Of Algorithms; Combinatorial Theory Of Satisfiability; Random Instances Vs Structured Instances; Problem Encodings; Industrial Applications; Applications To Combinatorics; Solvers, Simplifiers And Tools; And Exact And Parameterized Algorithms. Front Matter....Pages - The Big Deal: Applying Constraint Satisfaction Technologies Where It Makes the Difference....Pages 1-7 Exact Algorithms and Complexity....Pages 8-9 Improving Stochastic Local Search for SAT with a New Probability Distribution....Pages 10-15 Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas....Pages 16-29 Proof Complexity of Propositional Default Logic....Pages 30-43 Automated Testing and Debugging of SAT and QBF Solvers....Pages 44-57 Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN....Pages 58-70 Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT....Pages 71-84 sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning....Pages 85-98 Non Uniform Selection of Solutions for Upper Bounding the 3-SAT Threshold....Pages 99-112 Symmetry and Satisfiability: An Update....Pages 113-127 A Non-prenex, Non-clausal QBF Solver with Game-State Learning....Pages 128-142 SAT Solving with Reference Points....Pages 143-157 Integrating Dependency Schemes in Search-Based QBF Solvers....Pages 158-171 An Exact Algorithm for the Boolean Connectivity Problem for k -CNF....Pages 172-180 Improving Unsatisfiability-Based Algorithms for Boolean Optimization....Pages 181-193 Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs....Pages 194-208 Statistical Methodology for Comparison of SAT Solvers....Pages 209-222 On the Relative Merits of Simple Local Search Methods for the MAX-SAT Problem....Pages 223-236 The Seventh QBF Solvers Evaluation (QBFEVAL’10)....Pages 237-250 Complexity Results for Linear XSAT-Problems....Pages 251-263 Bounds on Threshold of Regular Random k -SAT....Pages 264-277 Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT....Pages 278-292 Improved Local Search for Circuit Satisfiability....Pages 293-299 A System for Solving Constraint Satisfaction Problems with SMT....Pages 300-305 Two Techniques for Minimizing Resolution Proofs....Pages 306-312 On Moderately Exponential Time for SAT....Pages 313-325 Minimising Deterministic Büchi Automata Precisely Using SAT Solving....Pages 326-332 Exploiting Circuit Representations in QBF Solving....Pages 333-339 Reconstructing Solutions after Blocked Clause Elimination....Pages 340-345 An Empirical Study of Optimal Noise and Runtime Distributions in Local Search....Pages 346-351 Green-Tao Numbers and SAT....Pages 352-362 Exact MinSAT Solving....Pages 363-368 Uniquely Satisfiable k -SAT Instances with Almost Minimal Occurrences of Each Variable....Pages 369-374 Assignment Stack Shrinking....Pages 375-381 Simple but Hard Mixed Horn Formulas....Pages 382-387 Zero-One Designs Produce Small Hard SAT Instances....Pages 388-397 Back Matter....Pages -