Horn Upper Bounds and Renaming

Abstract. We consider the problem of computing tractable approximations to CNF formulas, extending the approach of Selman and Kautz to compute the Horn-LUB to involve renaming of variables. Negative results are given for the quality of approximation in this extended version. On the other hand, experiments for random 3-CNF show that the new algorithms improve both running time and approximation quality. The output sizes and approximation errors exhibit a ‘Horn bump’ phenomenon: unimodal patterns are observed with maxima in some intermediate range of densities. We also present the results of experiments generating pseudo-random satisfying assignments for Horn formulas.

• Type: Conference
• Year: 2007
• Where: SAT
• Authors: Marina Langlois, Robert H. Sloan, György Turán
• Keywords: Approximation, Approximation Quality, SAT 2007, Tractable Approximations