Simple but Hard Mixed Horn Formulas

Abstract. We study simple classes of mixed Horn formulas, in which the structure of the Horn part is drastically constrained. We show that the SAT problem for formulas in these classes remains NP-complete, and demonstrate experimentally that formulas randomly generated from these classes are hard for the present SAT solvers, both complete and local-search ones.

• Type: Journal
• Year: 2010
• Where: SAT
• Authors: Gayathri Namasivayam, Miroslaw Truszczynski
• Keywords: Hardware, Mixed Horn Formulas, Present Sat Solvers, SAT 2010, Simple Classes