國立虎尾科技大學 |

Theory and Applications of Satisfiability Testing – SAT 2020 = 23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings /

Record Type:	Language materials, printed : Monograph/item
Title/Author:	Theory and Applications of Satisfiability Testing – SAT 2020/ edited by Luca Pulina, Martina Seidl.
Reminder of title:	23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings /
other author:	Pulina, Luca.
Description:	XI, 538 p. 271 illus., 70 illus. in color.online resource. :
Contained By:	Springer Nature eBook
Subject:	Computers. -
Online resource:	https://doi.org/10.1007/978-3-030-51825-7
ISBN:	9783030518257

Theory and Applications of Satisfiability Testing – SAT 2020 = 23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings /
Theory and Applications of Satisfiability Testing – SAT 202023rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings /[electronic resource] :edited by Luca Pulina, Martina Seidl. - 1st ed. 2020. - XI, 538 p. 271 illus., 70 illus. in color.online resource. - Theoretical Computer Science and General Issues ;12178. - Theoretical Computer Science and General Issues ;9163.

Sorting Parity Encodings by Reusing Variables -- Community and LBD-based Clause Sharing Policy for Parallel SAT Solving -- Clause size reduction with all-UIP Learning -- Trail Saving on Backtrack -- Four Flavors of Entailment -- Designing New Phase Selection Heuristics -- On the Effect of Learned Clauses on Stochastic Local Search -- SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers -- Distributed Cube and Conquer with Paracooba -- Reproducible E cient Parallel SAT Solving -- Improving Implementation of SAT Competitions 2017-2019 Winners -- On CDCL-based Proof Systems with the Ordered Decision Strategy -- Equivalence Between Systems Stronger Than Resolution -- Simplified and Improved Separations Between Regular and General Resolution by Lifting -- Mycielski graphs and PR proofs -- Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems -- Towards a Complexity-theoretic Understanding of Restarts in SAT solvers -- On the Sparsity of XORs in Approximate Model Counting -- A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth -- Abstract Cores in Implicit Hitting Set MaxSat Solving -- MaxSAT Resolution and SubCube Sums -- A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints -- On Weakening Strategies for PB Solvers -- Reasoning About Strong Inconsistency in ASP -- Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology -- Reducing Bit-Vector Polynomials to SAT using Groebner Bases -- Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions -- Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths -- Short Q-Resolution Proofs with Homomorphisms -- Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness -- Positional Games and QBF: The Corrective Encoding -- Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles -- Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits -- SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing -- SAT-based Encodings for Optimal Decision Trees with Explicit Paths -- Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks. .

This book constitutes the proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing, SAT 2020, which was planned to take place in Alghero, Italy, during July 5-9, 2020. Due to the coronavirus COVID-19 pandemic, the conference was held virtually. The 25 full, 9 short, and 2 tool papers presented in this volume were carefully reviewed and selected from 69 submissions. They deal with SAT interpreted in a broad sense, including theoretical advances (such as exact algorithms, proof complexity, and other complexity issues), practical search algorithms, knowledge compilation, implementation-level details of SAT solvers and SAT-based systems, problem encodings and reformulations, applications (including both novel application domains and improvements to existing approaches), as well as case studies and reports on findings based on rigorous experimentation. .

ISBN: 9783030518257

Standard No.: 10.1007/978-3-030-51825-7doiSubjects--Topical Terms:

565115
Computers.

LC Class. No.: QA75.5-76.95

Dewey Class. No.: 004.0151

