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.
Author(s): Yehuda Naveh (auth.), Ofer Strichman, Stefan Szeider (eds.)
Series: Lecture Notes in Computer Science 6175 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 400
Tags: Algorithm Analysis and Problem Complexity; Software Engineering; Programming Techniques; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Mathematics of Computing
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 -
