SAT-Based Local Improvement Methods (SLIM)

Structural decomposition is one of the most successful approaches to the solution of hard computational problems, such as for probabilistic reasoning and computational medical diagnosis. Finding a suitable structural decomposition is itself a computationally hard problem. In this project we propose to study a new approach to finding structural decompositions. The idea is to use an exact method (in particular one that is based on satisfiability- solvers) to locally improve a heuristically obtained decomposition. Based on this new idea we will develop new algorithms for the decomposition of graphs and hypergraphs as well as for structural Bayesian Network learning. Our new approach bears the potential of achieving better decompositions for instances that are too large to be handled by exact approaches, and it also provides novel applications for satisfiability solver technology. The research will be a combination of theoretical investigations and the development and testing of prototype implementations.

Many hard computational problems can be efficiently translated into the propositional satisfiability problem (SAT) and then solved with a powerful SAT solver or variants such as MaxSAT or QBF-SAT. In some cases, the translation causes a significant blow-up in size, so this one-shot translation is not feasible. In this project, we overcome this limitation by repeatedly translating small local parts of the problem instance to SAT, which allows us to scale the SAT solver's power to large instances. We could successfully implement this approach for various critical computational problems, including learning the structure of a Bayesian network, inducing an interpretable decision tree, or minimizing a Boolean circuit.