Theory and Applications of Satisfiability Testing – SAT 2020 = 23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings /
LDR:04773nam a22004335i 4500 001 1024486
003 DE-He213
005 20200703163500.0
007 cr nn 008mamaa
008 210318s2020 gw | s |||| 0|eng d
020 $a 9783030518257 $9 978-3-030-51825-7
024 7 $a 10.1007/978-3-030-51825-7 $2 doi
035 $a 978-3-030-51825-7
050 4 $a QA75.5-76.95
050 4 $a QA76.63
072 7 $a UY $2 bicssc
072 7 $a COM014000 $2 bisacsh
072 7 $a UY $2 thema
072 7 $a UYA $2 thema
082 0 4 $a 004.0151 $2 23
245 1 0 $a Theory and Applications of Satisfiability Testing – SAT 2020 $h [electronic resource] : $b 23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings / $c edited by Luca Pulina, Martina Seidl.
250 $a 1st ed. 2020.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2020.
300 $a XI, 538 p. 271 illus., 70 illus. in color. $b online resource.
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
347 $a text file $b PDF $2 rda
490 1 $a Theoretical Computer Science and General Issues ; $v 12178
505 0 $a Sorting Parity Encodings by Reusing Variables -- Community and LBD-based Clause Sharing Policy for Parallel SAT Solving -- Clause size reduction with all-UIP Learning -- Trail Saving on Backtrack -- Four Flavors of Entailment -- Designing New Phase Selection Heuristics -- On the Effect of Learned Clauses on Stochastic Local Search -- SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers -- Distributed Cube and Conquer with Paracooba -- Reproducible E cient Parallel SAT Solving -- Improving Implementation of SAT Competitions 2017-2019 Winners -- On CDCL-based Proof Systems with the Ordered Decision Strategy -- Equivalence Between Systems Stronger Than Resolution -- Simplified and Improved Separations Between Regular and General Resolution by Lifting -- Mycielski graphs and PR proofs -- Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems -- Towards a Complexity-theoretic Understanding of Restarts in SAT solvers -- On the Sparsity of XORs in Approximate Model Counting -- A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth -- Abstract Cores in Implicit Hitting Set MaxSat Solving -- MaxSAT Resolution and SubCube Sums -- A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints -- On Weakening Strategies for PB Solvers -- Reasoning About Strong Inconsistency in ASP -- Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology -- Reducing Bit-Vector Polynomials to SAT using Groebner Bases -- Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions -- Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths -- Short Q-Resolution Proofs with Homomorphisms -- Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness -- Positional Games and QBF: The Corrective Encoding -- Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles -- Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits -- SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing -- SAT-based Encodings for Optimal Decision Trees with Explicit Paths -- Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks. .
520 $a This book constitutes the proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing, SAT 2020, which was planned to take place in Alghero, Italy, during July 5-9, 2020. Due to the coronavirus COVID-19 pandemic, the conference was held virtually. The 25 full, 9 short, and 2 tool papers presented in this volume were carefully reviewed and selected from 69 submissions. They deal with SAT interpreted in a broad sense, including theoretical advances (such as exact algorithms, proof complexity, and other complexity issues), practical search algorithms, knowledge compilation, implementation-level details of SAT solvers and SAT-based systems, problem encodings and reformulations, applications (including both novel application domains and improvements to existing approaches), as well as case studies and reports on findings based on rigorous experimentation. .
650 0 $a Computers. $3 565115
650 0 $a Computer organization. $3 596298
650 0 $a Microprogramming . $3 1257366
650 0 $a Numerical analysis. $3 527939
650 0 $a Artificial intelligence. $3 559380
650 0 $a Computer logic. $3 786340
650 0 $a Software engineering. $3 562952
650 1 4 $a Theory of Computation. $3 669322
650 2 4 $a Computer Systems Organization and Communication Networks. $3 669309
650 2 4 $a Control Structures and Microprogramming. $3 669788
650 2 4 $a Numeric Computing. $3 669943
650 2 4 $a Logic in AI. $3 1228083
650 2 4 $a Software Engineering. $3 669632
700 1 $a Pulina, Luca. $e editor. $1 https://orcid.org/0000-0003-0258-3222 $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1320645
700 1 $a Seidl, Martina. $4 edt $4 http://id.loc.gov/vocabulary/relators/edt $3 1066319
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783030518240
776 0 8 $i Printed edition: $z 9783030518264
830 0 $a Theoretical Computer Science and General Issues ; $v 9163 $3 1253524
856 4 0 $u https://doi.org/10.1007/978-3-030-51825-7
912 $a ZDB-2-SCS
912 $a ZDB-2-SXCS
912 $a ZDB-2-LNC
950 $a Computer Science (SpringerNature-11645)
950 $a Computer Science (R0) (SpringerNature-43710)