|Sunday, July 7th|
|SMT WorkShop||Vampire Workshop||QBF Workshop|
|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|
|10:00-10:30||David Narváez: A QSAT Benchmark Based on Vertex-Folkman Problems|
|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|
|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|
|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-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|
|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|
SMT-COMP 2019 Report. Liana Hadarean, Antti Hyvarinen, Aina Niemetz and Giles RegerSMT-COMP Tool Presentations
|Invited Talk: Joao Marques-Silva. SAT: Disruption, Demise and Resurgence||Invited Talk: Konstantin Korovin. Solving non-linear constraints in CDCL style.|
|15:00-15:30||Mario Wenzel. Prolog API for LEGO EV3|
|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|
For further information, please visit the SMT workshop website: http://smt2019.galois.com/
Workshop Dates:July 7th-8th 2019
For further information, please visit the QBF workshop website: http://fmv.jku.at/qbf19/
Workshop Date:July 7th 2019
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
For further information, please visit the Pragmatics of SAT workshop website: http://www.pragmaticsofsat.org/2019/
Workshop Date:July 8th 2019
For further information, please visit the LaSh 2019 workshop website: http://www.logicandsearch.org/LaSh2019/
Workshop Date:July 8th 2019
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.
The SMT workshop will be held in building #10, while all other workshops will take place in building #7 (see map below):
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).
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.
Proposals should be submitted in pdf format to the following address: firstname.lastname@example.org.
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:
Questions regarding workshop proposals should be sent to email@example.com.
SAT 2019 Workshop Chair
INESC-ID, IST - Universidade de Lisboa, Portugal