Satisfiability of mixed Horn formulas

In this paper the class of mixed Horn formulas is introduced that contain a Horn part and a 2-CNF (conjunctive normal form) (also called quadratic) part. We show that SAT remains NP-complete for such instances and also that any CNF formula can be encoded in terms of a mixed Horn formula in polynomial time. Further, we provide an exact deterministic algorithm showing that SAT for mixed Horn formulas containing n variables is solvable in time O(2^0.5284n). A strong argument showing that it is hard to improve a time bound of O(2^n/2) for mixed Horn formulas is provided. We also obtain a fixed-parameter tractability classification for SAT restricted to mixed Horn formulas C of at most k variables in its positive 2-CNF part providing the bound O(∥C∥2^0.5284k). We further show that the NP-hard optimization problem minimum weight SAT for mixed Horn formulas can be solved in time O(2^0.5284n) if non-negative weights are assigned to the variables. Motivating examples for mixed Horn formulas are level graph formulas B. Randerath, E. Speckenmeyer, E. Boros, P. Hammer, A. Kogan, K. Makino, B. Simeone, O. Cepek, A satisfiability formulation of problems on level graphs, ENDM 9 (2001)] and graph colorability formulas.