Theory and Applications of Satisfiability Testing
Editat de Fahiem Bacchus, Toby Walshen Limba Engleză Paperback – 9 iun 2005
Preț: 331.80 lei
Preț vechi: 414.75 lei
-20% Nou
Puncte Express: 498
Preț estimativ în valută:
58.72€ • 68.47$ • 51.55£
58.72€ • 68.47$ • 51.55£
Carte tipărită la comandă
Livrare economică 16-30 ianuarie 26
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783540262763
ISBN-10: 3540262768
Pagini: 508
Ilustrații: XII, 492 p.
Dimensiuni: 155 x 235 x 28 mm
Greutate: 0.76 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540262768
Pagini: 508
Ilustrații: XII, 492 p.
Dimensiuni: 155 x 235 x 28 mm
Greutate: 0.76 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
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.- AnImproved 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.