ABSTRACT. The ability of modern SAT solvers to handle huge industrial instances having 100,000,000’s clauses is highly intriguing, if not mysterious. It is well-known that the breakthrough in capacity was enabled by the introduction of the so-called Conflict-Driven-Clause-Learning (CDCL), or, simply, Conflict-driven SAT solving in the late 90s and early 00s. We will start by reviewing the seminal works on the first conflict-driven solvers--GRASP and Chaff--including some lesser-known facts. We will also discuss the crucial Boolean Constraint Propagation (BCP) algorithm and the evolvement of the underlying data structures. Furthermore, we will review later works on chronological backtracking, their relation to the original work in GRASP and the challenges of combining chronological backtracking with efficient BCP. Finally, we will go over algorithms for enhanced clause learning.

ABSTRACT. Modern Maximum Satisfiability (MaxSAT) offers an effective tool for solving NP-hard optimization problems arising in various domains. In this talk I will overview the history and development of algorithms and solvers for solving instances of MaxSAT, focusing especially on the so called complete algorithms, geared toward computing provably optimal solutions to instances arising in real-world domains. I will also highlight some interesting future research directions in the field, including the introduction of a new incremental track in the 2022 MaxSAT Evaluation.

ABSTRACT. Many critical applications crucially rely on the correctness of SAT solvers. Particularly in the context of formal verification, the claim by a SAT solver that a formula is unsatisfiable corresponds to a safety or security property to hold, and thus needs to be trusted. In order to increase the level of trust an exciting development in this century was to let SAT solvers produce certificates, i.e., by tracing proofs of unsatisfiability, which can independently be checked. In the last ten years this direction of research gained substantial momentum, e.g., solvers in the main track of the SAT competition are required to produce such certificates and industrial applications of SAT solvers require that feature too. In this talk we review this quarter of century of research in certifying the result of SAT solvers, discuss briefly alternatives, including testing approaches and verifying the SAT solver directly, mention exciting research on new proof systems produced in this context as well as how these ideas extend beyond formulas in conjunctive normal form.

ABSTRACT. This talk will provide a brief survey on the relations between proof complexity and SAT solving. What can proof complexity tell us about the strength and limitations of SAT solving? Why should practitioners be interested in proof complexity results and why should theorists study SAT solving? What have we achieved in the past 25 years and which problems remain open?

ABSTRACT. The talk will have two parts:

1. Modern SAT solvers combine rewriting techniques with conflict-driven clause learning (CDCL) search to maximize performance. Rewriting techniques improve the encoding of problems and they can further simplify formulas after CDCL search found useful clauses. The most effective rewriting technique is bounded variable elimination combined with subsumption. Together they reduce the size of industrial problems substantially. Other powerful rewriting techniques are shrinking clauses (vivification) and eliminating redundant clauses. Each rewriting technique can enable simplifications by other rewriting techniques. The order in which they are applied impacts the effectiveness.

Novel value selection heuristics are also key to modern SAT solving. Assigning decision variables to the last implied value facilitates rapid restarts to improve the quality of learning while staying in a similar part of the search space. Additionally, the search is guided toward a solution using assignments obtained by local search techniques. These heuristic improvements boosted modern SAT solver performance on satisfiable formulas.

2. Remembering Hans van Maaren

ABSTRACT. Generating realistic random SAT instances ---random SAT formulas with computational characteristics similar to the ones of application SAT benchmarks--- is a challenging problem in order to understand the success of modern SAT solvers solving this kind of problems. Traditional approaches are based on probabilistic models, where a probability distribution characterizes the occurrences of variables into clauses in order to mimic a certain feature exhibited in most application formulas (e.g., community structure), but they may be unable to reproduce others. Alternatively, deep generative models have been recently proposed to address this problem. The goal of these models is to learn the whole structure of the formula without focusing on any predefined feature, in order to reproduce all its computational characteristics at once. In this work, we propose two new deep generative models of realistic SAT instances, and carry out an exhaustive experimental evaluation of these and other existing models in order to analyze their performances. Our results show that models based on graph convolutional networks, possibly enhanced with edge features, return the best results in terms of structural properties and SAT solver performance.

