Theory and Applications of Satisfiability Testing 8th International Conference, SAT 2005, St Andrews, UK, June 19-23, 2005. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Bacchus, Fahiem (Επιμελητής έκδοσης), Walsh, Toby (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2005.
• Σειρά: Lecture Notes in Computer Science, 3569
• Θέματα: Computer science.; Operating systems (Computers).; Algorithms.; Mathematical logic.; Numerical analysis.; Artificial intelligence.; Computer Science.; Mathematical Logic and Formal Languages.; Algorithm Analysis and Problem Complexity.; Operating Systems.; Numeric Computing.; Artificial Intelligence (incl. Robotics).; Mathematical Logic and Foundations.

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...

Πίνακας περιεχομένων:

• 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.