Computer Science

Topics:  Vijay Ganesh: Perspectives on Practice and Theory of SAT Solving Abstract: Over the last two decades, SAT solvers have revolutionized many sub-fields of software engineering, security, and AI. This is largely due to a dramatic improvement in the scalability of these solvers vis-a-vis large real-world formulas. What is surprising is that the Boolean satisfiability problem is NP-complete, believed to be intractable, and yet these solvers easily solve industrial instances containing millions of variables and clauses in them. How can that be? In my talk, I will briefly survey what we know about the power of SAT solvers through the lens of parameterized and proof complexity, as well as how we can build better SAT solvers by combining machine learning and proof systems. Laurent Simon: Towards an (experimental) Understanding of SAT Solvers Abstract: Despite important progresses in the practical solving of SAT problems, the behavior of CDCL solvers are only partially understood. In this talk, we will review some of the experimental studies that have been conducted so far, uncovering some surprising structures CDCL solvers are working on. David Mitchell: On Using Structural Properties to Improve CDCL Solver Performance Abstract: Instance structure is widely discussed and studied in the SAT solving community, but has never been explicitly made use of in dominant "industrial" SAT solvers.  We briefly review some structural properties of CNF formulas that have received attention, and some recent efforts to improve CDCL SAT solver performance using these properties.

Approximate Model Counting asks to compute the number of solutions of a formula F within a desired tolerance and confidence. While the earliest algorithmic ideas go back to the seminal work in the 1980's, scalable approximate counters were elusive until recently. In this talk, we will shed light on what makes the state of the art counters such as ApproxMC tick. In particular, we will illustrate how algorithmic frameworks' design needs considerations beyond the classical theory. The practical realization of these frameworks requires one to go beyond the traditional CNF solving.

Reactive synthesis is the problem of translating a logical specification into a reactive system that is guaranteed to satisfy the specification for all possible behaviors of its environment. More than 60 years after its introduction by Alonzo Church, the synthesis problem is still one of the most intriguing challenges in the theory of reactive systems. Recent years have brought advances both in reasoning methods that can be used as tools in the synthesis process and in the synthesis approaches themselves. As a result, the complexity of the synthesized systems has risen steadily. However, the logical and algorithmic foundations of the synthesis problem are still far from complete. In this tutorial, I will give an overview of both the classic constructions and more recent ideas such as bounded synthesis and the synthesis of distributed systems. In the latter, we try to find a combination of process implementations that jointly guarantee that a given specification is satisfied. A reduction from multi-player games shows that the problem is in general undecidable. Despite this negative result, there is a long history of discoveries where the decidability of the synthesis problem was established for distributed systems with specific architectures, although usually with high computational cost. Compositional approaches and new specification languages like HyperLTL, which offer a more comprehensive logical representation of the distributed synthesis problem, are potential ways forward. 

Today's cloud systems heavily rely on redundancy for reliability. Nevertheless, as cloud systems become ever more structurally complex, independent infrastructure components may unwittingly share deep dependencies. These unexpected common dependencies may result in causal failures that undermine redundancy efforts. The state-of-the-art efforts, e.g., post-failure forensics, not only lead to prolonged failure recovery time in the face of structurally complex systems, but also fail to avoid expensive service downtime. We describe RepAudit, an auditing system which builds on the so-called fault graph, to identify causal failures in the cloud. To ensure the practicality, efficiency, and accuracy of our approach, we further equip RepAudit with a domain-specific auditing language framework, a set of high-performance auditing primitives. We leverage SAT solvers to construct efficient fault graph analysis algorithms. To empirically evaluate this claim, we run RepAudit on a real-world cloud storage dataset and we observed that RepAudit is 300 times more efficient than other state-of-the-art auditing tools.  RepAudit technique has been used in Alibaba Group---the system is named CloudCanary---to perform real-time audits on service update scenarios to identify the root causes of correlated failure risks, and generate improvement plans with increased reliability.  CloudCanary has successfully detected various correlated failure risks such as single-point microservice, common power source, and shared network components, preventing service outages ahead of time.  The talk will conclude with an overview of the state of the arts on network verification community which widely relies on using SAT/SMT solver to check the correctness of network behaviors. References: [1] Ennan Zhai, Ruichuan Chen, David Isaac Wolinsky, Bryan Ford: Heading Off Correlated Failures through Independence-as-a-Service. OSDI 2014: 317-334 [2] Ennan Zhai, Ruzica Piskac, Ronghui Gu, Xun Lao, Xi Wang: An auditing language for preventing correlated failures in the cloud. PACMPL 1(OOPSLA): 97:1-97:28 (2017) This talk will be given in collaboration with Ennan Zhai, a researcher at Alibaba Group.

 This tutorial provides a programmer's introduction to Satisfiability Modulo Theories based on Z3. It illustrates how to define and solve SMT problems using scripts and walks through algorithms using exposed functionality.   Pre-recorded videos not available for Friday session.  

