Theory and Applications of Satisfiability Testing - SAT 2006 : 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings / edited by Armin Biere, Carla P. Gomes.

Format:

Book

Contributor:

Biere, Armin, editor.

Gomes, Carla, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

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

Theoretical Computer Science and General Issues ; 4121

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

Edition:

First edition 2006.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2006.

System Details:

text file PDF

Contents:

Invited Talks

From Propositional Satisfiability to Satisfiability Modulo Theories

CSPs: Adding Structure to SAT

Session 1. Proofs and Cores

Complexity of Semialgebraic Proofs with Restricted Degree of Falsity

Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel

A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

Minimum Witnesses for Unsatisfiable 2CNFs

Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs

Extended Resolution Proofs for Symbolic SAT Solving with Quantification

Session 2. Heuristics and Algorithms

Encoding CNFs to Empower Component Analysis

Satisfiability Checking of Non-clausal Formulas Using General Matings

Determinization of Resolution by an Algorithm Operating on Complete Assignments

A Complete Random Jump Strategy with Guiding Paths

Session 3. Applications

Applications of SAT Solvers to Cryptanalysis of Hash Functions

Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies

Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/

SAT in Bioinformatics: Making the Case with Haplotype Inference

Session 4. SMT

Lemma Learning in SMT on Linear Constraints

On SAT Modulo Theories and Optimization Problems

Fast and Flexible Difference Constraint Propagation for DPLL(T)

A Progressive Simplifier for Satisfiability Modulo Theories

Session 5. Structure

Dependency Quantified Horn Formulas: Models and Complexity

On Linear CNF Formulas

A Dichotomy Theorem for Typed Constraint Satisfaction Problems

Session 6. MAX-SAT

A Complete Calculus for Max-SAT

On Solving the Partial MAX-SAT Problem

MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in Time

Average-Case Analysis for the MAX-2SAT Problem

Session 7. Local Search and Survey Propagation

Local Search for Unsatisfiability

Efficiency of Local Search

Implementing Survey Propagation on Graphics Processing Units

Characterizing Propagation Methods for Boolean Satisfiability

Session 8. QBF

Minimal False Quantified Boolean Formulas

Binary Clause Reasoning in QBF

Solving Quantified Boolean Formulas with Circuit Observability Don't Cares

QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency

Session 9. Counting and Concurrency

Solving #SAT Using Vertex Covers

Counting Models in Integer Domains

sharpSAT - Counting Models with Advanced Component Caching and Implicit BCP

A Distribution Method for Solving SAT in Grids.

Other Format:

Printed edition:

ISBN:

978-3-540-37207-3

9783540372073

Access Restriction:

Restricted for use by site license.