Theory and Applications of Satisfiability Testing : 8th International Conference, SAT 2005, St Andrews, Scotland, June 19-23, 2005, Proceedings / edited by Fahiem Bacchus, Toby Walsh.

Format:

Book

Contributor:

Bacchus, Fahiem, editor.

Walsh, Toby, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

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

Theoretical Computer Science and General Issues ; 3569

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

Edition:

First edition 2005.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2005.

System Details:

text file PDF

Summary:

The 8th International Conference on Theory and Applications of Satis?ability Testing(SAT2005)providedaninternationalforumforthemostrecentresearch on the satis?ablity problem (SAT). SAT is the classic problem of determining whether or not a propositional formula has a satisfying truth assignment. It was the ?rst problem shown by Cook to be NP-complete. Despite its seemingly specialized nature, satis?ability testing has proved to extremely useful in a wide range of di?erent disciplines, both from a practical as well as from a theoretical point of view. For example, work on SAT continues to provide insight into various fundamental problems in computation, and SAT solving technology has advanced to the point where it has become the most e?ective way of solving a number of practical problems. The SAT series of conferences are multidisciplinary conferences intended to bring together researchers from various disciplines who are interested in SAT. Topics of interest include, but are not limited to: proof systems and proof c- plexity; search algorithms and heuristics; analysis of algorithms; theories beyond the propositional; hard instances and random formulae; problem encodings; - dustrial applications; solvers and other tools. This volume contains the papers accepted for presentation at SAT 2005. The conference attracted a record number of 73 submissions. Of these, 26 papers were accepted for presentation in the technical programme. In addition, 16 - pers were accepted as shorter papers and were presented as posters during the technicalprogramme.Theacceptedpapersandposterpaperscoverthefullrange of topics listed in the call for papers.

Contents:

Preface

Solving Over-Constrained Problems with SAT Technology

A Symbolic Search Based Approach for Quantified Boolean Formulas

Substitutional Definition of Satisfiability in Classical Propositional Logic

A Clause-Based Heuristic for SAT Solvers

Effective Preprocessing in SAT Through Variable and Clause Elimination

Resolution and Pebbling Games

Local and Global Complete Solution Learning Methods for QBF

Equivalence Checking of Circuits with Parameterized Specifications

Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming

Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution

Resolution Tunnels for Improved SAT Solver Performance

Diversification and Determinism in Local Search for Satisfiability

On Finding All Minimally Unsatisfiable Subformulas

Optimizations for Compiling Declarative Models into Boolean Formulas

Random Walk with Continuously Smoothed Variable Weights

Derandomization of PPSZ for Unique-k-SAT

Heuristics for Fast Exact Model Counting

A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic

DPvis - A Tool to Visualize the Structure of SAT Instances

Constraint Metrics for Local Search

Input Distance and Lower Bounds for Propositional Resolution Proof Length

Sums of Squares, Satisfiability and Maximum Satisfiability

Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable

A New Approach to Model Counting

Benchmarking SAT Solvers for Bounded Model Checking

Model-Equivalent Reductions

Improved Exact Solvers for Weighted Max-SAT

Quantifier Trees for QBFs

Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas

A Branching Heuristics for Quantified Renamable Horn Formulas

An Improved Upper Bound for SAT

Bounded Model Checking with QBF

Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas

Automated Generation of Simplification Rules for SAT and MAXSAT

Speedup Techniques Utilized in Modern SAT Solvers

FPGA Logic Synthesis Using Quantified Boolean Satisfiability

On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization

A New Set of Algebraic Benchmark Problems for SAT Solvers

A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas

Threshold Behaviour of WalkSAT and Focused Metropolis Search on Random 3-Satisfiability

On Subsumption Removal and On-the-Fly CNF Simplification.

Other Format:

Printed edition:

ISBN:

978-3-540-31679-4

9783540316794

Access Restriction:

Restricted for use by site license.