SAT 2019
July 7 - 12, Lisboa, Portugal
Lisbon
Welcome Dates Committees CFP Workshops Proceedings Program Competitions Speakers Summer-School Registration Venue

Workshops

The list of workshops co-located with the SAT conference are as follows: For the Workshop Venue, Room location and options of where to eat, please check the information bellow.

Workshop Program (July 7th and 8th)

Sunday, July 7th
SMT WorkShop Vampire Workshop QBF Workshop
09:00-10:30Session 1
09:00-09:30 Invited Talk: SMT-Based Weighted Model Integration, Roberto Sebastiani (joint SMT/Vampire workshop) Invited Talk: Alexander Feldman: Toward Computer-Aided Digital Design
09:30-10:00
10:00-10:30 David Narváez: A QSAT Benchmark Based on Vertex-Folkman Problems
10:30-11:00Coffee break
11:00-12:30Session 2
11:00-11:30 The Eos SMT/SMA-Solver: A Preliminary Report, Maria Paola Bonacina and Giulio Mazzi Agnieszka Słowik, Chaitanya Mangla, Mateja Jamnik, Sean Holden and Lawrence Paulson Bayesian Optimisation with Gaussian Processes for Premise Selection Aile Ge-Ernst, Christoph Scholl and Ralf Wimmer: Localizing Quantifiers for DQBF
11:30-12:00 Interpolating Bit-vector Arithmetic Constraints in MCSAT, Stéphane Graham-Lengrand and Dejan Jovanović Bernhard Gleiss, Laura Kovacs and Jakob Rath Forward Subsumption Demodulation - Fast Conditional Rewriting in Vampire Oliver Kullmann and Ankit Shukla: Autarkies for DQCNF
12:00-12:30 Extending SMT solvers to Higher-Order Logic (presentation-only) Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett Martin Riener, A Flock of Vampires Leander Tentrup: Expanding Conflict Clauses
12:30-14:00Lunch
14:00-15:30Session 3
14:00-14:30 High-Level Abstractions for Simplifying Extended String Constraints in SMT, Andrew Reynolds, Andres Noetzli, Clark Barrett and Cesare Tinell Armin Biere, SAT, Computer Algebra and Multiplier Verification (invited talk) Stefan Mengel: Width measures for QBF (invited)
14:30-15:00 An Algorithm Selection Approach for QF_FP Solvers, Joseph Scott, Pascal Poupart and Vijay Ganesh
15:00-15:30 Constrained Optimization Benchmark for Optimization Modulo Theory: A Cloud Resource Management Problem, Madalina Erascu and Razvan Metes Olaf Beyersdorff, Joshua Blinkhorn and Meena Mahajan: Building Strategies into QBF Proofs
15:30-16:00Coffee break
16:00-17:30Session 4
16:00-16:30 An SMT Approach To A Multiparty Economic Scheduling Problem, Shriphani Palakodety, Guha Jayachandran and Aditya Thakur Martin Suda, Hints for AVATAR Valentin Mayer-Eichberger and Abdallah Saffidine: A Compact Encoding from Positional Games into QBF
16:30-17:00 Update on SMTLIB 3, Clark Barrett and Pascal Fontaine Yu-Ting Chen, Interfacing Intermediate Languages to Vampire Luca Pulina, Martina Seidl, Ankit Shukla: QBFEval 2019
17:00-17:30 Giles Reger and Andrei Voronkov, Induction in Saturation-Based Proof Search Discussion
Monday, July 8th
SMT WorkShop Pragmatics of SAT LaSh 2019 Workshop
09:00-10:30Session 1
09:00-09:30 Invited Talk: Programming Z3, Nikolaj Bjorner Jan Elffers and Jakob Nordström. On-the-fly cardinality detection David Mitchell. LaSh Welcome and Tutorial
09:30-10:00 Daniel Le Berre, Pierre Marquis, Stefan Mengel and Romain Wallon. On Irrelevant Literals in Pseudo-Boolean Constraint Learning Invited Talk: Martina Seidl. Expansion-Based QBF Solving
10:00-10:30 Stephan Gocht, Jakob Nordstrom and Amir Yehudayoff. On Division Versus Saturation in Pseudo-Boolean Solving
10:30-11:00Coffee break
11:00-12:30Session 2
11:00-11:30 Intrepid: an SMT-based Model Checker for Control Engineering and Industrial Automation. Roberto Bruttomesso Vadim Ryvchin and Alexander Nadel. Flipped Recording Isabel Oitavem A Recursion-Theoretic Approach to the Polynomial Hierarchy (11:00 - 11:45)
11:30-12:00 SPASS-SATT: a CDCL(LA) Solver. Martin Bromberger, Mathias Fleury, Simon Schwarz and Christoph Weidenbach Jan Elffers and Jakob Nordström. Visualizing CDCL VSIDS and phase values Antonius Weinzerl Lazy Grounding for Answer Set Programming: Challenges and Potential (11:45-12:30)
12:00-12:30 Towards Bit-Width-Independent Proofs in SMT Solvers. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett and Cesare Tinelli Katalin Fazekas, Daniela Kaufmann and Armin Biere. Ranking Robustness under Sub-Sampling for the SAT Competition 2018
12:30-14:00Lunch
14:00-15:30Session 3
14:00-14:30

SMT-COMP 2019 Report. Liana Hadarean, Antti Hyvarinen, Aina Niemetz and Giles Reger

