Handbook of Satisfiability : (Record no. 66868)

000 -LEADER
fixed length control field 12551nam a22005773i 4500
001 - CONTROL NUMBER
control field EBC448770
003 - CONTROL NUMBER IDENTIFIER
control field MiAaPQ
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20181121152727.0
006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS--GENERAL INFORMATION
fixed length control field m o d |
007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION
fixed length control field cr cnu||||||||
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 181113s2009 xx o ||||0 eng d
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9781607503767
-- (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Cancelled/invalid ISBN 9781586039295
035 ## - SYSTEM CONTROL NUMBER
System control number (MiAaPQ)EBC448770
035 ## - SYSTEM CONTROL NUMBER
System control number (Au-PeEL)EBL448770
035 ## - SYSTEM CONTROL NUMBER
System control number (CaPaEBR)ebr10309230
035 ## - SYSTEM CONTROL NUMBER
System control number (CaONFJC)MIL577647
035 ## - SYSTEM CONTROL NUMBER
System control number (OCoLC)935268045
040 ## - CATALOGING SOURCE
Original cataloging agency MiAaPQ
Language of cataloging eng
Description conventions rda
-- pn
Transcribing agency MiAaPQ
Modifying agency MiAaPQ
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA9.3 -- .H36 2009eb
082 0# - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 006.3
100 1# - MAIN ENTRY--PERSONAL NAME
Personal name Biere, A.
245 10 - TITLE STATEMENT
Title Handbook of Satisfiability :
Remainder of title Handbook of Satisfiability.
264 #1 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Place of publication, distribution, etc Amsterdam :
Name of publisher, distributor, etc IOS Press,
Date of publication, distribution, etc 2009.
264 #4 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Date of publication, distribution, etc ©2009.
300 ## - PHYSICAL DESCRIPTION
Extent 1 online resource (980 pages)
336 ## - CONTENT TYPE
Content type term text
Content type code txt
Source rdacontent
337 ## - MEDIA TYPE
Media type term computer
Media type code c
Source rdamedia
338 ## - CARRIER TYPE
Carrier type term online resource
Carrier type code cr
Source rdacarrier
490 1# - SERIES STATEMENT
Series statement Frontiers in Artificial Intelligence and Applications ;
Volume number/sequential designation v.185
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Title page -- Contents -- Part I. Theory and Algorithms -- Chapter 1. A History of Satisfiability -- 1.1 Preface: the concept of satisfiability -- 1.2 The ancients -- 1.3 The medieval period -- 1.4 The renaissance -- 1.5 The first logic machine -- 1.6 Boolean algebra -- 1.7 Frege, logicism, and quantification logic -- 1.8 Russell and Whitehead -- 1.9 G"odel's incompleteness theorem -- 1.10 Effective process and recursive functions -- 1.11 Herbrand's theorem -- 1.12 Model theory and Satisfiability -- 1.13 Completeness of first-order logic -- 1.14 Application of logic to circuits -- 1.15 Resolution -- 1.16 The complexity or resolution -- 1.17 Refinement of Resolution-Based SAT Solvers -- 1.18 Upper bounds -- 1.19 Classes of easy expressions -- 1.20 Binary Decision Diagrams -- 1.21 Probabilistic analysis: SAT algorithms -- 1.22 Probabilistic analysis: thresholds -- 1.23 Stochastic Local Search -- 1.24 Maximum Satisfiability -- 1.25 Nonlinear formulations -- 1.26 Pseudo-Boolean Forms -- 1.27 Quantified Boolean formulas -- References -- Chapter 2. CNF Encodings -- 2.1 Introduction -- 2.2 Transformation to CNF -- 2.3 Case studies -- 2.4 Desirable properties of CNF encodings -- 2.5 Conclusion -- References -- Chapter 3. Complete Algorithms -- 3.1 Introduction -- 3.2 Technical Preliminaries -- 3.3 Satisfiability by Existential Quantification -- 3.4 Satisfiability by Inference Rules -- 3.5 Satisfiability by Search: The DPLL Algorithm -- 3.6 Satisfiability by Combining Search and Inference -- 3.7 Conclusions -- References -- Chapter 4. CDCL Solvers -- 4.1 Introduction -- 4.2 Notation -- 4.3 Organization of CDCL Solvers -- 4.4 Conflict Analysis -- 4.5 Modern CDCL Solvers -- 4.6 Bibliographical and Historical Notes -- References -- Chapter 5. Look-Ahead Based SAT Solvers -- 5.1 Introduction -- 5.2 General and Historical Overview -- 5.3 Heuristics.
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note 5.4 Additional Reasoning -- 5.5 Eager Data-Structures -- References -- Chapter 6. Incomplete Algorithms -- 6.1 Greedy Search and Focused Random Walk -- 6.2 Extensions of the Basic Local Search Method -- 6.3 Discrete Lagrangian Methods -- 6.4 The Phase Transition Phenomenon in Random k-SAT -- 6.5 A New Technique for Random k-SAT: Survey Propagation -- 6.6 Conclusion -- References -- Chapter 7. Fundaments of Branching Heuristics -- 7.1 Introduction -- 7.2 A general framework for branching algorithms -- 7.3 Branching tuples and the canonical projection -- 7.4 Estimating tree sizes -- 7.5 Axiomatising the canonical order on branching tuples -- 7.6 Alternative projections for restricted branching width -- 7.7 How to select distances and measures -- 7.8 Optimising distance functions -- 7.9 The order of branches -- 7.10 Beyond clause-sets -- 7.11 Conclusion and outlook -- References -- Chapter 8. Random Satisfiability -- 8.1 Introduction -- 8.2 The State of the Art -- 8.3 Random MAX k-SAT -- 8.4 Physical Predictions for Solution-space Geometry -- 8.5 The Role of the Second Moment Method -- 8.6 Generative models -- 8.7 Algorithms -- 8.8 Belief/Survey Propagation and the Algorithmic Barrier -- 8.9 Backtracking Algorithms -- 8.10 Exponential Running-Time for k > 3 -- References -- Chapter 9. Exploiting Runtime Variation in Complete Solvers -- 9.1 Runtime Variation in Backtrack Search -- 9.2 Exploiting Runtime Variation: Randomization and Restarts -- 9.3 Conclusion -- References -- Chapter 10. Symmetry and Satisfiability -- 10.1 Motivating Example -- 10.2 Preliminaries -- 10.3 Group Theory Basics -- 10.4 CNF Symmetry -- 10.5 Automorphism Group of a Colored Graph -- 10.6 Symmetry Detection -- 10.7 Symmetry Breaking -- 10.8 Summary and a Look Forward -- 10.9 Bibliographic Notes -- References -- Chapter 11. Minimal Unsatisfiability and Autarkies.
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note 11.1 Introduction -- 11.2 Deficiency -- 11.3 Resolution and Homomorphism -- 11.4 Special Classes -- 11.5 Extension to non-clausal formulas -- 11.6 Minimal Falsity for QBF -- 11.7 Applications and Experimental Results -- 11.8 Generalising satisfying assignments through "autarkies -- 11.9 The autarky monoid -- 11.10 Finding and using autarkies -- 11.11 Autarky systems: Using weaker forms of autarkies -- 11.12 Connections to combinatorics -- 11.13 Generalisations and extensions of autarkies -- 11.14 Conclusion -- References -- Chapter 12. Worst-Case Upper Bounds -- 12.1 Preliminaries -- 12.2 Tractable and intractable classes -- 12.3 Upper bounds for k-SAT -- 12.4 Upper bounds for General SAT -- 12.5 How large is the exponent? -- 12.6 Summary table -- References -- Chapter 13. Fixed-Parameter Tractability -- 13.1 Introduction -- 13.2 Fixed-Parameter Algorithms -- 13.3 Parameterized SAT -- 13.4 Backdoor Sets -- 13.5 Treewidth -- 13.6 Matchings -- 13.7 Concluding Remarks -- References -- Part II. Applications and Extensions -- Chapter 14. Bounded Model Checking -- 14.1 Model Checking -- 14.2 Bounded Semantics -- 14.3 Propositional Encodings -- 14.4 Completeness -- 14.5 Induction -- 14.6 Interpolation -- 14.7 Completeness with Interpolation -- 14.8 Invariant Strengthening -- 14.9 Related Work -- 14.10 Conclusion -- References -- Chapter 15. Planning and SAT -- 15.1 Introduction -- 15.2 Notation -- 15.3 Sequential Plans -- 15.4 Parallel Plans -- 15.5 Finding a Satisfiable Formula -- 15.6 Improved SAT Solving for Planning -- 15.7 QBF and Planning with Nondeterministic Actions -- References -- Chapter 16. Software Verification -- 16.1 Programs use Bit-Vectors -- 16.2 Formal Models of Software -- 16.3 Turning Bit-Vector Arithmetic into CNF -- 16.4 Bounded Model Checking for Software -- 16.5 Predicate Abstraction using SAT -- 16.6 Conclusion -- References.
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note Chapter 17. Combinatorial Designs by SAT Solvers -- 17.1 Introduction -- 17.2 Quasigroup Problems -- 17.3 Ramsey and Van der Waerden Numbers -- 17.4 Covering Arrays -- 17.5 Steiner Systems -- 17.6 Mendelsohn Designs -- 17.7 Encoding Design Theory Problems -- 17.8 Conclusions and Open Problems -- References -- Chapter 18. Connections to Statistical Physics -- 18.1 Introduction -- 18.2 Phase Transitions: Basic Concepts and Illustration -- 18.3 Phase transitions in random CSPs -- 18.4 Local search algorithms -- 18.5 Decimation based algorithms -- 18.6 Conclusion -- References -- Chapter 19. MaxSAT -- 19.1 Introduction -- 19.2 Preliminaries -- 19.3 Branch and Bound Algorithms -- 19.4 Complete Inference in MaxSAT -- 19.5 Approximation Algorithms -- 19.6 Partial MaxSAT and Soft Constraints -- 19.7 Evaluations of MaxSAT Solvers -- 19.8 Conclusions -- References -- Chapter 20. Model Counting -- 20.1 Computational Complexity of Model Counting -- 20.2 Exact Model Counting -- 20.3 Approximate Model Counting -- 20.4 Conclusion -- References -- Chapter 21. Non-Clausal SAT and ATPG -- 21.1 Introduction -- 21.2 Basic Definitions -- 21.3 Satisfiability Checking for Boolean Circuits -- 21.4 Automatic Test Pattern Generation -- 21.5 Conclusions -- References -- Chapter 22. Pseudo-Boolean and Cardinality Constraints -- 22.1 Introduction -- 22.2 Basic Definitions -- 22.3 Decision Problem versus Optimization Problem -- 22.4 Expressive Power of Cardinality and Pseudo-Boolean Constraints -- 22.5 Inference Rules -- 22.6 Current Algorithms -- 22.7 Conclusion -- References -- Chapter 23. QBF Theory -- 23.1 Introduction -- 23.2 Syntax and Semantics -- 23.3 Complexity Results -- 23.4 Models and Expressive power -- 23.5 Q-Resolution -- 23.6 Quantified Horn Formulas and Q2-CNF -- References -- Chapter 24. QBFs reasoning -- 24.1 Introduction -- 24.2 Quantified Boolean Logic.
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note 24.3 Applications of QBFs and QBF reasoning -- 24.4 QBF solvers -- 24.5 Other approaches, extensions and conclusions -- References -- Chapter 25. SAT Techniques for Modal and Description Logics -- 25.1 Introduction -- 25.2 Background -- 25.3 Basic Modal DPLL -- 25.4 Advanced Modal DPLL -- 25.5 The OBDD-based Approach -- 25.6 The Eager DPLL-based approach -- References -- Chapter 26. Satisfiability Modulo Theories -- 26.1 Introduction -- 26.2 Background -- 26.3 Eager Encodings to SAT -- 26.4 Integrating Theory Solvers into SAT Engines -- 26.5 Theory Solvers -- 26.6 Combining Theories -- 26.7 Extensions and Enhancements -- References -- Chapter 27. Stochastic Boolean Satisfiability -- 27.1 Introduction -- 27.2 Definitions and Notation -- 27.3 Complexity of SSAT and Related Problems -- 27.4 Applications -- 27.5 Analytical Results -- 27.6 Algorithms and Empirical Results -- 27.7 Stochastic Constraint Programming -- 27.8 Future Directions -- References -- Subject Index -- Cited Author Index -- Contributing Authors and Affiliations.
520 ## - SUMMARY, ETC.
Summary, etc "Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT. My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software. Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas. Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way. Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field."--Edmund Clarke (FORE Systems University Professor of Computer Science and Professor of Electrical
520 8# - SUMMARY, ETC.
Summary, etc and Computer Engineering at Carnegie Mellon University, winner of the 2007 A.M. Turing Award).
588 ## - SOURCE OF DESCRIPTION NOTE
Source of description note Description based on publisher supplied metadata and other sources.
590 ## - LOCAL NOTE (RLIN)
Local note Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2018. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Algebra, Boolean -- Congresses.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer algorithms -- Congresses.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Decision making -- Congresses.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Propositional calculus -- Congresses.
655 #4 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Electronic books.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Heule, M.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name van Maaren, H.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Walsh, T.
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Display text Print version:
Main entry heading Biere, A.
Title Handbook of Satisfiability : Handbook of Satisfiability
Place, publisher, and date of publication Amsterdam : IOS Press,c2009
International Standard Book Number 9781586039295
797 2# - LOCAL ADDED ENTRY--CORPORATE NAME (RLIN)
Corporate name or jurisdiction name as entry element ProQuest (Firm)
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Frontiers in Artificial Intelligence and Applications
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://ebookcentral.proquest.com/lib/buse-ebooks/detail.action?docID=448770">https://ebookcentral.proquest.com/lib/buse-ebooks/detail.action?docID=448770</a>
Public note Click to View

No items available.

Powered by Koha