| 2016 | 2QBF: Challenges and Solutions. Valeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton |
| 2016 | A SAT Approach to Branchwidth. Neha Lodha, Sebastian Ordyniak, Stefan Szeider |
| 2016 | BEACON: An Efficient SAT-Based Tool for Debugging M. Fareed Arif, Carlos Mencía, Alexey Ignatiev, Norbert Manthey, Rafael Peñaloza, João Marques-Silva |
| 2016 | Computing Maximum Unavoidable Subgraphs Using SAT Solvers. C. K. Cuong, M. J. H. Heule |
| 2016 | Deciding Bit-Vector Formulas with mcSAT. Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer |
| 2016 | Dependency Schemes for DQBF. Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker |
| 2016 | Extreme Cases in SAT Problems. Gilles Audemard, Laurent Simon |
| 2016 | Finding Finite Models in Multi-sorted First-Order Logic. Giles Reger, Martin Suda, Andrei Voronkov |
| 2016 | Heuristic NPN Classification for Large Functions Using AIGs and LEXSAT. Mathias Soeken, Alan Mishchenko, Ana Petkovska, Baruch Sterin, Paolo Ienne, Robert K. Brayton, Giovanni De Micheli |
| 2016 | HordeQBF: A Modular and Massively Parallel QBF Solver. Tomás Balyo, Florian Lonsing |
| 2016 | Improved Static Symmetry Breaking for SAT. Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, Marc Denecker |
| 2016 | Incremental Determinization. Markus N. Rabe, Sanjit A. Seshia |
| 2016 | LMHS: A SAT-IP Hybrid MaxSAT Solver. Paul Saikko, Jeremias Berg, Matti Järvisalo |
| 2016 | Learning Rate Based Branching Heuristic for SAT Solvers. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki |
| 2016 | Lifting QBF Resolution Calculi to DQBF. Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda |
| 2016 | Long Distance Q-Resolution with Dependency Schemes. Tomás Peitl, Friedrich Slivovsky, Stefan Szeider |
| 2016 | MCS Extraction with Sublinear Oracle Queries. Carlos Mencía, Alexey Ignatiev, Alessandro Previti, João Marques-Silva |
| 2016 | Non-prenex QBF Solving Using Abstraction. Leander Tentrup |
| 2016 | On Q-Resolution and CDCL QBF Solving. Mikolás Janota |
| 2016 | On Stronger Calculi for QBFs. Uwe Egly |
| 2016 | On the Hardness of SAT with Community Structure. Nathan Mull, Daniel J. Fremont, Sanjit A. Seshia |
| 2016 | OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina |
| 2016 | Parameterized Compilation Lower Bounds for Restricted CNF-Formulas. Stefan Mengel |
| 2016 | Predicate Elimination for Preprocessing in First-Order Theorem Proving. Zurab Khasidashvili, Konstantin Korovin |
| 2016 | Q-Resolution with Generalized Axioms. Florian Lonsing, Uwe Egly, Martina Seidl |
| 2016 | Satisfiability via Smooth Pictures. Mateus de Oliveira Oliveira |
| 2016 | Solution-Graphs of Boolean Formulas and Isomorphism. Patrick Scharpfenecker, Jacobo Torán |
| 2016 | Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. Martin Jonás, Jan Strejcek |
| 2016 | Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek |
| 2016 | Speeding up the Constraint-Based Method in Difference Logic. Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
| 2016 | SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers. Norbert Manthey, Marius Lindauer |
| 2016 | Strong Backdoors for Default Logic. Johannes Klaus Fichte, Arne Meier, Irina Schindler |
| 2016 | Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers. Jeevana Priya Inala, Rohit Singh, Armando Solar-Lezama |
| 2016 | The Normalized Autocorrelation Length of Random Max r -Sat Converges in Probability to (1-1/2^r)/r. Daniel Berend, Yochai Twitto |
| 2016 | Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings Nadia Creignou, Daniel Le Berre |
| 2016 | Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle. Vsevolod Oparin |
| 2016 | Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström, Marc Vinyals |