This volume contains the papers presented at SAT 2007: 10th International Conference on Theory and Applications of Satis?ability Testing. The International Conferences on Theory and Applications of Satis?ability Testing (SAT) originated in 1996 as a series of workshops “on Satis?ability.” By the third meeting in 2000, the workshop had attracted a mix of theorists and experimentalists whose common interest was the enhancement of our basic understanding of the theoretical underpinnings of the Satis?ability problem as well as the development of scalable algorithms for its solution in a wide range of application domains. In 2002 a competition of SAT solvers was inaugurated to spur further algorithmic and implementation developments, and to create an eclectic collection of benchmarks. The competition—expanded in subsequent years to include pseudo Boolean, QBF, and MAX-SAT solvers—has become an integralpartofthesemeetings,addinganelementofexcitementandanticipation. Theinterplaybetweentheoryandapplication,aswellastheincreasedinterestin Satis?abilityfromawider communityofresearchers,ledtothe naturalevolution of these initial workshops into the current conference format. The annual SAT conference is now universally recognized as “the venue” for publishing the latest advances in SAT research.
Author(s): Martin Davis (auth.), João Marques-Silva, Karem A. Sakallah (eds.)
Series: Lecture Notes in Computer Science 4501 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2007
Language: English
Pages: 388
Tags: Mathematical Logic and Formal Languages; Algorithm Analysis and Problem Complexity; Operating Systems; Numeric Computing; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations
Front Matter....Pages -
SAT: Past and Future....Pages 1-2
Encodings of Problems in Effectively Propositional Logic....Pages 3-3
Efficient Circuit to CNF Conversion....Pages 4-9
Mapping CSP into Many-Valued SAT....Pages 10-15
Circuit Based Encoding of CNF Formula....Pages 16-21
Breaking Symmetries in SAT Matrix Models....Pages 22-27
Partial Max-SAT Solvers with Clause Learning....Pages 28-40
MiniMaxSat: A New Weighted Max-SAT Solver....Pages 41-55
Solving Multi-objective Pseudo-Boolean Problems....Pages 56-69
Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities....Pages 70-79
Horn Upper Bounds and Renaming....Pages 80-93
Matched Formulas and Backdoor Sets....Pages 94-99
Short XORs for Model Counting: From Theory to Practice....Pages 100-106
Variable Dependency in Local Search: Prevention Is Better Than Cure....Pages 107-120
Combining Adaptive Noise and Look-Ahead in Local Search for SAT....Pages 121-133
From Idempotent Generalized Boolean Assignments to Multi-bit Search....Pages 134-147
Satisfiability with Exponential Families....Pages 148-158
Formalizing Dangerous SAT Encodings....Pages 159-172
Algorithms for Variable-Weighted 2-SAT and Dual Problems....Pages 173-186
On the Boolean Connectivity Problem for Horn Relations....Pages 187-200
A First Step Towards a Unified Proof Checker for QBF....Pages 201-214
Dynamically Partitioning for Solving QBF....Pages 215-229
Backdoor Sets of Quantified Boolean Formulas....Pages 230-243
Bounded Universal Expansion for Preprocessing QBF....Pages 244-257
Effective Incorporation of Double Look-Ahead Procedures....Pages 258-271
Applying Logic Synthesis for Speeding Up SAT....Pages 272-286
Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver....Pages 287-293
A Lightweight Component Caching Scheme for Satisfiability Solvers....Pages 294-299
Minimum 2CNF Resolution Refutations in Polynomial Time....Pages 300-313
Polynomial Time SAT Decision for Complementation-Invariant Clause-Sets, and Sign-non-Singular Matrices....Pages 314-327
Verifying Propositional Unsatisfiability: Pitfalls to Avoid....Pages 328-333
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories....Pages 334-339
SAT Solving for Termination Analysis with Polynomial Interpretations....Pages 340-354
Fault Localization and Correction with QBF....Pages 355-368
Sensor Deployment for Failure Diagnosis in Networked Aerial Robots: A Satisfiability-Based Approach....Pages 369-376
Inversion Attacks on Secure Hash Functions Using sat Solvers....Pages 377-382
Back Matter....Pages -
