Theory and Applications of Satisfiability Testing: 8th International Conference, SAT 2005, St Andrews, Scotland, June 19-23, 2005, ProceedingsThe 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 | 1 |
A Symbolic Search Based Approach for Quantified Boolean Formulas | 16 |
Substitutional Definition of Satisfiability in Classical Propositional Logic | 31 |
A ClauseBased Heuristic for SAT Solvers | 46 |
Effective Preprocessing in SAT Through Variable and Clause | 61 |
Resolution and Pebbling Games | 76 |
Local and Global Complete Solution Learning Methods for | 91 |
Equivalence Checking of Circuits with Parameterized Specifications | 107 |
DPvis A Tool to Visualize the Structure of SAT Instances | 257 |
Input Distance and Lower Bounds for Propositional Resolution Proof | 282 |
Faster Exact Solving of SAT Formulae with a Low Number | 309 |
A New Approach to Model Counting | 324 |
Benchmarking SAT Solvers for Bounded Model Checking | 340 |
ModelEquivalent Reductions | 355 |
Improved Exact Solvers for Weighted MaxSAT | 371 |
Quantifier Rewriting and Equivalence Models for Quantified Horn | 386 |
Observed Lower Bounds for Random 3SAT Phase Transition Density | 122 |
Simulating Cutting Plane Proofs with Restricted Degree of Falsity | 135 |
Diversification and Determinism in Local Search for Satisfiability | 158 |
On Finding All Minimally Unsatisfiable Subformulas | 173 |
Optimizations for Compiling Declarative Models into Boolean Formulas | 187 |
Random Walk with Continuously Smoothed Variable Weights | 203 |
Derandomization of PPSZ for UniquekSAT | 216 |
A Scalable Method for Solving Satisfiability of Integer Linear | 241 |
An Improved Upper Bound for | 400 |
Variable Ordering for Efficient SAT Search by Analyzing | 415 |
Automated Generation of Simplification Rules for SAT and MAXSAT | 430 |
FPGA Logic Synthesis Using Quantified Boolean Satisfiability | 444 |
A New Set of Algebraic Benchmark Problems for SAT Solvers | 459 |
Threshold Behaviour of WalkSAT and Focused Metropolis Search | 475 |
| 491 | |
Other editions - View all
Common terms and phrases
added algorithm applied approach assignment backtracks benchmarks block Boolean boolean formula bound branching called circuits clauses CNF formula compared complete Computer Conference consider constraints contains corresponding counting decision defined Definition denote described different equivalent evaluation example existential exists experiments false first flipped formula function give given graph hard heuristic implemented implication improve increase indicator input instances learning least Lemma length linear literal logic lower bound means method node Note obtained occurs optimizations original performance polynomial possible present problem procedure Proceedings Programming proof propositional prove quantified random reasoning reduced removed represent resolution respectively SAT solvers satisfiability satisfying selected shown solution solving space step strategy structure substitution Table techniques Testing Theorem tree true unit universal unsatisfied variables weights