Accepted Papers

• Emre Yolcu, Xinyu Wu and Marijn Heule. Mycielski graphs and PR proofs
• Michał Karpiński and Marek Piotrów. Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks
• Marc Vinyals, Jan Elffers, Jan Johannsen and Jakob Nordstrom. Simplified and Improved Separations Between Regular and General Resolution by Lifting
• Thomas Seed, Andy King and Neil Evans. Reducing Bit-Vector Polynomials to SAT using Groebner Bases
• Nathan Mull, Shuo Pang and Alexander Razborov. On CDCL-based Proof Systems with the Ordered Decision Strategy
• Jan-Hendrik Lorenz and Florian Wörz. On the Effect of Learned Clauses on Stochastic Local Search
• Markus Hecher, Patrick Thier and Stefan Woltran. Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology
• Matthew Anderson, Zongliang Ji and Anthony Xu. Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles
• Sibylle Möhle, Roberto Sebastiani and Armin Biere. Four Flavors of Entailment
• Javier Larrosa and Emma Rollon. Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
• Friedrich Slivovsky and Stefan Szeider. A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
• Maximilian Heisinger, Mathias Fleury and Armin Biere. Distributed Cube and Conquer with Paracooba
• Leroy Chew and Marijn Heule. Sorting Parity Encodings by Reusing Variables
• Daniel Le Berre, Pierre Marquis and Romain Wallon. On Weakening Strategies for PB Solvers
• Alexis de Colnet. A lower bound on DNNF encodings of pseudo-Boolean constraints
• Hidetomo Nabeshima and Katsumi Inoue. Reproducible Efficient Parallel SAT Solving
• Olaf Beyersdorff, Joshua Blinkhorn and Tomáš Peitl. Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths
• Rüdiger Ehlers, Kai Treutler and Volker Wesling. SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing
  
• Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon and Vijay Ganesh. Community and LBD-based Clause Sharing Policy for Parallel SAT Solving
• Ankit Shukla, Friedrich Slivovsky and Stefan Szeider. Short Q-Resolution Proofs with Homomorphisms
• Milan Ceska, Jiri Matyas, Vojtech Mrazek and Tomas Vojnar. Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits
• Nick Feng and Fahiem Bacchus. Clause size reduction with all-UIP Learning
• Randy Hickey and Fahiem Bacchus. Trail Saving on Backtrack
• Durgesh Agrawal, Bhavishya, and Kuldeep S. Meel. On the Sparsity of XORs in Approximate Model Counting
• Maria Luisa Bonet and Jordi Levy. Equivalence Between Systems Stronger Than Resolution
• Jeremias Berg, Fahiem Bacchus and Alex Poole. Abstract Cores in Implicit Hitting Set MaxSat Solving
• Stepan Kochemazov. Improving implementations of SAT competitions 2017-2019 main track winners
• Arijit Shaw and Kuldeep S. Meel. Designing New Phase Selection Heuristics
• Mikolas Janota and António Morgado. SAT-based Encodings for Optimal Decision Trees with Explicit Paths
• Carlos Mencía and Joao Marques-Silva. Reasoning About Strong Inconsistency in ASP
• Matthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher and Florian Zuleger. Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness
• Gilles Audemard, Loïc Paulevé and Laurent Simon. SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers
• Valentin Mayer-Eichberger and Abdallah Saffidine. Positional Games and QBF: The Corrective Encoding
• Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi and Vijay Ganesh. Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
• Martin Jonáš and Jan Strejček. Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions
• Yuval Filmus, Meena Mahajan, Gaurav Sood and Marc Vinyals. MaxSAT Resolution and SubCube Sums