Coverart for item
The Resource Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Nadia Creignou, Daniel Le Berre (eds.), (electronic book)

Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Nadia Creignou, Daniel Le Berre (eds.), (electronic book)

Label
Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
Title
Theory and applications of satisfiability testing -- SAT 2016
Title remainder
19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
Statement of responsibility
Nadia Creignou, Daniel Le Berre (eds.)
Title variation
SAT 2016
Creator
Contributor
Editor
Subject
Genre
Language
eng
Summary
This book constitutes the refereed proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, held in Bordeaux, France, in July 2016. The 31 regular papers, 5 tool papers presented together with 3 invited talks were carefully reviewed and selected from 70 submissions. The papers address different aspects of SAT, including complexity, satisfiability solving, satisfiability applications, satisfiability modulop theory, beyond SAT, quantified Boolean formula, and dependency QBF.
Member of
Cataloging source
GW5XE
Dewey number
005.1
Illustrations
illustrations
Index
index present
LC call number
QA76.9.A43
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2016
http://bibfra.me/vocab/lite/meetingName
SAT (Conference)
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorName
  • Creignou, Nadia
  • Le Berre, Daniel
Series statement
  • Lecture notes in computer science,
  • LNCS sublibrary. SL 1, Theoretical computer science and general issues
Series volume
9710
http://library.link/vocab/subjectName
  • Computer algorithms
  • Computer software
Label
Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Nadia Creignou, Daniel Le Berre (eds.), (electronic book)
Instantiates
Publication
Note
International conference proceedings
Antecedent source
unknown
Bibliography note
Includes bibliographical references and author index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Parameterized Compilation Lower Bounds for Restricted CNF-formulas -- Satisfiability via Smooth Pictures -- Solution-Graphs of Boolean Formulas and Isomorphism -- Strong Backdoors for Default Logic -- The Normalized Autocorrelation Length of Max r-Sat Converges in Probability to (1-1/2=r)/r -- Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle -- Extreme Cases in SAT Problems -- Improved Static Symmetry Breaking for SAT -- Learning Rate Based Branching Heuristic for SAT Solvers -- On the Hardness of SAT with Community Structure -- Trade-offs between Time and Memory in a Tighter Model of CDCL SAT Solvers -- A SAT Approach to Branch Width -- Computing Maximum Unavoidable Subgraphs Using SAT Solvers -- Heuristic NPN Classification for Large Functions Using AIGs and LEXSAT -- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer -- Deciding Bit-Vector Formulas with mcSAT -- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams -- Speeding Up the Constraint-Based Method in Difference Logic -- Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers -- Finding Finite Models in Multi-Sorted First Order Logic -- MCS Extraction with Sublinear Oracle Queries -- Predicate Elimination for Preprocessing in First-Order Theorem Proving -- Quantified Boolean Formula Incremental Determinization -- Non-prenex QBF Solving using Abstraction -- On Q-Resolution and CDCL QBF Solving -- On Stronger Calculi for QBFs -- Q-Resolution with Generalized Axioms -- 2QBF: Challenges and Solutions -- Dependency Schemes for DQBF -- Lifting QBF Resolution Calculi to DQBF -- Long Distance Q-Resolution with Dependency Schemes -- BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies -- HordeQBF: A Modular and Massively Parallel QBF Solver -- LMHS: A SAT-IP Hybrid MaxSAT Solver -- OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing -- SpyBug: Automated Bug Detection in the Con_guration Space of SAT Solvers.
Control code
SPR951904034
Dimensions
unknown
Extent
1 online resource (xxiv, 564 pages)
File format
unknown
Form of item
online
Isbn
9783319409702
Level of compression
unknown
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/978-3-319-40970-2
Other physical details
illustrations.
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote
Label
Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Nadia Creignou, Daniel Le Berre (eds.), (electronic book)
Publication
Note
International conference proceedings
Antecedent source
unknown
Bibliography note
Includes bibliographical references and author index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Parameterized Compilation Lower Bounds for Restricted CNF-formulas -- Satisfiability via Smooth Pictures -- Solution-Graphs of Boolean Formulas and Isomorphism -- Strong Backdoors for Default Logic -- The Normalized Autocorrelation Length of Max r-Sat Converges in Probability to (1-1/2=r)/r -- Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle -- Extreme Cases in SAT Problems -- Improved Static Symmetry Breaking for SAT -- Learning Rate Based Branching Heuristic for SAT Solvers -- On the Hardness of SAT with Community Structure -- Trade-offs between Time and Memory in a Tighter Model of CDCL SAT Solvers -- A SAT Approach to Branch Width -- Computing Maximum Unavoidable Subgraphs Using SAT Solvers -- Heuristic NPN Classification for Large Functions Using AIGs and LEXSAT -- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer -- Deciding Bit-Vector Formulas with mcSAT -- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams -- Speeding Up the Constraint-Based Method in Difference Logic -- Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers -- Finding Finite Models in Multi-Sorted First Order Logic -- MCS Extraction with Sublinear Oracle Queries -- Predicate Elimination for Preprocessing in First-Order Theorem Proving -- Quantified Boolean Formula Incremental Determinization -- Non-prenex QBF Solving using Abstraction -- On Q-Resolution and CDCL QBF Solving -- On Stronger Calculi for QBFs -- Q-Resolution with Generalized Axioms -- 2QBF: Challenges and Solutions -- Dependency Schemes for DQBF -- Lifting QBF Resolution Calculi to DQBF -- Long Distance Q-Resolution with Dependency Schemes -- BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies -- HordeQBF: A Modular and Massively Parallel QBF Solver -- LMHS: A SAT-IP Hybrid MaxSAT Solver -- OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing -- SpyBug: Automated Bug Detection in the Con_guration Space of SAT Solvers.
Control code
SPR951904034
Dimensions
unknown
Extent
1 online resource (xxiv, 564 pages)
File format
unknown
Form of item
online
Isbn
9783319409702
Level of compression
unknown
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/978-3-319-40970-2
Other physical details
illustrations.
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote

Library Locations

Processing Feedback ...