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.

翻译：命题公式的最小化是逻辑学中的一个经典问题，其最早的算法至少可追溯至20世纪50年代奎因和卡诺的研究。该领域以往的工作主要集中于获取合取范式（CNF）或析取范式（DNF）中的最小或拟最小公式，以应用于硬件设计。本文关注的问题是如何获得任意格式下的等价公式，同时允许使用原始公式中不存在的连接词。我们应用最小化算法的主要动机是生成原始公式的自然语言翻译，因为更短的等价输入可能产生更好的翻译结果。近期，Buchfuhrer和Umans已证明该问题（的判定版本）是$\Sigma_2^p$完全的。我们分析了三种可行的（实际）求解方案。其一，采用暴力方法，按从短到长的顺序生成所有可能的公式，并通过穷举所有变量赋值来验证它们是否与原始公式等价。其二，生成所有公式的Tseitin编码，并利用SAT求解器检验其与原始公式的等价性。其三，将问题编码为量化的布尔公式（QBF），并采用QBF求解器。结果表明，QBF方法的性能显著优于其他两种。