Program

PROGRAM

Days: Monday, July 4th Tuesday, July 5th Wednesday, July 6th Thursday, July 7th Friday, July 8th Saturday, July 9th

Monday, July 4th

View this program: with abstracts session overview talk overview

08:30-09:30 Session 1: Reception desk (SAT 2016)

Location: Labri Main Entrance

09:00-10:30 Session 2: Presentations I (QBF 2016)

Location: Room 3 First floor, building A29

09:00	Joshua Blinkhorn and Olaf Beyersdorff Dependency Schemes in QBF Calculi: Semantics and Soundness ( abstract )
09:30	Günther Charwat and Stefan Woltran Dynamic Programming-based QBF Solving ( abstract )
10:00	Diptarama, Ryo Yoshinaka and Ayumi Shinohara QBF Encoding of Generalized Tic-Tac-Toe ( abstract )

09:30-10:30 Session 3A: Solvers presentations (POS-16)

"Beans and Eggs - Proteins for Glucose 3.0" by Markus Iser
"Splatz" by Armin Biere
"Sub-Stochastic Monte Carlo (SSMC)" by Brad Lackey, Stephen Jordan, and Michael Jarret
Tie break by Seongsoo Moon

Location: Auditorium Labri

09:30-10:30 Session 3B: Presentations I (STRUCTSAT 2016)

Location: Room 4 First floor, building A29

09:30	Eduard Eiben, Robert Ganian and Sebastian Ordyniak Using Decomposition-Parameters for QBF: Mind the Prefix! ( abstract )
10:00	Jesus Giráldez-Cru and Jordi Levy Pseudo-Industrial Random SAT Generators ( abstract )

10:30-11:00Coffee Break

11:00-12:30 Session 4A: Presentations I (POS-16)

Location: Auditorium Labri

11:00	Miquel Bofill, Marc Garcia, Jesús Giráldez-Cru and Mateu Villaret A Study on Implied Constraints in a MaxSAT Approach to B2B Problems ( abstract )
11:30	Saeed Nejati, Jia Liang, Vijay Ganesh, Catherine Gebotys and Krzysztof Czarnecki Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions ( abstract )
12:00	Seongsoo Moon and Mary Inaba Approximate History Map for Massively Parallel Environments ( abstract )

11:00-12:30 Session 4B: Presentations II (QBF 2016)

Location: Room 3 First floor, building A29

11:00	Mikolas Janota On Conflicts and Strategies in QBF ( abstract )
11:25	Christoph Scholl and Ralf Wimmer Skolem Functions for DQBF ( abstract )
11:50	Martin Suda First-Order Logic and Blocked Clauses ( abstract )
12:10	Martina Seidl and Florian Lonsing Discussion ( abstract )

11:00-12:30 Session 4C: Presentations II (STRUCTSAT 2016)

Location: Room 4 First floor, building A29

11:00	Sima Jamali, Ryan Mcbride and David Mitchell Experiments with CNF Structure and Hardness ( abstract )
11:30	Florent Capelli Structure-based knowledge compilation: the singular case of $\beta$-acyclic formulas ( abstract )
12:00	Oliver Kullmann Minimal unsatisfiability and deficiency: recent developments ( abstract )

12:30-14:00Lunch Break

14:00-15:00 Session 5A: Invited Talk (POS-16)

Location: Auditorium Labri

14:00

Mate Soos

Lessons learnt -- Seven years of CryptoMiniSat ( abstract )

14:00-15:00 Session 5B: Keynote (QBF 2016)

Location: Room 3 First floor, building A29

14:00

Hans Kleine Büning

Open Problems for Quantified Boolean Formulas ( abstract )

14:00-15:00 Session 5C: Presentations III (STRUCTSAT 2016)

Location: Room 4 First floor, building A29

14:00	Yoichi Iwata CNF Encoding of Cardinality Constraints via Tree-Decomposition ( abstract )
14:30	Holger Dell, Eunjung Kim, Michael Lampis, Valia Mitsou and Tobias Mömke Complexity and Approximability for Parameterized MAXCSPs ( abstract )

15:00-15:30Coffee Break

15:30-17:00 Session 6A: Presentations II (POS-16)

Location: Auditorium Labri

15:30	Norbert Manthey and Sibylle Moehle Better Evaluations by Analyzing Benchmark Structure ( abstract )
16:00	Jan Elffers, Jakob Nordstrom, Laurent Simon and Karem A. Sakallah Seeking Practical CDCL Insights from Theoretical SAT Benchmarks ( abstract )
16:30	Allen Van Gelder The Clashing-Neighbor Relation for Propositional Formulas ( abstract )

15:30-17:30 Session 6B: Competition (QBF 2016)

Competition

Location: Room 3 First floor, building A29

15:30	Florian Lonsing, Mikolas Janota, Shahab Tasharrofi, Allen Van Gelder, Markus Rabe, Konstantin Korovin and Leander Tentrup Short Presentations of Submissions to QBF Eval 2016 ( abstract )
16:30	Luca Pulina QBFEval 2016 ( abstract )

15:30-16:30 Session 6C: Keynote STRUCTSAT (STRUCTSAT 2016)

Invited Talk

Location: Room 4 First floor, building A29

15:30

Stefan Szeider

Capturing Structure in SAT and Related Problems ( abstract )

19:30-22:00 Session : Welcome reception (SAT 2016)

Chair:

Laurent Simon

Location: Palais de la bourse

Tuesday, July 5th

View this program: with abstracts session overview talk overview

08:30-09:00 Session 7: Reception desk (SAT 2016)

Location: Labri Main Entrance

09:00-09:30 Session 8: Conference Opening (SAT 2016)

Chair:

Nadia Creignou

Location: Auditorium Labri

09:30-10:30 Session 9: Satisfiability 1 (In memoriam Hilary Putnam) (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

Chair:

Daniel Le Berre

Location: Auditorium Labri

18:30-20:00 Session : Wine Tasting (SAT 2016)

Chair:

Laurent Simon

Location: Badiane

Wednesday, July 6th

View this program: with abstracts session overview talk overview

09:00-10:30 Session 14: Complexity 1 (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

Chair:

Armin Biere

Location: Auditorium Labri

Thursday, July 7th

View this program: with abstracts session overview talk overview

09:00-10:30 Session 20: Dependency QBF (SAT 2016)

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 (SAT 2016)

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) (SAT 2016)

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 (SAT 2016)

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) (SAT 2016)

Chair:

Laurent Simon

Location: Château Carbonnieux

Friday, July 8th

View this program: with abstracts session overview talk overview

09:00-09:15 Session 24: Sponsor presentation (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

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 (SAT 2016)

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 )