MARC details
| 000 -LEADER |
|---|
| fixed length control field |
06315nam a22005775i 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
978-3-540-31679-4 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
DE-He213 |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20160302161807.0 |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION |
|---|
| fixed length control field |
cr nn 008mamaa |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
100715s2005 gw | s |||| 0|eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783540316794 |
| -- |
978-3-540-31679-4 |
| 024 7# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.1007/b137280 |
| Source of number or code |
doi |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA8.9-QA10.3 |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
UYA |
| Source |
bicssc |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
MAT018000 |
| Source |
bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
COM051010 |
| Source |
bisacsh |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
005.131 |
| Edition number |
23 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Theory and Applications of Satisfiability Testing |
| Medium |
[electronic resource] : |
| Remainder of title |
8th International Conference, SAT 2005, St Andrews, UK, June 19-23, 2005. Proceedings / |
| Statement of responsibility, etc. |
edited by Fahiem Bacchus, Toby Walsh. |
| 264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE |
|---|
| Place of production, publication, distribution, manufacture |
Berlin, Heidelberg : |
| Name of producer, publisher, distributor, manufacturer |
Springer Berlin Heidelberg, |
| Date of production, publication, distribution, manufacture, or copyright notice |
2005. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
XII, 492 p. |
| Other physical details |
online resource. |
| 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 |
| 347 ## - DIGITAL FILE CHARACTERISTICS |
|---|
| File type |
text file |
| Encoding format |
PDF |
| Source |
rda |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture Notes in Computer Science, |
| International Standard Serial Number |
0302-9743 ; |
| Volume/sequential designation |
3569 |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
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. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
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 was the ?rst problem shown by Cook to be NP-complete. Despite its seemingly specialized nature, satis?ability testing has proved to extremely useful in a wide range of di?erent disciplines, both from a practical as well as from a theoretical point of view. For example, work on SAT continues to provide insight into various fundamental problems in computation, and SAT solving technology has advanced to the point where it has become the most e?ective way of solving a number of practical problems. The SAT series of conferences are multidisciplinary conferences intended to bring together researchers from various disciplines who are interested in SAT. Topics of interest include, but are not limited to: proof systems and proof c- plexity; search algorithms and heuristics; analysis of algorithms; theories beyond the propositional; hard instances and random formulae; problem encodings; - dustrial applications; solvers and other tools. This volume contains the papers accepted for presentation at SAT 2005. The conference attracted a record number of 73 submissions. Of these, 26 papers were accepted for presentation in the technical programme. In addition, 16 - pers were accepted as shorter papers and were presented as posters during the technicalprogramme.Theacceptedpapersandposterpaperscoverthefullrange of topics listed in the call for papers. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Operating systems (Computers). |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Algorithms. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Mathematical logic. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Numerical analysis. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Artificial intelligence. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Mathematical Logic and Formal Languages. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Algorithm Analysis and Problem Complexity. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Operating Systems. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Numeric Computing. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Artificial Intelligence (incl. Robotics). |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Mathematical Logic and Foundations. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Bacchus, Fahiem. |
| Relator term |
editor. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Walsh, Toby. |
| Relator term |
editor. |
| 710 2# - ADDED ENTRY--CORPORATE NAME |
|---|
| Corporate name or jurisdiction name as entry element |
SpringerLink (Online service) |
| 773 0# - HOST ITEM ENTRY |
|---|
| Title |
Springer eBooks |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Printed edition: |
| International Standard Book Number |
9783540262763 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture Notes in Computer Science, |
| International Standard Serial Number |
0302-9743 ; |
| Volume number/sequential designation |
3569 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Uniform Resource Identifier |
<a href="http://dx.doi.org/10.1007/b137280">http://dx.doi.org/10.1007/b137280</a> |
| 912 ## - |
|---|
| -- |
ZDB-2-SCS |
| 912 ## - |
|---|
| -- |
ZDB-2-LNC |
