Theory and Applications of Satisfiability Testing - SAT 2007 : 10th International Conference, SAT 2007, Lisbon, Portugal, May 28-31, 2007, Proceedings / edited by Joao Marques-Silva, Karem A. Sakallah.

Format:

Book

Contributor:

Marques-Silva, João, editor.

Sakallah, Karem A., editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 4501.

Theoretical Computer Science and General Issues ; 4501

Language:

English

Subjects (All):

Logic, Symbolic and mathematical.

Algorithms.

Operating systems (Computers).

Numerical analysis.

Artificial intelligence.

Mathematical Logic and Formal Languages.

Algorithm Analysis and Problem Complexity.

Operating Systems.

Numeric Computing.

Artificial Intelligence.

Mathematical Logic and Foundations.

Local Subjects:

Mathematical Logic and Formal Languages.

Algorithm Analysis and Problem Complexity.

Operating Systems.

Numeric Computing.

Artificial Intelligence.

Mathematical Logic and Foundations.

Physical Description:

1 online resource (XII, 388 pages).

Edition:

First edition 2007.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2007.

System Details:

text file PDF

Summary:

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.

Contents:

SAT: Past and Future

Encodings of Problems in Effectively Propositional Logic

Efficient Circuit to CNF Conversion

Mapping CSP into Many-Valued SAT

Circuit Based Encoding of CNF Formula

Breaking Symmetries in SAT Matrix Models

Partial Max-SAT Solvers with Clause Learning

MiniMaxSat: A New Weighted Max-SAT Solver

Solving Multi-objective Pseudo-Boolean Problems

Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities

Horn Upper Bounds and Renaming

Matched Formulas and Backdoor Sets

Short XORs for Model Counting: From Theory to Practice

Variable Dependency in Local Search: Prevention Is Better Than Cure

Combining Adaptive Noise and Look-Ahead in Local Search for SAT

From Idempotent Generalized Boolean Assignments to Multi-bit Search

Satisfiability with Exponential Families

Formalizing Dangerous SAT Encodings

Algorithms for Variable-Weighted 2-SAT and Dual Problems

On the Boolean Connectivity Problem for Horn Relations

A First Step Towards a Unified Proof Checker for QBF

Dynamically Partitioning for Solving QBF

Backdoor Sets of Quantified Boolean Formulas

Bounded Universal Expansion for Preprocessing QBF

Effective Incorporation of Double Look-Ahead Procedures

Applying Logic Synthesis for Speeding Up SAT

Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver

A Lightweight Component Caching Scheme for Satisfiability Solvers

Minimum 2CNF Resolution Refutations in Polynomial Time

Polynomial Time SAT Decision for Complementation-Invariant Clause-Sets, and Sign-non-Singular Matrices

Verifying Propositional Unsatisfiability: Pitfalls to Avoid

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories

SAT Solving for Termination Analysis with Polynomial Interpretations

Fault Localization and Correction with QBF

Sensor Deployment for Failure Diagnosis in Networked Aerial Robots: A Satisfiability-Based Approach

Inversion Attacks on Secure Hash Functions Using sat Solvers.

Other Format:

Printed edition:

ISBN:

978-3-540-72788-0

9783540727880

Access Restriction:

Restricted for use by site license.