Theory and Applications of Satisfiability Testing - SAT 2009 : 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings / edited by Oliver Kullmann.

Format:

Book

Contributor:

Kullmann, Oliver, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

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

Theoretical Computer Science and General Issues ; 5584

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, 540 pages).

Edition:

First edition 2009.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2009.

System Details:

text file PDF

Summary:

This book constitutes the refereed proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009, held in Swansea, UK, in June/July 2009. The 34 revised full papers presented together with 11 revised short papers and 2 invited talks were carefully selected from 86 submissions. The papers are organized in topical sections on applications of SAT, complexity theory, structures for SAT, resolution and SAT, translations to CNF, techniques for conflict-driven SAT Solvers, solving SAT by local search, hybrid SAT solvers, automatic adaption of SAT solvers, stochastic approaches to SAT solving, QBFs and their representations, optimization algorithms, distributed and parallel solving.

Contents:

Invited Talks

SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms

Symbolic Techniques in Propositional Satisfiability Solving

Applications of SAT

Efficiently Calculating Evolutionary Tree Measures Using SAT

Finding Lean Induced Cycles in Binary Hypercubes

Finding Efficient Circuits Using SAT-Solvers

Encoding Treewidth into SAT

Complexity Theory

The Complexity of Reasoning for Fragments of Default Logic

Does Advice Help to Prove Propositional Tautologies?

Structures for SAT

Backdoors in the Context of Learning

Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences

On Some Aspects of Mixed Horn Formulas

Variable Influences in Conjunctive Normal Forms

Resolution and SAT

Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution

An Exponential Lower Bound for Width-Restricted Clause Learning

Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces

Boundary Points and Resolution

Translations to CNF

Sequential Encodings from Max-CSP into Partial Max-SAT

Cardinality Networks and Their Applications

New Encodings of Pseudo-Boolean Constraints into CNF

Efficient Term-ITE Conversion for Satisfiability Modulo Theories

Techniques for Conflict-Driven SAT Solvers

On-the-Fly Clause Improvement

Dynamic Symmetry Breaking by Simulating Zykov Contraction

Minimizing Learned Clauses

Extending SAT Solvers to Cryptographic Problems

Solving SAT by Local Search

Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability

A Theoretical Analysis of Search in GSAT

The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT

Hybrid SAT Solvers

A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem

Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques

Automatic Adaption of SAT Solvers

Restart Strategy Selection Using Machine Learning Techniques

Instance-Based Selection of Policies for SAT Solvers

Width-Based Restart Policies for Clause-Learning Satisfiability Solvers

Problem-Sensitive Restart Heuristics for the DPLL Procedure

Stochastic Approaches to SAT Solving

(1,2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms

VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search

QBFs and Their Representations

Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits

A Compact Representation for Syntactic Dependencies in QBFs

Beyond CNF: A Circuit-Based QBF Solver

Optimisation Algorithms

Solving (Weighted) Partial MaxSAT through Satisfiability Testing

Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation?

Relaxed DPLL Search for MaxSAT

Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates

Exploiting Cycle Structures in Max-SAT

Generalizing Core-Guided Max-SAT

Algorithms for Weighted Boolean Optimization

Distributed and Parallel Solving

PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing

c-sat: A Parallel SAT Solver for Clusters.

Other Format:

Printed edition:

ISBN:

978-3-642-02777-2

9783642027772

Access Restriction:

Restricted for use by site license.