SLIM: SAT Based Local Improvement

Funding organization: Austrian Science Fund (FWF)

Project number: (FWF P 32441)

Project Team

• Stefan Szeider (PI)
• André Schidler
• P.R. Vaidyanathan

Topic

Many 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.