HTTP/1.1 200 OK Date: Wed, 14 Jan 2026 12:22:53 GMT Server: Apache/2.4.41 (Ubuntu) Expires: Wed, 14 Jan 2026 12:22:53 GMT Connection: close Vary: Accept-Encoding Content-Encoding: gzip Content-Length: 6111 Content-Type: text/html; charset=UTF-8

SAT 2016: 19TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING PROGRAMINDEXES POS-16 | QBF 2016 | STRUCTSAT 2016 | SAT 2016 | SOLVE IT WITH SAT PROGRAM | INDEXES SAT 2016 PROGRAM Days: Tuesday, July 5th Wednesday, July 6th Thursday, July 7th Friday, July 8th Tuesday, July 5th View this program: with abstractssession overviewtalk overviewside by side with other conferences 08:30-09:00 Session 7: Reception desk Location: Labri Main Entrance 09:00-09:30 Session 8: Conference Opening Chair: Nadia Creignou Location: Auditorium Labri 09:30-10:30 Session 9: Satisfiability 1 (In memoriam Hilary Putnam) Chair: Stefan Mengel Location: Auditorium Labri 09:30 Nathan Mull, Daniel J. Fremont and Sanjit A. Seshia On the Hardness of SAT with Community Structure ( abstract ) 10:00 Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordstrom and Marc Vinyals Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ( abstract ) 10:30-11:00Coffee Break 11:00-12:30 Session 10: QBF Complexity Chair: Stefan Szeider Location: Auditorium Labri 11:00 Uwe Egly On stronger calculi for QBFs ( abstract ) 11:30 Mikolas Janota On Q-Resolution and DPLL QBF Solving ( abstract ) 12:00 Florian Lonsing, Uwe Egly and Martina Seidl Q-Resolution with Generalized Axioms ( abstract ) 12:30-14:00Lunch Break 14:00-15:00 Session 11: Invited Talk 1 Chair: Daniel Le Berre Location: Auditorium Labri 14:00 David Monniaux Satisfiability Testing, a Disruptive Technology in Program Verification ( abstract ) 15:00-15:30Coffee Break 15:30-17:00 Session 12: Satisfiability 2 Chair: Marijn Heule Location: Auditorium Labri 15:30 Neha Lodha, Sebastian Ordyniak and Stefan Szeider A SAT Approach to Branchwidth ( abstract ) 16:00 Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe and Marc Denecker Improved static symmetry breaking for SAT ( abstract ) 16:30 Jia Liang, Vijay Ganesh, Pascal Poupart and Krzysztof Czarnecki Learning Rate Based Branching Heuristic for SAT Solvers ( abstract ) 17:00-18:00 Session 13: Competitive events results Chair: Daniel Le Berre Location: Auditorium Labri 18:30-20:00 Session : Wine Tasting Chair: Laurent Simon Location: Badiane Wednesday, July 6th View this program: with abstractssession overviewtalk overviewside by side with other conferences 09:00-10:30 Session 14: Complexity 1 Chair: Martina Seidl Location: Auditorium Labri 09:00 Stefan Mengel Parameterized Compilation Lower Bounds for Restricted CNF-formulas ( abstract ) 09:20 Patrick Scharpfenecker and Jacobo Torán Solution-Graphs of Boolean Formulas and Isomorphism ( abstract ) 09:50 Johannes K. Fichte, Arne Meier and Irina Schindler Strong Backdoors for Default Logic ( abstract ) 10:30-11:00 Session 15: SAT Applications 1 Chair: Joao Marques-Silva Location: Auditorium Labri 10:30 Mathias Soeken, Alan Mishchenko, Ana Petkovska, Baruch Sterin, Paolo Ienne, Robert Brayton and Giovanni De Micheli Heuristic NPN classification for large functions using AIGs and LEXSAT ( abstract ) 11:00-11:30Coffee Break 11:30-12:30 Session 16: Invited Talk 2 Chair: Nadia Creignou Location: Auditorium Labri 11:30 Phokion Kolaitis Coping with Inconsistent Databases: Semantics, Algorithms, and Complexity ( abstract ) 12:30-14:00Lunch Break 14:00-15:00 Session 17: SMT 1 Chair: Roberto Sebastiani Location: Auditorium Labri 14:00 Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio Speeding Up the Constraint-Based Method in Difference Logic ( abstract ) 14:30 Jeevana Priya Inala, Rohit Singh and Armando Solar-Lezama Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers ( abstract ) 15:00-15:30Coffee Break 15:30-17:00 Session 18: CEGAR in memoriam Helmut Veith Chair: Uwe Egly Location: Auditorium Labri 15:30 Markus N. Rabe and Sanjit A. Seshia Incremental Determinization ( abstract ) 16:00 Leander Tentrup Non-prenex QBF Solving using Abstraction ( abstract ) 16:20 Valeriy Balabanov, Jie-Hong Roland Jiang, Alan Mishchenko, Christoph Scholl and Robert K. Brayton 2QBF: challenges and solutions ( abstract ) 17:00-18:00 Session 19: SAT association general assembly Chair: Armin Biere Location: Auditorium Labri Thursday, July 7th View this program: with abstractssession overviewtalk overviewside by side with other conferences 09:00-10:30 Session 20: Dependency QBF Chair: Mikolas Janota Location: Auditorium Labri 09:00 Ralf Wimmer, Christoph Scholl, Karina Wimmer and Bernd Becker Dependency Schemes for DQBF ( abstract ) 09:30 Olaf Beyersdorff, Leroy Chew, Renate Schmidt and Martin Suda Lifting QBF Resolution Calculi to DQBF ( abstract ) 09:50 Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider Long Distance Q-Resolution with Dependency Schemes ( abstract ) 10:30-11:00Coffee Break 11:00-12:30 Session 21: Complexity 2 Chair: John Franco Location: Auditorium Labri 11:00 Mateus de Oliveira Oliveira Satisfiability via Smooth Pictures ( abstract ) 11:30 Daniel Berend and Yochai Twitto The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r ( abstract ) 12:00 Vsevolod Oparin Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle ( abstract ) 12:30-14:00Lunch Break 14:00-15:00 Session 22: Invited Talk 3 (EurAI sponsored) Chair: Daniel Le Berre Location: Auditorium Labri 14:00 Torsten Schaub From SAT to ASP and back! ( abstract ) 15:00-15:30Coffee Break 15:30-17:30 Session 23: SAT and beyond Chair: Fahiem Bacchus Location: Auditorium Labri 15:30 Gilles Audemard and Laurent Simon Extreme Cases in SAT Problems ( abstract ) 16:00 Zurab Khasidashvili and Konstantin Korovin Predicate elimination for preprocessing in first-order theorem proving ( abstract ) 16:20 Giles Reger, Martin Suda and Andrei Voronkov Finding Finite Models in Multi-Sorted First Order Logic ( abstract ) 16:50 Carlos Mencía, Alexey Ignatiev, Alessandro Previti and Joao Marques-Silva MCS Extraction with Sublinear Oracle Calls ( abstract ) 18:00-23:00 Session : Banquet (bus leaving at 18:15 from LaBRI) Chair: Laurent Simon Location: Château Carbonnieux Friday, July 8th View this program: with abstractssession overviewtalk overviewside by side with other conferences 09:00-09:15 Session 24: Sponsor presentation Chair: Laurent Simon Location: Auditorium Labri 09:00 Ilia Zintchenko Presentation of the company Mindi ( abstract ) 09:15-10:30 Session 25: SAT Applications 2 Chair: Daniel Le Berre Location: Auditorium Labri 09:15 Marijn Heule, Oliver Kullmann and Victor Marek Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer ( abstract ) 10:00 Cuong Chau and Marijn Heule Computing Maximum Unavoidable Subgraphs using SAT Solvers ( abstract ) 10:30-11:00Coffee Break 11:00-12:40 Session 26: Tools presentations Chair: Albert Oliveras Location: Auditorium Labri 11:00 M. Fareed Arif, Carlos Mencia, Alexey Ignatiev, Norbert Manthey, Rafael Penaloza and Joao Marques-Silva BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies ( abstract ) 11:20 Antti Hyvärinen, Matteo Marescotti, Leonardo Alt and Natasha Sharygina OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing ( abstract ) 11:40 Tomas Balyo and Florian Lonsing HordeQBF: A Modular and Massively Parallel QBF Solver ( abstract ) 12:00 Paul Saikko, Jeremias Berg and Matti Järvisalo LMHS: A SAT-IP Hybrid MaxSAT Solver ( abstract ) 12:20 Norbert Manthey and Marius Lindauer SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers ( abstract ) 12:40-14:00Lunch Break 14:00-15:00 Session 27: SMT 2 Chair: Armin Biere Location: Auditorium Labri 14:00 Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Ruemmer Deciding Bit-Vector Formulas with mcSAT ( abstract ) 14:30 Martin Jonas and Jan Strejcek Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams ( abstract ) 15:00-15:30Coffee Break 15:30-16:30 Session 28: Competitive events panel Chair: Daniel Le Berre Location: Auditorium Labri 16:30-17:00 Session 29: Conference ending Chair: Laurent Simon Location: Auditorium Labri Disclaimer | Powered by EasyChair Smart Program