Abstract is missing.
- Sorting Parity Encodings by Reusing VariablesLeroy Chew, Marijn J. H. Heule. 1-10 [doi]
- Community and LBD-Based Clause Sharing Policy for Parallel SAT SolvingVincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Vijay Ganesh, Fabrice Kordon. 11-27 [doi]
- Clause Size Reduction with all-UIP LearningNick Feng, Fahiem Bacchus. 28-45 [doi]
- Trail Saving on BacktrackRandy Hickey, Fahiem Bacchus. 46-61 [doi]
- Four Flavors of EntailmentSibylle Möhle, Roberto Sebastiani, Armin Biere. 62-71 [doi]
- Designing New Phase Selection HeuristicsArijit Shaw, Kuldeep S. Meel. 72-88 [doi]
- On the Effect of Learned Clauses on Stochastic Local SearchJan-Hendrik Lorenz, Florian Wörz. 89-106 [doi]
- SAT Heritage: A Community-Driven Effort for Archiving, Building and Running More Than Thousand SAT SolversGilles Audemard, Loïc Paulevé, Laurent Simon. 107-113 [doi]
- Distributed Cube and Conquer with ParacoobaMaximilian Heisinger, Mathias Fleury, Armin Biere. 114-122 [doi]
- Reproducible Efficient Parallel SAT SolvingHidetomo Nabeshima, Katsumi Inoue. 123-138 [doi]
- Improving Implementation of SAT Competitions 2017-2019 WinnersStepan Kochemazov. 139-148 [doi]
- On CDCL-Based Proof Systems with the Ordered Decision StrategyNathan Mull, Shuo Pang, Alexander A. Razborov. 149-165 [doi]
- Equivalence Between Systems Stronger Than ResolutionMaria Luisa Bonet, Jordi Levy. 166-181 [doi]
- Simplified and Improved Separations Between Regular and General Resolution by LiftingMarc Vinyals, Jan Elffers, Jan Johannsen, Jakob Nordström. 182-200 [doi]
- Mycielski Graphs and $\mathrm {PR}$ ProofsEmre Yolcu, Xinyu Wu, Marijn J. H. Heule. 201-217 [doi]
- Towards a Better Understanding of (Partial Weighted) MaxSAT Proof SystemsJavier Larrosa, Emma Rollon. 218-232 [doi]
- Towards a Complexity-Theoretic Understanding of Restarts in SAT SolversChunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, Vijay Ganesh. 233-249 [doi]
- On the Sparsity of XORs in Approximate Model CountingDurgesh Agrawal, Bhavishya, Kuldeep S. Meel. 250-266 [doi]
- A Faster Algorithm for Propositional Model Counting Parameterized by Incidence TreewidthFriedrich Slivovsky, Stefan Szeider. 267-276 [doi]
- Abstract Cores in Implicit Hitting Set MaxSat SolvingJeremias Berg, Fahiem Bacchus, Alex Poole. 277-294 [doi]
- MaxSAT Resolution and Subcube SumsYuval Filmus, Meena Mahajan, Gaurav Sood, Marc Vinyals. 295-311 [doi]
- A Lower Bound on DNNF Encodings of Pseudo-Boolean ConstraintsAlexis de Colnet. 312-321 [doi]
- On Weakening Strategies for PB SolversDaniel Le Berre, Pierre Marquis, Romain Wallon. 322-331 [doi]
- Reasoning About Strong Inconsistency in ASPCarlos Mencía, João Marques-Silva 0001. 332-342 [doi]
- Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database TechnologyMarkus Hecher, Patrick Thier, Stefan Woltran. 343-360 [doi]
- Reducing Bit-Vector Polynomials to SAT Using Gröbner BasesThomas Seed, Andy King, Neil Evans. 361-377 [doi]
- Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and ExtensionsMartin Jonás, Jan Strejcek. 378-393 [doi]
- Strong (D)QBF Dependency Schemes via Tautology-Free Resolution PathsOlaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl. 394-411 [doi]
- Short Q-Resolution Proofs with HomomorphismsAnkit Shukla, Friedrich Slivovsky, Stefan Szeider. 412-428 [doi]
- Multi-linear Strategy Extraction for QBF Expansion Proofs via Local SoundnessMatthias Schlaipfer, Friedrich Slivovsky, Georg Weissenbacher, Florian Zuleger. 429-446 [doi]
- Positional Games and QBF: The Corrective EncodingValentin Mayer-Eichberger, Abdallah Saffidine. 447-463 [doi]
- Matrix Multiplication: Verifying Strong Uniquely Solvable PuzzlesMatthew Anderson, Zongliang Ji, Anthony Yang Xu. 464-480 [doi]
- Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate CircuitsMilan Ceska 0001, Jirí Matyás, Vojtech Mrazek, Tomás Vojnar. 481-491 [doi]
- SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive ManufacturingRüdiger Ehlers, Kai Treutler, Volker Wesling. 492-500 [doi]
- SAT-Based Encodings for Optimal Decision Trees with Explicit PathsMikolás Janota, António Morgado. 501-518 [doi]
- Incremental Encoding of Pseudo-Boolean Goal Functions Based on Comparator NetworksMichal Karpinski, Marek Piotrów. 519-535 [doi]