General Boolean Formula Minimization with QBF Solvers

TL;DR

This paper explores Boolean formula minimization using QBF solvers, demonstrating that encoding the problem as a QBF and solving with a QBF solver is more effective than brute force or SAT-based methods.

Contribution

It introduces a practical approach to Boolean formula minimization via QBF encoding and compares its performance to other methods, showing significant improvements.

Findings

QBF approach outperforms brute force and SAT-based methods

Encoding as QBF is effective for formula minimization

QBF solvers can handle the problem efficiently

Abstract

The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previous work in the area has focused on obtaining minimal, or quasi-minimal, formulae in conjunctive normal form (CNF) or disjunctive normal form (DNF), with applications in hardware design. In this paper, we are interested in the problem of obtaining an equivalent formula in any format, also allowing connectives that are not present in the original formula. We are primarily motivated in applying minimization algorithms to generate natural language translations of the original formula, where using shorter equivalents as input may result in better translations. Recently, Buchfuhrer and Umans have proved that the (decisional version of the) problem is $\Sigma_2^p$-complete. We analyze three possible (practical) approaches to solving the problem. First, using brute force, generating all possible formulae in increasing size and checking if they are equivalent to the original formula by testing all possible variable assignments. Second, generating the Tseitin coding of all the formulae and checking equivalence with the original using a SAT solver. Third, encoding the problem as a Quantified Boolean Formula (QBF), and using a QBF solver. Our results show that the QBF approach largely outperforms the other two.