000			04943nam a22006135i 4500
001			978-3-540-37207-3
003			DE-He213
005			20240423125859.0
007			cr nn 008mamaa
008			100301s2006 gw | s |||| 0|eng d
020			_a9783540372073 _9978-3-540-37207-3
024	7		_a10.1007/11814948 _2doi
050		4	_aQA267-268.5
072		7	_aUYA _2bicssc
072		7	_aCOM014000 _2bisacsh
072		7	_aUYA _2thema
082	0	4	_a005.131 _223
245	1	0	_aTheory and Applications of Satisfiability Testing - SAT 2006 _h[electronic resource] : _b9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings / _cedited by Armin Biere, Carla P. Gomes.
250			_a1st ed. 2006.
264		1	_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg : _bImprint: Springer, _c2006.
300			_aXII, 440 p. _bonline resource.
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
347			_atext file _bPDF _2rda
490	1		_aTheoretical Computer Science and General Issues, _x2512-2029 ; _v4121
505	0		_aInvited Talks -- From Propositional Satisfiability to Satisfiability Modulo Theories -- CSPs: Adding Structure to SAT -- Session 1. Proofs and Cores -- Complexity of Semialgebraic Proofs with Restricted Degree of Falsity -- Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel -- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction -- Minimum Witnesses for Unsatisfiable 2CNFs -- Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs -- Extended Resolution Proofs for Symbolic SAT Solving with Quantification -- Session 2. Heuristics and Algorithms -- Encoding CNFs to Empower Component Analysis -- Satisfiability Checking of Non-clausal Formulas Using General Matings -- Determinization of Resolution by an Algorithm Operating on Complete Assignments -- A Complete Random Jump Strategy with Guiding Paths -- Session 3. Applications -- Applications of SAT Solvers to Cryptanalysis of Hash Functions -- Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies -- Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ -- SAT in Bioinformatics: Making the Case with Haplotype Inference -- Session 4. SMT -- Lemma Learning in SMT on Linear Constraints -- On SAT Modulo Theories and Optimization Problems -- Fast and Flexible Difference Constraint Propagation for DPLL(T) -- A Progressive Simplifier for Satisfiability Modulo Theories -- Session 5. Structure -- Dependency Quantified Horn Formulas: Models and Complexity -- On Linear CNF Formulas -- A Dichotomy Theorem for Typed Constraint Satisfaction Problems -- Session 6. MAX-SAT -- A Complete Calculus for Max-SAT -- On Solving the Partial MAX-SAT Problem -- MAX-SAT for Formulas with Constant ClauseDensity Can Be Solved Faster Than in Time -- Average-Case Analysis for the MAX-2SAT Problem -- Session 7. Local Search and Survey Propagation -- Local Search for Unsatisfiability -- Efficiency of Local Search -- Implementing Survey Propagation on Graphics Processing Units -- Characterizing Propagation Methods for Boolean Satisfiability -- Session 8. QBF -- Minimal False Quantified Boolean Formulas -- Binary Clause Reasoning in QBF -- Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares -- QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency -- Session 9. Counting and Concurrency -- Solving #SAT Using Vertex Covers -- Counting Models in Integer Domains -- sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP -- A Distribution Method for Solving SAT in Grids.
650		0	_aMachine theory.
650		0	_aAlgorithms.
650		0	_aOperating systems (Computers).
650		0	_aNumerical analysis.
650		0	_aArtificial intelligence.
650		0	_aMathematical logic.
650	1	4	_aFormal Languages and Automata Theory.
650	2	4	_aAlgorithms.
650	2	4	_aOperating Systems.
650	2	4	_aNumerical Analysis.
650	2	4	_aArtificial Intelligence.
650	2	4	_aMathematical Logic and Foundations.
700	1		_aBiere, Armin. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt
700	1		_aGomes, Carla P. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt
710	2		_aSpringerLink (Online service)
773	0		_tSpringer Nature eBook
776	0	8	_iPrinted edition: _z9783540372066
776	0	8	_iPrinted edition: _z9783540827535
830		0	_aTheoretical Computer Science and General Issues, _x2512-2029 ; _v4121
856	4	0	_uhttps://doi.org/10.1007/11814948
912			_aZDB-2-SCS
912			_aZDB-2-SXCS
912			_aZDB-2-LNC
942			_cSPRINGER
999			_c182674 _d182674