Structure Identification with SAT (STRIDES)

SAT is the famous propositional satisfiability problem. It asks to assign the variables of a propositional formula with truth values 0 and 1 such that the entire formula becomes true. SAT is generally considered intractable, but over the last twenty years, computer programs (SAT solvers) have been engineered that can solve the problem surprisingly fast. Numerous other hard problems can be translated to SAT and solved via SAT solvers. However, the translation to SAT often causes a significant increase in size, which limits the application of SAT solvers to small problem inputs. The project aims at scaling the use of SAT solvers to large problem inputs by utilizing the recently introduced SAT-based Local Improvement Method (SLIM). It starts with an initial heuristic solution and repeatedly applies a SAT solver to small local parts of the input, overcoming the size limitation. The project will investigate using SLIM for problems that ask to find a specific hard-to-find structure in given data. Such structure identification problems arise in text data, large graphs and networks, and logical circuits. It will focus on methods for making the SLIM approach more efficient and finding general insights into its workings. The research is expected to lead to new theoretical and practical results.