Theory and applications of satisfiability testing -- SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings /: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. (2016)

• Record Type: Book
• Other Titles: SAT 2016
• Further Information: Note: Nadia Creignou, Daniel Le Berre (eds.).
• Editors: Creignou, Nadia; Le Berre, Daniel
• Other Names: SAT (Conference), 19th
• 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.
• Publisher Details: Switzerland : Springer
• Publication Date: 2016
• Extent: 1 online resource (xxiv, 564 pages), illustrations
• Subjects: 005.1; Computer science; Computer algorithms -- Congresses; Computer software -- Verification -- Congresses; Information theory; Artificial intelligence; Software engineering; Computer algorithms; Computer software -- Verification; Computers -- Intelligence (AI) & Semantics; Computers -- Data Processing; Computers -- Software Development & Engineering -- General; Artificial intelligence; Mathematical theory of computation; Software Engineering; Computers -- Computer Science; Computer science; Electronic books; Conference papers and proceedings; Electronic books
• Languages: English
• ISBNs: 9783319409702; 3319409700
• Related ISBNs: 9783319409696
• Notes: Note: Includes bibliographical references and author index.; Note: Online resource; title from PDF title page (SpringerLink, viewed June 14, 2016).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.