Site Overlay

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