# Hardness of Horn-modulated Satsifiability problem?

It is known that there is sharp complexity jump between Horn 3-SAT and 3-SAT problems. The former is $P$-complete while the later is $NP$-complete. I would like to see a continuous spectrum of hardness variation between these two problems. I'm interested in finding the influence of the number Horn clauses in general 3-SAT problem. Suppose the number of Horn 3-SAT clauses in input 3-SAT formula is given as a function $f(n)$ in the number of variables $n$. What is known about the complexity of the 3-SAT(f) problem where $f(n)$ is one of the following cases:

1- $f(n)$ is $O(1)$

2- $f(n)$ is $O(\log n)$

3- $f(n)$ is $\Omega(n)$

4- $f(n)$ is $o(n)$

My intuition is that the first case is tractable while the third one is intractable. Also, I guess the second case is of intermediate complexity (NPI). What is known about the complexity of this problem? I'm looking for formal proofs of complexity?

EDIT: There is no restriction on the number of anti-Horn 3-SAT clauses. A 3-SAT clause must be either Horn or anti-Horn but not both.

-
Did you meant to say that $f$ is the number of non-Horn clauses? In case 1 we can do a brute force for non-Horn clauses as well as in case 2. Case 3 contains 3-SAT. Case 4 is likely to be NPI but we need to be careful about details (the number of clauses and the size of the input), probably a simple padding argument can be shown to prove it (we may need some complexity theory assumptions to prove it). – Kaveh Dec 21 '12 at 20:08
what ever you choose. It is purely conventional. – Mohammad Al-Turkistany Dec 21 '12 at 20:17
The number of Horn clauses is not useful because you can add polynomially many of them without changing complexity. Complexity comes from non-Horn clauses. – Kaveh Dec 21 '12 at 20:42
A 3-SAT clause must be either Horn or anti-Horn not both. – Mohammad Al-Turkistany Dec 21 '12 at 21:37
@MohammadAl-Turkistany: perhaps another interesting similar problem is picking two types of clauses used in Schaefer's theorem (2-Sat, Xor-sat, Horn-sat, anti-Horn-sat) and building a formula with 50% of one type and 50% of another and then studying how the satisfiability complexity of the whole formula is affected by the number of variables shared among the two blocks. – Marzio De Biasi Dec 21 '12 at 22:11