000 05700nam a22006375i 4500
001 978-3-030-51825-7
003 DE-He213
005 20240730170508.0
007 cr nn 008mamaa
008 200630s2020 sz | s |||| 0|eng d
020 _a9783030518257
_9978-3-030-51825-7
024 7 _a10.1007/978-3-030-51825-7
_2doi
050 4 _aQA75.5-76.95
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a004.0151
_223
245 1 0 _aTheory and Applications of Satisfiability Testing - SAT 2020
_h[electronic resource] :
_b23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings /
_cedited by Luca Pulina, Martina Seidl.
250 _a1st ed. 2020.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2020.
300 _aXI, 538 p. 271 illus., 70 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v12178
505 0 _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 Sparsityof 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 _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. .
650 0 _aComputer science.
_99832
650 0 _aComputer engineering.
_910164
650 0 _aComputer networks .
_931572
650 0 _aMicroprogramming .
_932081
650 0 _aNumerical analysis.
_94603
650 0 _aLogic programming.
_92730
650 0 _aSoftware engineering.
_94138
650 1 4 _aTheory of Computation.
_993958
650 2 4 _aComputer Engineering and Networks.
_993960
650 2 4 _aControl Structures and Microprogramming.
_932083
650 2 4 _aNumerical Analysis.
_94603
650 2 4 _aLogic in AI.
_933012
650 2 4 _aSoftware Engineering.
_94138
700 1 _aPulina, Luca.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_993963
700 1 _aSeidl, Martina.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_993964
710 2 _aSpringerLink (Online service)
_993967
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783030518240
776 0 8 _iPrinted edition:
_z9783030518264
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v12178
_993968
856 4 0 _uhttps://doi.org/10.1007/978-3-030-51825-7
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c86997
_d86997