Pre-recorded videos not available for Friday session.   The availability of efficient SAT solvers presents opportunity for designing techniques for problems "beyond SAT". We will discuss two such problems that have witnessed increase in interest over the past decade: counting and sampling. Given a formula, the problem of counting is to compute the total number of solutions while sampling seeks to sample solutions uniformly at random. Counting and sampling are fundamental problems with applications such as probabilistic reasoning, information leakage, verification, and the like. In this talk, we will discuss approach that combines the classical ideas of universal hashing with CDCL solvers to design scalable approximate counters and samplers.  

Pseudo-Boolean solving is the task of finding a solution to a collection of (linear) pseudo-Boolean constraints, also known as a 0-1 integer linear program, possibly optimizing some linear objective function. This problem can be approached using methods from conflict-driven clause learning (CDCL) SAT solving as in MaxSAT solvers, or "native" pseudo-Boolean reasoning based on variants of the cutting planes proof system, or (mixed) integer linear programming (MIP). The purpose of this tutorial is to provide a brief survey of pseudo-Boolean reasoning, MaxSAT solving, and integer linear programming, focusing on the potential for synergy between these different approaches and highlighting many open problems on both the applied and the theoretical side.

These videos provide an introduction to proof complexity, especially from the point of view of satisfiability algorithms.  There are four videos.  Part A introduces proof complexity, and discusses Frege proofs, abstract proof systems, resolution, and extended Frege proofs and extended resolution.  Part B discusses the propositional pigeonhole principle, and upper and lower bounds on the complexity of proofs of the pigeonhole principle in the extended Frege proof system, the Frege proof systems, and resolution. Part C discusses the CDCL satisfiability algorithms from the point of view from proof complexity, including discussion of clause learning, trivial resolution, unit propagation, restarts, and RUP and (D)RAT proof traces.  Part D discusses cutting planes, the Nullstellsatz and Polynomial Calculus proof systems and concludes with a short discussion of automatizability. Parts B and C are independent of each other. Part D has a modest dependency on Part B, but can also be watched independently.

This tutorial focuses on explaining the most important aspects of the search loop in modern SAT solvers. It is an online BBC talk, i.e., black board and code, switching between a virtual black board to explain details and reviewing and using code in an interleaved manner. The code part features the new SAT Satch developed from scratch for this particular occasion. It is now available at  https://github.com/arminbiere/satch. We start with an introduction on encoding problems into conjunctive normal form, the input format of SAT solvers, and then delve into search based complete algorithms for SAT solving, from DPLL to CDCL and all its modern concepts, including the implication graph, decision heuristics (VSIDS and VMTF), restarts, as well as clause data base reduction, and then end with a closer look at clause and watching data structures and how they are updated during boolean constraint propagation.

From the early 1970s until now, SAT has been the central problem in Complexity Theory, inspiring many research directions. In the tutorial, I hope to show why SAT is such a favorite with complexity theorists, by talking about classical and modern results that involve SAT or its close relatives.  We'll talk about NP-completeness, polynomial-time hierarchy, interactive proofs, PCPs, as well as (circuit) lower bounds, Exponential-Time Hypothesis, and learning.

Cyberphysical systems are roughly characterized as systems enabled by coordination between computational and physical components and resources. They appear in a vast range of applications. Most applications of cyberphysical systems are subject to strict requirements for---to name a few---safety, security, and privacy. Formal methods for specification, verification, and synthesis have the potential to provide the languages, tools, and discipline necessary to meet these strict requirements. On the other hand, this potential can be realized only through proper connections between formal methods and several other fields. This tutorial will provide an overview of the complications in the context of cyberphysical systems that may benefit---and have benefited---from formal methods. It will provide examples of problems whose solution heavily relies on formal methods: correct-by-construction synthesis of hierarchical control protocols; synthesis of strategies under limitations on information availability; and verifiability of learning-enabled components.

In this talk I will outline automated techniques for the verification and control of partially observable probabilistic systems for both discrete and dense models of time. For the discrete-time case, we formally model these systems using partially observable Markov decision processes; for dense time, we propose an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. Quantitative properties of interest, relate to the probability of an event’s occurrence or the expected value of some reward measure. I will present techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. The approach is based on an integer discretisation of the model’s dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however both lower and upper bounds on numerical results can be generated.