000			04936nam a22003855i 4500
001			295231
003			MX-SnUAN
005			20160429155219.0
007			cr nn 008mamaa
008			150903s2005 gw | o |||| 0|eng d
020			_a9783540316794 _99783540316794
024	7		_a10.1007/b137280 _2doi
035			_avtls000347870
039		9	_a201509031115 _bVLOAD _c201405070506 _dVLOAD _y201402070941 _zstaff
040			_aMX-SnUAN _bspa _cMX-SnUAN _erda
050		4	_aQA8.9-QA10.3
100	1		_aBacchus, Fahiem. _eeditor. _9329472
245	1	0	_aTheory and Applications of Satisfiability Testing : _b8th International Conference, SAT 2005, St Andrews, UK, June 19-23, 2005. Proceedings / _cedited by Fahiem Bacchus, Toby Walsh.
264		1	_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c2005.
300			_axii, 492 páginas Also available online. _brecurso en línea.
336			_atexto _btxt _2rdacontent
337			_acomputadora _bc _2rdamedia
338			_arecurso en línea _bcr _2rdacarrier
347			_aarchivo de texto _bPDF _2rda
490	0		_aLecture Notes in Computer Science, _x0302-9743 ; _v3569
500			_aSpringer eBooks
505	0		_aPreface -- 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.
520			_aThis book constitutes the refereed proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing, SAT 2005, held in St Andrews, Scotland in June 2005. The 26 revised full papers presented together with 16 revised short papers presented as posters during the technical programme were carefully selected from 73 submissions. The whole spectrum of research in propositional and quantified Boolean formula satisfiability testing is covered including proof systems, search techniques, probabilistic analysis of algorithms and their properties, problem encodings, industrial applications, specific tools, case studies, and empirical results.
590			_aPara consulta fuera de la UANL se requiere clave de acceso remoto.
700	1		_aWalsh, Toby. _eeditor. _9308622
710	2		_aSpringerLink (Servicio en línea) _9299170
776	0	8	_iEdición impresa: _z9783540262763
856	4	0	_uhttp://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/b137280 _zConectar a Springer E-Books (Para consulta externa se requiere previa autentificación en Biblioteca Digital UANL)
942			_c14
999			_c295231 _d295231