The programme of the summer school will include both introductory and more advanced lectures. In addition, there will be three practical sessions, on SAT, SMT, and Automated Reasoning, respectively. Participants are kindly asked to bring their own laptops (if possible) for the practical sessions; of course, internet and WiFi will be available during the school.
Maria Paola Bonacina: Introduction to Automated Reasoning (slides)
Abstract: After a brief presentation of automated reasoning as a field of computer science, touching upon its goals, applications, and interfaces with other fields, the lecture focuses on first-order logic and surveys three families of theorem-proving strategies: ordering-based (e.g., resolution and superposition), subgoal-reduction-based (e.g., model-elimination tableaux), and instance-based (e.g., hyperlinking), where the latter may invoke SAT or SMT solvers. Then, it introduces SGGS, for Semantically-Guided Goal-Sensitive reasoning, a recent instance based theorem-proving method that generalizes CDCL (Conflict Driven Clause Learning) to first-order logic, and opens several directions for future research.
João Marques Silva: Introduction to SAT (slides)
Abstract: The success of Boolean Satisfiability (SAT) solver technology cannot be overstated. SAT solvers are currently used in hundreds of practical applications. Moreover, SAT solvers represent the core technology for other approaches to logic-based reasoning, including Satisfiability Modulo Theories and Answer Set Programming. Furthermore, the techniques proven effective in SAT have been applied in other domains, including Constraint Programming. This talk gives a mostly practical introductory overview of SAT, covering logic foundations, key technologies, propositional encodings, practical applications of SAT, and current research work. The talk also overviews work on applying SAT solvers as oracles in logic-based problem solving.
Dejan Jovanović: Introduction to SMT (slides)
Abstract: The lecture will provide an introduction to the SMT problem, various applications of SMT, and the techniques for solving it. The main focus will be on efficient decision procedures for theories of practical interest, and ways of combining them. While most of the lecture will revolve around the DPLL(T) framework, we will also touch on model-based decision procedures and interpolation.
Supratik Chakraborty: Counting and sampling solutions of SAT/SMT constraints (extended set of slides)
Abstract: Given a propositional formula, how many solutions does it have? Can we sample uniformly from the solution space, given that SAT solvers crucially depend on heuristics to quickly zoom down into a region of the solution space? What if we associate a weight with each solution and want the cumulative weight of all solutions? Can we sample solutions biased by their weights? Each of these problems has important applications spanning diverse domains like machine learning, statistical physics, software/hardware testing, network reliability estimation etc. Unfortunately, these problems are also provably hard (much harder than SAT solving), and therefore approximate solutions are of significant interest. Interestingly, the above problems are also closely related to each other: an efficient algorithm for one would yield an efficient algorithm for another as well. In this lecture, we will discuss both exact and approximate techniques to solve these problems. We will also show how improvements in SAT solving technology contribute directly to improving counting and sampling techniques. Among approximate techniques, we will focus particularly on techniques that provide strong approximation guarantees, while also scaling to large problem instances. We will also discuss how some of these techniques can be lifted to the SMT setting, yielding practically useful algorithms with rigorous guarantees for weighted model counting/integration and sampling from SMT constraints in certain theories.
Matti Järvisalo: Maximum Satisfiability (slides)
Abstract: Maximum satisfiability (MaxSAT) is an optimization version of Boolean satisfiability (SAT). As a Boolean optimization paradigm, MaxSAT is becoming a competitive alternative to e.g. integer programming (IP) for many NP-hard industrial and AI optimization problems. A big role in the recent successes of MaxSAT is played by advances in MaxSAT solver technology. This tutorial covers basic concepts on MaxSAT, and provides an overview of recent applications of MaxSAT and some of the main algorithmic approaches implemented in current state-of-the-art MaxSAT solvers.
Marius Lindauer: Algorithm Configuration: How to boost the performance of your SAT solver? (slides)
Abstract: Manual optimization of algorithm parameters (e.g., of SAT solvers) is a tedious, time-consuming and error-prone task; but nevertheless it is an important task since default parameter configurations often do not achieve peak performance. A recent example is the Configurable SAT Solver Challenge (CSSC), where the parameters of SAT solvers were optimized for each individual instance set and thereby the performance was often significantly improved by one or two orders of magnitude. To automate this process of parameter optimization, algorithm configurators (such as ParamILS and SMAC) have impressively shown how cutting-edge optimization and machine learning techniques can be combined to effectively solve the problem of parameter optimization. In the lecture, we will discuss how these algorithm configurators work and how they can be effectively applied to SAT solvers.
Florian Lonsing: Advances in QBF Reasoning (slides)
Abstract: The logic of quantified Boolean formulas (QBF) extends propositional logic by explicit existential or universal quantification of propositional variables. The satisfiability problem of QBF is PSPACE-complete. Therefore, QBFs are a natural formalism to encode problems from the complexity class PSPACE or from subclasses in the polynomial hierarchy. QBF encodings of problems are potentially exponentially more succinct than encodings in propositional logic. We review the current state of the art in QBF reasoning from a practical point of view. Given the stages in a typical workflow that arises from QBF reasoning tasks, we present approaches related to each stage. In this respect, relevant topics are QBF encodings, normal form transformation, QBF solving based on CDCL and expansion of variables, and generation of certificates or strategies. We outline the interplay between theoretical results in QBF proof complexity and practical applications of QBF reasoning tools. Recent progress in QBF proof complexity also motivates future directions of the development of QBF solvers.
Nuno P. Lopes: From Program Analysis to SMT and back (slides)
Abstract: Program analysis is of extreme importance. With applications ranging from finding costly (sometimes deadly) bugs, proving absence of bugs, to understanding how large code bases work, automating program analysis is of ever increasing interest. In this talk, I’ll give a crash course on automated program analysis with SMT solvers. We’ll see what makes this class of applications special and how to optimize SMT solvers for it. We’ll then discuss shortcomings and opportunities for improvement for SMT solvers, including what can SMT solvers learn with program analysis and compiler techniques.
Jakob Nordström: On the Interplay Between Proof Complexity and SAT Solving (slides)
Abstract: Although determining satisfiability of Boolean formulas is an NP-complete problem, and is hence believed to require exponential time in the worst case, algorithmic developments over the last 15-20 years have led to so-called SAT solvers that successfully handle real-world formulas with millions of variables. It is still quite poorly understood when and how such solvers work, however. Proof complexity studies formal methods for reasoning about Boolean formulas, and provides one of the few tools available for rigorous analysis of SAT solver performance. This talk is intended as something of a crash course in proof complexity, focusing on some comparatively weak proof systems of particular interest in the context of SAT solving. We will review resolution, polynomial calculus, and cutting planes (related to conflict-driven clause learning, Gröbner basis computations, and pseudo-Boolean solvers, respectively) and some proof complexity measures that have been studied for these proof systems. This will then allow us to discuss if and how these complexity measures could provide insights into the potential and limitations of current state-of-the-art SAT solvers, and how concerns related to applied SAT solving can give rise to interesting complexity-theoretic questions.
Andrew Reynolds: Instantiation for Quantified Formulas in SMT: Techniques and Practical Aspects (slides)
Abstract: Developing approaches for first-order quantified formulas in Satisfiablity Modulo Theories (SMT) solvers is a long standing challenge in the community. This talk will survey some of the techniques and practical aspects behind these approaches, focusing on those that are based on quantifier instantiation. To date, one of the most successful techniques is heuristic instantiation based on E-matching. This talk examines various ways to supplement this technique, both for accelerating the search for proofs of unsatisfiability and for establishing models. Finally, this talk will introduce new approaches for handling quantified formulas in first-order theories such as linear arithmetic, and how these techniques combined in practice with existing approaches.
Laurent Simon: Implementation of CDCL SAT solvers (slides, implementation)
Abstract: Over the last 20 years, the practical solving of SAT problems have made so much progresses that now, SAT solvers are omnipresent when solving combinatorial problems. In this talk, we will see the essential ingredients needed to write a state of the art SAT solver. We will describe how an essential data structure, the watched literals scheme, has pushed the entire algorithmic design of nowadays SAT solvers. We will show how conflict clause learning mechanism works and how to properly handle the set of learnt clauses and the restarting strategy. Before concluding, we will explore a number of intriguing experimental evidences showing that, despite their efficiency, SAT solvers are not yet well understood.
Christoph Weidenbach: Why Automated Reasoning Procedures Work: From Propositional SAT to More Expressive Logics (slides)
Abstract: One aspect why today’s SAT solvers work is non-redundant clause learning. This principle was already known in first-order logic reasoning before the invention of the CDCL algorithm for SAT. However, in first-order logic it is still not known how it can be effectively and efficiently realized. I will explain non-redundant clause learning for SAT and show that it can be lifted to decidable fragments of first-order logic, including QBF and the Bernays-Schoenfinkel (BS) fragment. However, extending BS with equality is already a challenge for the application of non-redundant clause learning. Linear integer arithmetic is another challenge: non-redundant clause learning “should also work” for this fragment as well, but we don’t know how.
Thomas Wies: Automated Reasoning in Separation Logic (slides)
Abstract: Separation logic (SL) has gained widespread popularity as a formal foundation of tools that analyze and verify heap-manipulating programs. Its great asset lies in its assertion language, which can succinctly express how data structures are laid out in memory, and its discipline of local reasoning, which mimics human intuition about how to prove heap programs correct. While the succinctness of separation logic makes it attractive for developers of program analysis tools, it also poses a challenge to automation: separation logic is a nonclassical logic that requires specialized theorem provers for discharging the generated proof obligations. SL-based tools therefore implement their own tailor-made theorem provers for this task. However, these theorem provers are not robust under extensions, e.g., involving reasoning about the data stored in heap structures. I will present an approach that enables complete combinations of decidable separation logic fragments with first-order theories. The approach works by reducing SL assertions to first-order logic. The target of this reduction is a decidable fragment of first-order logic that fits well into the SMT framework. That is, reasoning in separation logic is handled entirely by an SMT solver. The approach has been implemented in a deductive verification tool called GRASShopper, which I will demo in my lecture.
Practical Session on SAT, Propositional Satisfiability
Students are requested to install Python 3 on their laptops prior to the session.
Session leader: João Marques Silva, Laurent Simon, Matti Järvisalo
Practical Session on Automated Reasoning
This session will include exercises with the SPASS theorem prover:
- compact encoding of combinatorial problems using first-order logic (using Sudoku as an example);
- verification of real-world systems and protocols using first-order reasoning (e.g., the DHCP protocol).
Session leader: Christoph Weidenbach
Practical Session on SMT, Satisfiability modulo Theories
Students are requested to install the following solvers on their laptops:
Session leader: Dejan Jovanović