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.
Author(s): Josep Argelich, Felip Manyà (auth.), Fahiem Bacchus, Toby Walsh (eds.)
Series: Lecture Notes in Computer Science 3569 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 492
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 -
Solving Over-Constrained Problems with SAT Technology....Pages 1-15
A Symbolic Search Based Approach for Quantified Boolean Formulas....Pages 16-30
Substitutional Definition of Satisfiability in Classical Propositional Logic....Pages 31-45
A Clause-Based Heuristic for SAT Solvers....Pages 46-60
Effective Preprocessing in SAT Through Variable and Clause Elimination....Pages 61-75
Resolution and Pebbling Games....Pages 76-90
Local and Global Complete Solution Learning Methods for QBF....Pages 91-106
Equivalence Checking of Circuits with Parameterized Specifications....Pages 107-121
Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming....Pages 122-134
Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution....Pages 135-142
Resolution Tunnels for Improved SAT Solver Performance....Pages 143-157
Diversification and Determinism in Local Search for Satisfiability....Pages 158-172
On Finding All Minimally Unsatisfiable Subformulas....Pages 173-186
Optimizations for Compiling Declarative Models into Boolean Formulas....Pages 187-202
Random Walk with Continuously Smoothed Variable Weights....Pages 203-215
Derandomization of PPSZ for Unique- k -SAT....Pages 216-225
Heuristics for Fast Exact Model Counting....Pages 226-240
A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic....Pages 241-256
DPvis – A Tool to Visualize the Structure of SAT Instances....Pages 257-268
Constraint Metrics for Local Search....Pages 269-281
Input Distance and Lower Bounds for Propositional Resolution Proof Length....Pages 282-293
Sums of Squares, Satisfiability and Maximum Satisfiability....Pages 294-308
Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable....Pages 309-323
A New Approach to Model Counting....Pages 324-339
Benchmarking SAT Solvers for Bounded Model Checking....Pages 340-354
Model-Equivalent Reductions....Pages 355-370
Improved Exact Solvers for Weighted Max-SAT....Pages 371-377
Quantifier Trees for QBFs....Pages 378-385
Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas....Pages 386-392
A Branching Heuristics for Quantified Renamable Horn Formulas....Pages 393-399
An Improved Upper Bound for SAT....Pages 400-407
Bounded Model Checking with QBF....Pages 408-414
Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies....Pages 415-422
Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas....Pages 423-429
Automated Generation of Simplification Rules for SAT and MAXSAT....Pages 430-436
Speedup Techniques Utilized in Modern SAT Solvers....Pages 437-443
FPGA Logic Synthesis Using Quantified Boolean Satisfiability....Pages 444-450
On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization....Pages 451-458
A New Set of Algebraic Benchmark Problems for SAT Solvers....Pages 459-466
A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas....Pages 467-474
Threshold Behaviour of WalkSAT and Focused Metropolis Search on Random 3-Satisfiability....Pages 475-481
On Subsumption Removal and On-the-Fly CNF Simplification....Pages 482-489
Back Matter....Pages -
