SAT-based Techniques for Optimization and Synthesis.

The SAT technology has been tremendously successful at solving a wide range of real-world problems, including hardware and software verification, bioinformatics, planning and scheduling. In this talk, I will present two practically important generalizations of the Boolean satisfiability (SAT) problem. First, I will talk about the maximum satisfiability problem (MaxSAT), which requires finding a solution of an over-constrained SAT instance that satisfies as many constraints as possible. I will describe the first algorithm that marries the MaxSAT resolution proof systems and the traditional iterative search procedure over the cost value. The resulting MaxSAT solver outperforms existing algorithms by a large margin on industrial problems in MaxSAT Evaluation’14. Second, I will talk about two-player games, which are a useful formalism for the synthesis of reactive systems. The traditional approach to solving such games iteratively computes the set of winning states for one of the players. This can lead to a state explosion even when using efficient symbolic representations. I will present a new game solving method that is based on viewing the game as an instance of the quantified SAT problem. Our domain-specific game solving algorithm works by exploring a subset of all possible concrete runs of the game and proving that these runs can be generalized into a winning strategy on behalf of one of the players. Our approach outperforms state-of-the-art solvers on some families of benchmarks.