LEADER 05810nam 22007575 450 001 996418280803316 005 20230330060326.0 010 $a3-030-51825-6 024 7 $a10.1007/978-3-030-51825-7 035 $a(CKB)4100000011325823 035 $a(MiAaPQ)EBC6298669 035 $a(DE-He213)978-3-030-51825-7 035 $a(PPN)248595423 035 $a(EXLCZ)994100000011325823 100 $a20200630d2020 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aTheory and Applications of Satisfiability Testing ? SAT 2020$b[electronic resource] $e23rd International Conference, Alghero, Italy, July 3?10, 2020, Proceedings /$fedited by Luca Pulina, Martina Seidl 205 $a1st ed. 2020. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2020. 215 $a1 online resource (xi, 538 pages) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12178 300 $aIncludes index. 311 $a3-030-51824-8 327 $aSorting 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. . 330 $aThis 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. . 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v12178 606 $aComputer science 606 $aComputer engineering 606 $aComputer networks 606 $aMicroprogramming 606 $aNumerical analysis 606 $aLogic programming 606 $aSoftware engineering 606 $aTheory of Computation 606 $aComputer Engineering and Networks 606 $aControl Structures and Microprogramming 606 $aNumerical Analysis 606 $aLogic in AI 606 $aSoftware Engineering 615 0$aComputer science. 615 0$aComputer engineering. 615 0$aComputer networks. 615 0$aMicroprogramming. 615 0$aNumerical analysis. 615 0$aLogic programming. 615 0$aSoftware engineering. 615 14$aTheory of Computation. 615 24$aComputer Engineering and Networks. 615 24$aControl Structures and Microprogramming. 615 24$aNumerical Analysis. 615 24$aLogic in AI. 615 24$aSoftware Engineering. 676 $a005.1 702 $aPulina$b Luca$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSeidl$b Martina$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996418280803316 996 $aTheory and Applications of Satisfiability Testing ? SAT 2020$92241075 997 $aUNISA