ABSTRACT. This paper applies machine learning (ML) to solve quantified SMT problems more efficiently. The motivating idea is that the solver should learn from already solved formulas to solve new ones. This is especially relevant in classes of similar formulas.

We focus on the enumerative instantiation---a well-established approach to solving quantified formulas anchored in the Herbrand's theorem. The task is to select the right ground terms to be instantiated. In ML parlance, this means learning to rank ground terms. We devise a series of features of the considered terms and train on them using boosted decision trees. In particular, we integrate the LightGBM library into the SMT solver CVC5.

The experimental results demonstrate that ML-guided enables us to solve more formulas and reduce the number of quantifier instantiations.

ABSTRACT. We introduce Intel(R) SAT Solver (IntelSAT) -- a new open-source CDCL SAT solver, written from scratch. IntelSAT is optimized for applications which generate many mostly satisfiable incremental SAT queries. We apply the following Incremental Lazy Backtracking (ILB) principle: in-between incremental queries, backtrack only when necessary and to the highest possible decision level. ILB is enabled by a novel reimplication procedure, which can reimply an assigned literal at a lower level without backtracking. Reimplication also helped us to restore the following two properties, lost in the modern solvers with the introduction of chronological backtracking: no assigned literal can be implied at a lower level, conflict analysis always starts with a clause falsified at the lowest possible level. In addition, we apply some new heuristics. Integrating IntelSAT into the MaxSAT solver TT-Open-WBO-Inc resulted in a significant performance boost on incomplete unweighted MaxSAT Evaluation benchmarks and improved the state-of-the-art in anytime unweighted MaxSAT solving.

ABSTRACT. The development of practical approaches for efficiently reasoning over pseudo-Boolean constraints has recently received increasing attention as a natural generalization of SAT solving. Analogously, solvers for seudo-Boolean optimization draw inspiration form solving techniques developed for maximum satisfiability (MaxSAT) solving. Recently, first practical solver lifting the implicit hitting set (IHS) approach---one of the most efficient approaches in modern MaxSAT solving---to the realm of PBO was developed, employing a PB solver as a core extractor together with an integer programming solver as a hitting set solver. In this work, we make practical improvements to the IHS approach to PBO. We propose the integration of solution-improving search to the PBO-IHS approach, resulting in a hybrid approach to PBO making use of both types of search towards an optimal solution. Furthermore, we explore the potential of variations of core extraction within PBO-IHS---including recent advances in PB core extraction, allowing for extracting more general PB constraints compared to the at-least-one constraints typically relied on in IHS---in speeding up PBO-IHS search. We validate these ideas in the realm of PBO-IHS by showing that the empirical efficiency of PBO-IHS---recently shown to outperform other specialized PBO solvers---is further improved by the integration of these techniques.

ABSTRACT. The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the conjunctive normal form (CNF) format used for SAT proof logging means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is to translate the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.

ABSTRACT. A reactive system maintains an on-goint interaction with its environment. At each moment in time, the system receives from the environment an assignment to the input signals and responds with an assignment to the output signals. The system is correct with respect to a given specification if, for all environments, the infinite computation that is generated by the interaction between the system and the environment satisfies the specification. Reactive systems are modeled by transducers: finite state machines whose transitions are labeled by assignments to the input signals and whose states are labeled by assignments to the output signals. In the synthesis problem, we automatically transform a given specification into a correct transducer.

While complexity measures receive much attention in the design of algorithms, they are less explored in the context of synthesis. This is a serious drawback: just as we cannot imagine an algorithm designer that accepts a correct algorithm without checking its complexity, we cannot expect designers of reactive systems to accept synthesized systems that are only guaranteed to be correct. It is not clear, however, how to define the complexity of a transducer. Unlike the case of algorithms (or Turing machines in general), there is no "size of input" to relate to, and measures like time and space complexity are irrelevant. Indeed, we care for on-going interactions, along which the transducer reacts instantly according to its transition function. One immediate complexity measure for a transducer is its size, but many more complexity measures are of interest. The talk discusses such measures and describes how the search for optimal reactive systems affects the synthesis problem.