SAT-based horn least upper bounds

Abstract

Knowledge compilation and approximation finds a wide range of practical applications. One relevant task in this area is to compute the Horn least upper bound (Horn LUB) of a propositional theory F. The Horn LUB is the strongest Horn theory entailed by F. This paper studies this problem and proposes two new algorithms that rely on making successive calls to a SAT solver. The algorithms are analyzed theoretically and evaluated empirically. The results show that the proposed methods are complementary and enable computing Horn LUBs for instances with a non-negligible number of variables.