You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Horn Upper Bounds and Renaming1


Selman and Kautz [22] proposed an approach to compute a Horn CNF approximation of CNF formulas. We extend this approach and propose a new algorithm for the Horn least upper bound that involves renaming variables. Although we provide negative results for the quality of approximation, experimental results for random CNF demonstrate that the proposed algorithm improves both computational efficiency and approximation quality. We observe an interesting behavior in the Horn approximation sizes and errors which we call the “Horn bump”: Maxima occur in an intermediate range of densities below the satisfiability threshold.