SMT-COMP Tool Presentations 		Invited Talk: Joao Marques-Silva. SAT: Disruption, Demise and Resurgence Invited Talk: Konstantin Korovin. Solving non-linear constraints in CDCL style.
14:30-15:00
15:00-15:30 Mario Wenzel. Prolog API for LEGO EV3
15:30-16:00Coffee break
16:00-17:30Session 4
16:00-16:30 Business Meeting Marc Hartung and Florian Schintke. Learned Clause Minimization in Parallel SAT Solvers Katalin Fazekas. Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories.
16:30-17:00 Johannes K. Fichte, Markus Hecher and Markus Zisser. gpusat2 – An Improved GPU Model Counter Pierre Carbonnelle. Abstract Model Generation in an Interactive Configuration Tool
17:00-17:30 Jo Devriendt, Jan Elffers, Ambros Gleixner and Jakob Nordström. Leveraging LP solving for PB solving
17:30-18:00 Summary / discussion

Workshop on Satisfiability Modulo Theories

The SMT Workshop is focused on bringing together researchers and users of tools and techniques for satisfiability modulo theories. Relevant topics include but are not limited to:

For further information, please visit the SMT workshop website: http://smt2019.galois.com/

Workshop Dates:July 7th-8th 2019

Organizers:

QBF Workshop

The goal of the International Workshop on Quantified Boolean Formulas (QBF Workshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. In addition to that, it addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges. In particular, the following topics shall be considered at the workshop: 1) Directions of Solver Development 2) Certificates 3) Applications, and 4) Community platform and repository.

For further information, please visit the QBF workshop website: http://fmv.jku.at/qbf19/

Workshop Date:July 7th 2019

Organizers:

6th Vampire Workshop

The workshop aims at discussing recent developments in implementing, applying benchmarking and comparing first-order theorem provers and their combinations with other systems.

Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The developers can learn more about the use of Vampire, its efficiency in various application areas and needs of the users.

For further information, please visit the Vampire Workshop website: https://easychair.org/smart-program/Vampire2019/

Workshop Date:July 7th 2019

Organizers:

Pragmatics of SAT

The aim of the Pragmatics of SAT (PoS) workshop series is to provide a venue for researchers working on designing and/or applying Boolean satisfiability (SAT) solvers and related solver technologies, including but not restricting to satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP) as well as their optimization counterparts, to meet, communicate, and discuss latest results. This workshop allows researchers to share both fundamental theoretical insights into practical solvers, as well as new implementation-level insights and ‘gory’ technical details about their systems that may at times be difficult to publish in the main conferences on the declarative solving paradigms.

For further information, please visit the Pragmatics of SAT workshop website: http://www.pragmaticsofsat.org/2019/

Workshop Date:July 8th 2019

Organizers:

Workshop on Logic and Search

The LaSh Workshops on Logic and Search are devoted to the study, from the point of view of logic, of declarative languages for defining or representing search and optimization problems, problem-solving systems that use these languages, and related issues regarding reductions, search algorithms, problem transformations, and others.

For further information, please visit the LaSh 2019 workshop website: http://www.logicandsearch.org/LaSh2019/

Workshop Date:July 8th 2019

Organizers:

Workshops Venue

The SAT 2019 Workshops will take place at Informática buildings of the Instituto Superior Técnico (IST/UL) of the University of Lisbon. The university of Lisbon was founded in 1911 and it is known to be the largest university in Portugal. Instituto Superior Técnico (IST/UL), well known by its short name “Técnico”, is the most reputed school of Engineering, Science and Technology in Portugal.

Located in one of the central-most parts of Lisbon, the Alameda campus benefits from a transport network that facilitates mobility to all the areas of the city. In its vicinity, there are many shopping, leisure, culture, entertaining and sports areas. Alameda Campus is located at a convenient distance from hotels, restaurants and diverse cultural sites. Being close to the centre of Lisbon, Instituto Superior Técnico (IST/UL), is easily reached by metro, bus, taxi or car from any location in town, including the airport, which is only 10 minute taxi ride.

Workshop Room Location

The SMT workshop will be held in building #10, while all other workshops will take place in building #7 (see map below):

Where to eat

The Alameda campus of IST is located in the city center and there are several restaurants available at walking distance. On Sunday, several restaurants can be closed. A safe option would be the Campo Pequeno shopping mall (12 minutes walking - see map below). The shopping mall is a big round building in the center of the Campo Pequeno square. It has several restaurants on the outside, and a food court downstairs with a large variety of choices (including vegetarian and vegan options).

Call for Workshops

The International Conference on Theory and Applications of Satisfiability Testing (SAT) is the premier annual meeting for researchers focusing on the theory and applications of the propositional satisfiability problem, broadly construed. In addition to plain propositional satisfiability, it also includes Boolean optimization (such as MaxSAT and Pseudo-Boolean (PB) constraints), Quantified Boolean Formulas (QBF), Satisfiability Modulo Theories (SMT), and Constraint Programming (CP) for problems with clear connections to Boolean-level reasoning.

We invite proposals for workshops associated to the main conference program of SAT 2019, which will be held in Lisbon (Portugal) from July 7 to July 12, 2019.

Submission of Workshop Proposals

Proposals should be submitted in pdf format to the following address: workshops@sat2019.tecnico.ulisboa.pt.

Proposals should consist of two parts. First, a short scientific justification of the proposed topic, its significance, and the particular benefits of the workshop to the community, as well as a list of previous or related workshops (if relevant). A second, organizational part should include:

Important Dates

Contact Information

Questions regarding workshop proposals should be sent to workshops@sat2019.tecnico.ulisboa.pt.

SAT 2019 Workshop Chair
Vasco Manquinho
INESC-ID, IST - Universidade de Lisboa, Portugal