001437922 000__ 06523cam\a2200721\i\4500
001437922 001__ 1437922
001437922 003__ OCoLC
001437922 005__ 20230309004239.0
001437922 006__ m\\\\\o\\d\\\\\\\\
001437922 007__ cr\cn\nnnunnun
001437922 008__ 210708s2021\\\\sz\a\\\\o\\\\\101\0\eng\d
001437922 019__ $$a1266810919
001437922 020__ $$a9783030802233$$q(electronic bk.)
001437922 020__ $$a303080223X$$q(electronic bk.)
001437922 020__ $$z9783030802226$$q(print)
001437922 0247_ $$a10.1007/978-3-030-80223-3$$2doi
001437922 035__ $$aSP(OCoLC)1259439469
001437922 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dOCLCO$$dEBLCP$$dOCLCF$$dDCT$$dOCLCQ$$dCOM$$dOCLCO$$dOCLCQ
001437922 049__ $$aISEA
001437922 050_4 $$aQA76.9.A43
001437922 08204 $$a005.1$$223
001437922 1112_ $$aSAT (Conference)$$n(24th :$$d2021 :$$cBarcelona, Spain ; Online)
001437922 24510 $$aTheory and applications of satisfiability testing -- SAT 2021 :$$b24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings /$$cChu-Min Li, Felip Manyà (eds.).
001437922 2463_ $$aSAT 2021
001437922 264_1 $$aCham, Switzerland :$$bSpringer,$$c[2021]
001437922 300__ $$a1 online resource (xi, 564 pages) :$$billustrations (some color)
001437922 336__ $$atext$$btxt$$2rdacontent
001437922 337__ $$acomputer$$bc$$2rdamedia
001437922 338__ $$aonline resource$$bcr$$2rdacarrier
001437922 347__ $$atext file
001437922 347__ $$bPDF
001437922 4901_ $$aLecture notes in computer science ;$$v12831
001437922 4901_ $$aLNCS sublibrary, SL 1, Theoretical computer science and general issues
001437922 500__ $$a"Because of the COVID-19 pandemic, SAT 2021 followed a hybrid format, with both in-person and virtual participation options."--Preface
001437922 500__ $$aIncludes author index.
001437922 5050_ $$aIntro -- Preface -- Organization -- Contents -- OptiLog: A Framework for SAT-based Systems -- 1 Introduction -- 2 OptiLog Framework Architecture -- 2.1 Formula Module -- 2.2 SAT Solver Module -- 2.3 PB Encoder Module -- 2.4 Automatic Configuration (AC) Module -- 2.5 Adding SAT Solvers to OptiLog Through iSAT Interface -- 3 Example: The Linear MaxSAT Algorithm with OptiLog -- 4 Conclusions and Future Work -- References -- PyDGGA: Distributed GGA for Automatic Configuration -- 1 Introduction -- 2 Preliminaries -- 3 PyDGGA -- 3.1 Distributed Architecture -- 3.2 Simulation
001437922 5058_ $$a3.3 Scheduling and Canceling -- 3.4 Instance Selection -- 3.5 Elite Mini-Tournament -- 3.6 Other Tool Enhancements -- 4 Using PyDGGA -- 5 Experiments with SAT -- 6 Conclusions and Future Work -- References -- QBFFam: A Tool for Generating QBF Families from Proof Complexity -- 1 Introduction -- 2 Related Work -- 3 Formula Families -- 4 Case Study -- 5 Conclusion -- References -- Davis and Putnam Meet Henkin: Solving DQBF with Resolution -- 1 Introduction -- 2 Preliminaries -- 3 Davis-Putnam Resolution for H-Form DQBF -- 3.1 Strategy Operations -- 3.2 Definition of the Construction
001437922 5058_ $$a3.3 Correctness and Completeness -- 3.4 Representing Strategies -- 4 NEXP-completeness of CNF H-Form DQBF -- 5 Conclusion -- References -- Lower Bounds for QCDCL via Formula Gauge -- 1 Introduction -- 2 Preliminaries -- 3 QCDCL as a Formal Proof System -- 4 Quasi Level-Ordered Proofs -- 5 A Lower Bound Technique via Gauge -- 6 Applications of the Lower Bound Technique -- 7 Conclusion -- References -- Deep Cooperation of CDCL and Local Search for SAT -- 1 Introduction -- 2 Preliminaries -- 2.1 Preliminary Definitions and Notations -- 2.2 CDCL Solvers -- 2.3 Local Search Solvers
001437922 5058_ $$a2.4 Experiment Preliminaries -- 3 Exploring Promising Branches by Local Search -- 4 Phase Resetting with Local Search Assignments -- 5 Branching with Conflict Frequency in Local Search -- 6 Experiments -- 7 Related Works -- 8 Conclusions -- References -- Hash-Based Preprocessing and Inprocessing Techniques in SAT Solvers -- 1 Introduction -- 2 Preliminaries -- 3 Hash-Based Methods -- 4 Probabilistic Analysis -- 5 Evaluation -- 6 Conclusions -- References -- Hardness and Optimality in QBF Proof Systems Modulo NP -- 1 Introduction -- 1.1 Organisation -- 2 Preliminaries -- 2.1 Proof Complexity
001437922 5058_ $$a2.2 Propositional Logic -- 2.3 Quantified Boolean Formulas -- 3 Simulations with Extension Variables -- 4 Extended Q-Res Modulo NP -- 5 Weaker QBF Systems -- 6 Conclusion -- References -- Characterizing Tseitin-Formulas with Short Regular Resolution Refutations -- 1 Introduction -- 2 Preliminaries -- 3 Reduction from Unsatisfiable to Satisfiable Formulas -- 3.1 Well-Structured Branching Programs for SearchVertex(G, c) -- 3.2 Constructing DNNF from Well-Structured Branching Programs -- 4 Adversarial Rectangle Bounds -- 5 Splitting Parity Constraints
001437922 506__ $$aAccess limited to authorized users.
001437922 520__ $$aThis book constitutes the proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing, SAT 2021, which took place in Barcelona, Spain, in July 2021. The 37 full papers presented in this volume were carefully reviewed and selected from 73 submissions. They deal with theory and applications of the propositional satisfiability problem, broadly construed. Aside from plain propositional satisfiability, the scope of the meeting includes Boolean optimization, including MaxSAT and pseudo-Boolean (PB) constraints, quantified Boolean formulas (QBF), satisfiability modulo theories (SMT), and constraint programming (CP) for problems with clear connections to Boolean reasoning.
001437922 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed July 8, 2021).
001437922 650_0 $$aComputer algorithms$$vCongresses.
001437922 650_0 $$aComputer software$$xVerification$$vCongresses.
001437922 650_6 $$aAlgorithmes$$vCongrès.
001437922 650_6 $$aLogiciels$$xVérification$$vCongrès.
001437922 655_7 $$aConference papers and proceedings.$$2fast$$0(OCoLC)fst01423772
001437922 655_7 $$aConference papers and proceedings.$$2lcgft
001437922 655_7 $$aActes de congrès.$$2rvmgf
001437922 655_0 $$aElectronic books.
001437922 7001_ $$aLi, Chu-Min,$$eeditor$$0(orcid)0000-0002-6886-8434$$1https://orcid.org/0000-0002-6886-8434
001437922 7001_ $$aManyà, Felip,$$eeditor.$$1https://orcid.org/0000-0002-8366-1458
001437922 77608 $$iPrint version: $$z9783030802226
001437922 77608 $$iPrint version: $$z9783030802240
001437922 830_0 $$aLecture notes in computer science ;$$v12831.
001437922 830_0 $$aLNCS sublibrary.$$nSL 1,$$pTheoretical computer science and general issues.
001437922 852__ $$bebk
001437922 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-3-030-80223-3$$zOnline Access$$91397441.1
001437922 909CO $$ooai:library.usi.edu:1437922$$pGLOBAL_SET
001437922 980__ $$aBIB
001437922 980__ $$aEBOOK
001437922 982__ $$aEbook
001437922 983__ $$aOnline
001437922 994__ $$a92$$bISE