Abstract
Marijn Heule
Title: Look-ahead SAT Solvers: Smart vs. Fast
Abstract: A crucial decision in algorithm design is whether to make an algorithm fast or smart. In most cases, it is impossible to have them both as data structures that facilitate fast execution tend to prevent making smart decisions, e.g. because they require detailed information. The three main SAT solving paradigms are conflict-driven clause learning (CDCL), look-ahead, and stochastic local search (SLS). While look-ahead focuses on smart, CDCL and SLS aim to be fast. Each of these paradigms is effective on different classes of formulas. This talk provides an overview of state-of-the-art look-ahead solvers, which are strong on small hard problems that require sophisticated heuristics to solve them efficiently. In contrast to the other two paradigms, look-ahead solvers can be parallelized naturally resulting in linear time speedups. Look-ahead solvers can also be used to split a formula into many subproblems, which can be helpful to parallelize CDCL or SLS.
Jakob Nordstrom
Title: Pseudo-Boolean Solving: In Between SAT and ILP
Abstract: Pseudo-Boolean formulas, also known as 0-1 integer linear programs, can be used to concisely encode a wide range of problems. They are traditionally attacked by using (mixed) integer linear programming (MIP) solvers, but can also be approached by extending the conflict-driven paradigm from SAT solving. In this talk, we will briefly describe solvers using "native" pseudo-Boolean reasoning based on the cutting planes method, discuss how they can be integrated with techniques from MIP such as linear programming (LP) relaxations, and highlight some research questions that could point the way towards even better solvers.
Zhiwei Zhang
Title: Searching Inside the Box: A Continuous-Local-Search Approach for Hybrid SAT Solving
Abstract: While CDCL-based (CNF-)SAT solvers are well-engineered and dominating in practice, non-CNF constraints, which are playing important roles in areas such as graph theory (cardinality constraints) and cryptography (XOR), are far less studied. Traditional encodings and add-ons on CNF solvers for adapting to non-CNF constraints fail to provide a light and uniform solution. Inspired by traditional discrete local search approaches (e.g., GSAT), we lift the search domain from the Boolean cube to the real box. In this talk, I will introduce our framework that attempts to solve the hybrid Boolean constraint satisfaction problem by applying continuous optimization inside the real box. We define a multilinear-polynomial objective function based on the Fourier expansions of Boolean functions. Some interesting theoretical results regarding our continuous-local-search approach will be discussed. The versatility of Fourier expansions enables our framework to handle (CNF) clauses, XOR, cardinality constraints, and pseudo-Boolean constraints. Experiments show that continuous-local-search can be a useful complement to existing SAT/MaxSAT/PB solvers. As a method bridging discrete and continuous optimization, our approach also finds promising connections with neuro-symbolic and message passing techniques.