| Authors | Title | Paper | Talk |
|---|
| Leonardo De Moura and Dejan Jovanović | A Model-Constructing Satisfiability Calculus |  | Jul 16 14:30 |
| Jakob Nordstrom | A (Biased) Proof Complexity Survey for SAT Practitioners | | Jul 15 14:30 |
| Nina Narodytska and Fahiem Bacchus | Cores in Core based MaxSat Algorithms: an Analysis | | Jul 14 11:45 |
| Jan Arne Telle, Sigve Hortemo Sæther and Martin Vatshelle | Solving MaxSAT and #SAT on structured CNF formulas | | Jul 14 11:15 |
| Takayuki Sakai, Kazuhisa Seto and Suguru Tamaki | Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction | | Jul 14 10:45 |
| Anton Belov, Marijn Heule and Joao Marques-Silva | MUS Extraction using Clausal Proofs | | Jul 14 12:40 |
| Joao Marques-Silva and Alessandro Previti | On Computing Preferred MUSes and MCSes | | Jul 14 12:10 |
| Matti Järvisalo and Janne H. Korhonen | Conditional Lower Bounds for Failed Literals and Related Techniques | | Jul 14 15:30 |
| Ronald de Haan and Stefan Szeider | Fixed-Parameter Tractable Reductions to SAT | | Jul 14 14:30 |
| Alexey Ignatiev, Antonio Morgado and Joao Marques-Silva | On Reducing Maximum Independent Set to Minimum Satisfiability | | Jul 14 15:00 |
| Mladen Miksa and Jakob Nordstrom | Long Proofs of (Seemingly) Simple Formulas | | Jul 15 10:45 |
| Gabriel Istrate and Adrian Crăciun | Proof complexity and the Lovasz-Kneser Theorem (I) | | Jul 15 11:15 |
| Valeriy Balabanov, Magdalena Widl and Jie-Hong Roland Jiang | QBF Resolution Systems and their Proof Complexities | | Jul 15 16:30 |
| Oliver Kullmann and Olaf Beyersdorff | Unified characterisations of resolution hardness measures | | Jul 15 15:30 |
| Tomohiro Sonobe, Shuya Kondoh and Mary Inaba | Community Branching for Parallel Portfolio SAT Solvers | | Jul 15 12:20 |
| Laurent Simon and Gilles Audemard | Lazy clause exchange policy for parallel SAT solvers | | Jul 15 12:40 |
| Alexander Nadel, Ofer Strichman and Vadim Ryvchin | Ultimately Incremental SAT | | Jul 15 11:50 |
| Boris Konev and Alexei Lisitsa | A SAT Attack on the Erdos Discrepancy Conjecture | | Jul 16 10:45 |
| Tamir Heyman, Dan Smith, Lance Leong, Husam Abu-Haimed and Yogesh Mahajan | Dominant Controllability Check Using QBF-Solver and Netlist Optimizer | | Jul 16 11:05 |
| Bernd Finkbeiner and Leander Tentrup | Fast DQBF Refutation | | Jul 16 11:35 |
| Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard and Laurent Simon | Impact of Community Structure on SAT Solver Performance | | Jul 16 12:30 |
| Friedrich Slivovsky and Stefan Szeider | Variable Dependencies and Q-Resolution | | Jul 16 12:00 |
| Armin Biere, Daniel Le Berre, Emmanuel Lonca and Norbert Manthey | Detecting cardinality constraints in CNF | | Jul 16 17:30 |
| Adrian Balint, Armin Biere, Andreas Fröhlich and Uwe Schöning | Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses | | Jul 16 15:30 |
| Tomáš Balyo, Andreas Fröhlich, Marijn Heule and Armin Biere | Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask) | | Jul 16 16:30 |
| Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio | Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions | | Jul 17 10:45 |
| Yoav Fekete and Michael Codish | Simplifying Pseudo-Boolean Constraints in Residual Number Systems | | Jul 16 17:00 |
| Oliver Gableske | An Ising Model inspired Extension of the Product-based MP Framework for SAT | | Jul 17 11:15 |
| Andrei Bulatov and Cong Wang | Approximating highly satisfiable random 2-SAT | | Jul 17 11:45 |
| Florent Capelli, Arnaud Durand and Stefan Mengel | Hypergraph Acyclicity and Propositional Model Counting | | Jul 17 12:15 |
| Carles Creus, Pau Fernández and Guillem Godoy | Automatic Evaluation of Reductions between NP-complete Problems | | Jul 14 17:10 |
| Nathan Wetzler, Marijn Heule and Warren Hunt | DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs | | Jul 14 16:50 |
| Charles Jordan, Lukasz Kaiser, Florian Lonsing and Martina Seidl | MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing | | Jul 14 16:30 |
| Ruben Martins, Vasco Manquinho and Ines Lynce | Open-WBO: a Modular MaxSAT Solver | | Jul 14 17:30 |