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 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. .

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. .