Theory and applications of satisfiability testing – SAT 2020. 23rd international conference, Alghero, Italy, July 3–10, 2020. Proceedings. (English) Zbl 1457.68014

Lecture Notes in Computer Science 12178. Cham: Springer (ISBN 978-3-030-51824-0/pbk; 978-3-030-51825-7/ebook). xi, 538 p. (2020).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1428.68027].
Indexed articles:
Chew, Leroy; Heule, Marijn J. H., Sorting parity encodings by reusing variables, 1-10 [Zbl 07331008]
Vallade, Vincent; Le Frioux, Ludovic; Baarir, Souheib; Sopena, Julien; Ganesh, Vijay; Kordon, Fabrice, Community and LBD-based clause sharing policy for parallel SAT solving, 11-27 [Zbl 07331009]
Feng, Nick; Bacchus, Fahiem, Clause size reduction with all-UIP learning, 28-45 [Zbl 07331010]
Hickey, Randy; Bacchus, Fahiem, Trail saving on backtrack, 46-61 [Zbl 07331011]
Möhle, Sibylle; Sebastiani, Roberto; Biere, Armin, Four flavors of entailment, 62-71 [Zbl 07331012]
Shaw, Arijit; Meel, Kuldeep S., Designing new phase selection heuristics, 72-88 [Zbl 07331013]
Lorenz, Jan-Hendrik; Wörz, Florian, On the effect of learned clauses on stochastic local search, 89-106 [Zbl 07331014]
Audemard, Gilles; Paulevé, Loïc; Simon, Laurent, SAT heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers, 107-113 [Zbl 07331015]
Heisinger, Maximilian; Fleury, Mathias; Biere, Armin, Distributed cube and conquer with Paracooba, 114-122 [Zbl 07331016]
Nabeshima, Hidetomo; Inoue, Katsumi, Reproducible efficient parallel SAT solving, 123-138 [Zbl 07331017]
Kochemazov, Stepan, Improving implementation of SAT competitions 2017–2019 winners, 139-148 [Zbl 07331018]
Mull, Nathan; Pang, Shuo; Razborov, Alexander, On CDCL-based proof systems with the ordered decision strategy, 149-165 [Zbl 07331019]
Bonet, Maria Luisa; Levy, Jordi, Equivalence between systems stronger than resolution, 166-181 [Zbl 07331020]
Vinyals, Marc; Elffers, Jan; Johannsen, Jan; Nordström, Jakob, Simplified and improved separations between regular and general resolution by lifting, 182-200 [Zbl 07331021]
Yolcu, Emre; Wu, Xinyu; Heule, Marijn J. H., Mycielski graphs and PR proofs, 201-217 [Zbl 07331022]
Larrosa, Javier; Rollon, Emma, Towards a better understanding of (partial weighted) MaxSAT proof systems, 218-232 [Zbl 07331023]
Li, Chunxiao; Fleming, Noah; Vinyals, Marc; Pitassi, Toniann; Ganesh, Vijay, Towards a complexity-theoretic understanding of restarts in SAT solvers, 233-249 [Zbl 07331024]
Agrawal, Durgesh; Bhavishya; Meel, Kuldeep S., On the sparsity of XORs in approximate model counting, 250-266 [Zbl 07331025]
Slivovsky, Friedrich; Szeider, Stefan, A faster algorithm for propositional model counting parameterized by incidence treewidth, 267-276 [Zbl 07331026]
Berg, Jeremias; Bacchus, Fahiem; Poole, Alex, Abstract cores in implicit hitting set MaxSat solving, 277-294 [Zbl 07331027]
Filmus, Yuval; Mahajan, Meena; Sood, Gaurav; Vinyals, Marc, MaxSAT resolution and subcube sums, 295-311 [Zbl 07331028]
de Colnet, Alexis, A lower bound on DNNF encodings of pseudo-Boolean constraints, 312-321 [Zbl 07331029]
Le Berre, Daniel; Marquis, Pierre; Wallon, Romain, On weakening strategies for PB solvers, 322-331 [Zbl 07331030]
Mencía, Carlos; Marques-Silva, Joao, Reasoning about strong inconsistency in ASP, 332-342 [Zbl 07331031]
Hecher, Markus; Thier, Patrick; Woltran, Stefan, Taming high treewidth with abstraction, nested dynamic programming, and database technology, 343-360 [Zbl 07331032]
Seed, Thomas; King, Andy; Evans, Neil, Reducing bit-vector polynomials to SAT using Gröbner bases, 361-377 [Zbl 07331033]
Jonáš, Martin; Strejček, Jan, Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions, 378-393 [Zbl 07331034]
Beyersdorff, Olaf; Blinkhorn, Joshua; Peitl, Tomáš, Strong (D)QBF dependency schemes via tautology-free resolution paths, 394-411 [Zbl 07331035]
Shukla, Ankit; Slivovsky, Friedrich; Szeider, Stefan, Short Q-resolution proofs with homomorphisms, 412-428 [Zbl 07331036]
Schlaipfer, Matthias; Slivovsky, Friedrich; Weissenbacher, Georg; Zuleger, Florian, Multi-linear strategy extraction for QBF expansion proofs via local soundness, 429-446 [Zbl 07331037]
Mayer-Eichberger, Valentin; Saffidine, Abdallah, Positional games and QBF: the corrective encoding, 447-463 [Zbl 07331038]
Anderson, Matthew; Ji, Zongliang; Xu, Anthony Yang, Matrix multiplication: verifying strong uniquely solvable puzzles, 464-480 [Zbl 07331039]
Češka, Milan; Matyáš, Jiří; Mrazek, Vojtech; Vojnar, Tomáš, Satisfiability solving meets evolutionary optimisation in designing approximate circuits, 481-491 [Zbl 07331040]
Ehlers, Rüdiger; Treutler, Kai; Wesling, Volker, SAT solving with fragmented Hamiltonian path constraints for wire arc additive manufacturing, 492-500 [Zbl 07331041]
Janota, Mikoláš; Morgado, António, SAT-based encodings for optimal decision trees with explicit paths, 501-518 [Zbl 07331042]
Karpiński, Michał; Piotrów, Marek, Incremental encoding of pseudo-Boolean goal functions based on comparator networks, 519-535 [Zbl 07331043]


68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68Q25 Analysis of algorithms and problem complexity
68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
00B25 Proceedings of conferences of miscellaneous specific interest


Zbl 1428.68027
Full Text: DOI