<p>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:</p>

<p>1- $f(n)$ is $O(1)$</p>

<p>2- $f(n)$ is $O(\log n)$</p>

<p>3- $f(n)$ is $\Omega(n)$</p>

<p>4- $f(n)$ is $o(n)$</p>

<p>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?</p>

<p>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.</p>

CC BY-SA 3.0
2012-12-21T20:08:41.310Z
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
CC BY-SA 3.0
2012-12-21T20:17:01.553Z
what ever you choose. It is purely conventional.
Mohammad Al-Turkistany
CC BY-SA 3.0
2012-12-21T20:42:07.163Z
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
CC BY-SA 3.0
2012-12-21T21:37:48.930Z
A 3-SAT clause must be either Horn or anti-Horn not both.
Mohammad Al-Turkistany
CC BY-SA 3.0
2012-12-21T21:57:51.627Z
@MarzioDeBiasi, your example is anti-Horn since the number of negative literals is at most one.
Mohammad Al-Turkistany
CC BY-SA 3.0
2012-12-21T22:11:39.133Z
@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
CC BY-SA 3.0
2012-12-21T23:37:40.827Z
I agree, your suggestion is interesting too.
Mohammad Al-Turkistany
CC BY-SA 3.0
2012-12-22T19:34:49.037Z
there are indeed many various transitions but the horn-to unrestrained SAT maybe has not been studied. that sounds more like limiting how many negative vs positive literals and theres probably some kind of phase transition(s) there. the "2.x" to 3SAT transition has been studied somewhat in some papers iirc. imho the way to go is to study the properties in what is called the "clause graph". see recent analysis [Decomposing SAT problems](http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf) by Herwig. maybe some generalization of clause graphs taking '+' vs '-' literals into acct somehow...
vzn
CC BY-SA 4.0
2019-11-27T04:45:57.453Z
@MarzioDeBiasi The mix of 2-Sat and Horn-Sat (not in 50:50 ratio) is studied. It is called Mixed Horn Formulas (MHF). A variant of this I find interesting is a mix of Anti-horn 2-sat clauses and horn clauses. That is, a CNF formula where each clause is either an anit-horn clause on two literals, or a Horn clause.
Cyriac Antony
<cc.complexity-theory><sat>
Hardness of Horn-modulated Satsifiability problem?
Mohammad Al-Turkistany
# Hardness of Horn-modulated Satsifiability problem?

(Asked by: username_0 on 2012-12-21)

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.

**Tags:** cc.complexity-theory, sat
> **Comments:**
> **username_1**: 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).  
> **username_0**: what ever you choose. It is purely conventional.  
> **username_1**: 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.  
> **username_0**: A 3-SAT clause must be either Horn or anti-Horn not both.  
> **username_0**: @MarzioDeBiasi, your example is anti-Horn since the number of negative literals is at most one.  
> **username_2**: @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.  
> **username_0**: I agree, your suggestion is interesting too.  
> **username_3**: there are indeed many various transitions but the horn-to unrestrained SAT maybe has not been studied. that sounds more like limiting how many negative vs positive literals and theres probably some kind of phase transition(s) there. the "2.x" to 3SAT transition has been studied somewhat in some papers iirc. imho the way to go is to study the properties in what is called the "clause graph". see recent analysis [Decomposing SAT problems](http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf) by Herwig. maybe some generalization of clause graphs taking '+' vs '-' literals into acct somehow...  
> **username_4**: @MarzioDeBiasi The mix of 2-Sat and Horn-Sat (not in 50:50 ratio) is studied. It is called Mixed Horn Formulas (MHF). A variant of this I find interesting is a mix of Anti-horn 2-sat clauses and horn clauses. That is, a CNF formula where each clause is either an anit-horn clause on two literals, or a Horn clause.  

---

## 0 answers

