View in EDS PDF Full Text

Handbook of Satisfiability

Saved in:
Bibliographic Details
Title: Handbook of Satisfiability
Description: “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 and Computer Engineering at Carnegie Mellon University, winner of the 2007 A.M. Turing Award)
Authors: Armin Biere, Hans van Maaren, Toby Walsh
Resource Type: eBook.
Subjects: Computer algorithms--Congresses, Algebra, Boolean--Congresses, Propositional calculus--Congresses, Decision making--Congresses
Categories: COMPUTERS / Artificial Intelligence / General
Database: eBook Collection (EBSCOhost)
FullText Links:
  – Type: ebook-pdf
Text:
  Availability: 0
Header DbId: nlebk
DbLabel: eBook Collection (EBSCOhost)
An: 281413
RelevancyScore: 1025
AccessLevel: 6
PubType: eBook
PubTypeId: ebook
PreciseRelevancyScore: 1024.62744140625
IllustrationInfo
ImageInfo – Size: thumb
  Target: https://rps2images.ebscohost.com/rpsweb/othumb?id=NL$281413$PDF&s=r
– Size: medium
  Target: https://rps2images.ebscohost.com/rpsweb/othumb?id=NL$281413$PDF&s=d
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Handbook of Satisfiability
– Name: Abstract
  Label: Description
  Group: Ab
  Data: “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 and Computer Engineering at Carnegie Mellon University, winner of the 2007 A.M. Turing Award)
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Armin+Biere%22">Armin Biere</searchLink><br /><searchLink fieldCode="AR" term="%22Hans+van+Maaren%22">Hans van Maaren</searchLink><br /><searchLink fieldCode="AR" term="%22Toby+Walsh%22">Toby Walsh</searchLink>
– Name: TypePub
  Label: Resource Type
  Group: TypPub
  Data: eBook.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Computer+algorithms--Congresses%22">Computer algorithms--Congresses</searchLink><br /><searchLink fieldCode="DE" term="%22Algebra%2C+Boolean--Congresses%22">Algebra, Boolean--Congresses</searchLink><br /><searchLink fieldCode="DE" term="%22Propositional+calculus--Congresses%22">Propositional calculus--Congresses</searchLink><br /><searchLink fieldCode="DE" term="%22Decision+making--Congresses%22">Decision making--Congresses</searchLink>
– Name: SubjectBISAC
  Label: Categories
  Group: Su
  Data: <searchLink fieldCode="ZK" term="%22COMPUTERS+%2F+Artificial+Intelligence+%2F+General%22">COMPUTERS / Artificial Intelligence / General</searchLink>
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=nlebk&AN=281413
RecordInfo BibRecord:
  BibEntity:
    Classifications:
      – Code: 511.3
        Scheme: ddc
        Type: prePub
    Languages:
      – Code: eng
        Text: English
    Subjects:
      – SubjectFull: Computer algorithms--Congresses
        Type: general
      – SubjectFull: Algebra, Boolean--Congresses
        Type: general
      – SubjectFull: Propositional calculus--Congresses
        Type: general
      – SubjectFull: Decision making--Congresses
        Type: general
    Titles:
      – TitleFull: Handbook of Satisfiability
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Armin Biere
      – PersonEntity:
          Name:
            NameFull: Hans van Maaren
      – PersonEntity:
          Name:
            NameFull: Toby Walsh
      – PersonEntity:
          Name:
            NameFull: Armin Biere
      – PersonEntity:
          Name:
            NameFull: Hans van Maaren
      – PersonEntity:
          Name:
            NameFull: Toby Walsh
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 01
              Type: published
              Y: 2009
            – D: 04
              M: 02
              Type: profile
              Y: 2014
          Identifiers:
            – Type: isbn-print
              Value: 9781586039295
            – Type: isbn-electronic
              Value: 9781441616784
            – Type: isbn-electronic
              Value: 9781607503767
          Numbering:
            – Type: volume
              Value: 00185
          Titles:
            – TitleFull: Handbook of Satisfiability
              Type: main
ResultId 1