000 -LEADER |
fixed length control field |
05572nam a22005895i 4500 |
020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
ISBN |
9783540727880 |
-- |
978-3-540-72788-0 |
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
Classification number |
005.131 |
245 10 - TITLE STATEMENT |
Title |
Theory and Applications of Satisfiability Testing – SAT 2007 |
Sub Title |
10th International Conference, Lisbon, Portugal, May 28-31, 2007. Proceedings / |
Statement of responsibility, etc |
edited by João Marques-Silva, Karem A. Sakallah. |
260 #1 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
Place of publication |
Berlin, Heidelberg : |
Name of publisher |
Springer Berlin Heidelberg, |
Year of publication |
2007. |
300 ## - PHYSICAL DESCRIPTION |
Number of Pages |
XII, 388 p. |
Other physical details |
online resource. |
490 1# - SERIES STATEMENT |
Series statement |
Lecture Notes in Computer Science, |
505 0# - FORMATTED CONTENTS NOTE |
Formatted contents note |
SAT: Past and Future -- Encodings of Problems in Effectively Propositional Logic -- Efficient Circuit to CNF Conversion -- Mapping CSP into Many-Valued SAT -- Circuit Based Encoding of CNF Formula -- Breaking Symmetries in SAT Matrix Models -- Partial Max-SAT Solvers with Clause Learning -- MiniMaxSat: A New Weighted Max-SAT Solver -- Solving Multi-objective Pseudo-Boolean Problems -- Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities -- Horn Upper Bounds and Renaming -- Matched Formulas and Backdoor Sets -- Short XORs for Model Counting: From Theory to Practice -- Variable Dependency in Local Search: Prevention Is Better Than Cure -- Combining Adaptive Noise and Look-Ahead in Local Search for SAT -- From Idempotent Generalized Boolean Assignments to Multi-bit Search -- Satisfiability with Exponential Families -- Formalizing Dangerous SAT Encodings -- Algorithms for Variable-Weighted 2-SAT and Dual Problems -- On the Boolean Connectivity Problem for Horn Relations -- A First Step Towards a Unified Proof Checker for QBF -- Dynamically Partitioning for Solving QBF -- Backdoor Sets of Quantified Boolean Formulas -- Bounded Universal Expansion for Preprocessing QBF -- Effective Incorporation of Double Look-Ahead Procedures -- Applying Logic Synthesis for Speeding Up SAT -- Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver -- A Lightweight Component Caching Scheme for Satisfiability Solvers -- Minimum 2CNF Resolution Refutations in Polynomial Time -- Polynomial Time SAT Decision for Complementation-Invariant Clause-Sets, and Sign-non-Singular Matrices -- Verifying Propositional Unsatisfiability: Pitfalls to Avoid -- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories -- SAT Solving for Termination Analysis with Polynomial Interpretations -- Fault Localization and Correction with QBF -- Sensor Deployment for Failure Diagnosis in Networked Aerial Robots: A Satisfiability-Based Approach -- Inversion Attacks on Secure Hash Functions Using sat Solvers. |
520 ## - SUMMARY, ETC. |
Summary, etc |
This volume contains the papers presented at SAT 2007: 10th International Conference on Theory and Applications of Satis?ability Testing. The International Conferences on Theory and Applications of Satis?ability Testing (SAT) originated in 1996 as a series of workshops “on Satis?ability.” By the third meeting in 2000, the workshop had attracted a mix of theorists and experimentalists whose common interest was the enhancement of our basic understanding of the theoretical underpinnings of the Satis?ability problem as well as the development of scalable algorithms for its solution in a wide range of application domains. In 2002 a competition of SAT solvers was inaugurated to spur further algorithmic and implementation developments, and to create an eclectic collection of benchmarks. The competition—expanded in subsequent years to include pseudo Boolean, QBF, and MAX-SAT solvers—has become an integralpartofthesemeetings,addinganelementofexcitementandanticipation. Theinterplaybetweentheoryandapplication,aswellastheincreasedinterestin Satis?abilityfromawider communityofresearchers,ledtothe naturalevolution of these initial workshops into the current conference format. The annual SAT conference is now universally recognized as “the venue” for publishing the latest advances in SAT research. |
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Computer science. |
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Operating systems (Computers). |
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Computer software. |
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Electronic data processing. |
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Artificial intelligence. |
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Logic, Symbolic and mathematical. |
650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Computer Science. |
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Mathematical Logic and Formal Languages. |
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Algorithm Analysis and Problem Complexity. |
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Operating Systems. |
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Numeric Computing. |
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Artificial Intelligence (incl. Robotics). |
650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
Topical Term |
Mathematical Logic and Foundations. |
700 1# - ADDED ENTRY--PERSONAL NAME |
Personal name |
Marques-Silva, João. |
700 1# - ADDED ENTRY--PERSONAL NAME |
Personal name |
Sakallah, Karem A. |
856 40 - ELECTRONIC LOCATION AND ACCESS |
Uniform Resource Identifier |
http://dx.doi.org/10.1007/978-3-540-72788-0 |
942 ## - ADDED ENTRY ELEMENTS (KOHA) |
Koha item type |
E-BOOKS |
264 #1 - |
-- |
Berlin, Heidelberg : |
-- |
Springer Berlin Heidelberg, |
-- |
2007. |
336 ## - |
-- |
text |
-- |
txt |
-- |
rdacontent |
337 ## - |
-- |
computer |
-- |
c |
-- |
rdamedia |
338 ## - |
-- |
online resource |
-- |
cr |
-- |
rdacarrier |
347 ## - |
-- |
text file |
-- |
PDF |
-- |
rda |
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
-- |
0302-9743 ; |