<p><strong>SHORT ANSWER</strong></p>
<ul>
<li><p>The existence of a method to decide EXACTLY if &quot;a formula can be solved in polynomial time&quot; would prove that P=NP. It does not mean that such a method cannot exist (proving this would prove that P&lt;&gt;NP), but it proves that deciding if such a method exists is hard, and has not been solved yet.</p>
</li>
<li><p>The alternative are heuristics which decide if a formula falls into some limited set of categories for which a polynomial time solver exists, which is what you described.</p>
</li>
</ul>
<p><strong>LONG ANSWER</strong></p>
<p>First, let's clarify that a list of 3-CNF formula (with <span class="math-container">$n$</span> variables and <span class="math-container">$m$</span> clauses) that can be solved in polynomial time would be exponential in <span class="math-container">$n$</span> and <span class="math-container">$m$</span>: I assume below that you are asking a list of <em>classes</em> of such formula.</p>
<p>Second, an exact characterization of all 3-CNF formula (with <span class="math-container">$n$</span> variables and <span class="math-container">$m$</span> clauses) in the form of a &quot;black box&quot; which, for any input coding a 3-CNF formula  &quot;f&quot;, decides EXACTLY if &quot;f is solvable in polynomial time&quot; would solve the P vs NP debate, which is quite unlikely or at least very very difficult:</p>
<p>Given such a black box you would be able to build another black box which decides that &quot;f is not solvable in polynomial time&quot;, which would in turn imply that P&lt;&gt;NP (because if P=NP, there is no such f).</p>
<p>I hope it helped!</p>

CC BY-SA 4.0
2022-08-28T16:51:44.253Z
`The alternative are heuristics which decide if a formula falls into some limited set of categories for which a polynomial time solver exist, which already exist, and is what you describe.` Yes i was asking for a list of limited set of categories for which a polynomial time solver exist, i doubt the list that i gave in my question is complete, hence i asked whether there exist another categories of 3-CNF formula for which a polynomial time solver exist but is not in the list i gave.
LLL
CC BY-SA 4.0
2022-08-28T20:08:52.240Z
But the very existence of a complete list of such categories  would imply that P=NP!
Maybe, rather than asking if there exist, you want to ask if some other categories are currently known?
J.y B.y
CC BY-SA 4.0
2022-08-29T04:21:23.717Z
`you want to ask if some other categories are currently known` yes this is what i was asking, perhaps i was wrong for asking a complete list
LLL
CC BY-SA 4.0
2022-08-30T16:53:49.553Z
Small formulas are easy. Large formulas are hard. So you need a measure of modest size, such as under 500 variables, as part a polynomial filter. Theorem 7.18 in Garey and Johnson where language A is small and language B is large, giving the interesting theorem.
daniel pehoushek
CC BY-SA 4.0
2022-08-28T10:20:58.597Z
2022-08-29T11:24:29.750Z
2022-08-29T11:24:29.750Z
J.y B.y
<p>Suppose i want to program a 3-SAT solver. I want my solver to first check whether a formula is in the list of 3-CNF that currently known can be solved in polynomial time before resorting to brute force.</p>
<p>Wikipedia page <a href="https://en.wikipedia.org/wiki/Boolean_satisfiability_problem" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Boolean_satisfiability_problem</a> listed the following formula as solvable in polynomial time: 2-CNF, XOR Formula, Horn Formula, Renamable Horn Formula, Dual Horn Formula, Renamable Dual Horn Formula.</p>
<p>Have anyone found polynomial time algorithm to find whether a formula is Renamable XOR formula ?
Is there any other form of 3-CNF formula that can be solved in polynomial time but is not listed above</p>

CC BY-SA 4.0
2022-08-27T18:14:49.673Z
Both ordinary Horn formulas and dual Horn formulas are subsumed by renamable Horn formulas. What do you mean by renamable dual Horn formulas?
Emil Jeřábek
CC BY-SA 4.0
2022-08-27T18:33:07.990Z
Also, renaming a XOR formula just yields another XOR formula. So what do you mean by renamable XOR formula?
Emil Jeřábek
CC BY-SA 4.0
2022-08-28T16:24:38.683Z
@EmilJeřábek ah i didn't notice that both horn and dual horn are subsumed by renamable horn, thanks for the reminder. What i mean by renamable XOR is a 3-CNF formula that can be converted to XOR formula by replacing all OR gate with XOR gate and by flipping variable polarity, i haven't found any paper that can check whether a formula is renamable XOR formula in polynomial time, hence i asked about it in my question.
LLL
CC BY-SA 4.0
2022-08-29T05:35:56.130Z
I still have no idea what you mean. Replacing OR gates with XOR gates is a syntactic operation that can be done with any CNF, and *always* results in a XOR formula, so there is nothing to check. Flipping polarity does not do anything here. XOR formulas are just linear systems over $\mathbb F_2$, and flipping polarity of some of the variables just changes the constant coefficients of some of the linear equations.
Emil Jeřábek
CC BY-SA 4.0
2022-08-29T05:56:25.913Z
@EmilJeřábek if F is a renamable Horn formula, then we can obtain formula G such that G is a horn formula and for all input that satisfy G, we can obtain input that satisfy F by flipping the polarity of variable in the input that satisfy G. If H is a renamable XOR formula, then we can obtain formula J such that J is a XOR formula, and for every input that satisfy J, we can obtain input that satisfy H by flipping the polarity of variable in the input that satisfy J.
LLL
CC BY-SA 4.0
2022-08-29T07:11:50.310Z
For the third time: if you can obtain a XOR formula J from a formula H by flipping polarity of some variables, then H was a XOR formula to begin with. So flipping variables is completely pointless here.
Emil Jeřábek
<time-complexity><sat><polynomial-time><boolean-formulas>
list of 3-CNF formula that can be solved in polynomial time
LLL
# list of 3-CNF formula that can be solved in polynomial time

(Asked by: username_0 on 2022-08-27)

Suppose i want to program a 3-SAT solver. I want my solver to first check whether a formula is in the list of 3-CNF that currently known can be solved in polynomial time before resorting to brute force.

Wikipedia page <https://en.wikipedia.org/wiki/Boolean_satisfiability_problem> listed the following formula as solvable in polynomial time: 2-CNF, XOR Formula, Horn Formula, Renamable Horn Formula, Dual Horn Formula, Renamable Dual Horn Formula.

Have anyone found polynomial time algorithm to find whether a formula is Renamable XOR formula ?
Is there any other form of 3-CNF formula that can be solved in polynomial time but is not listed above

**Tags:** time-complexity, sat, polynomial-time, boolean-formulas

> **Comments:**
> **username_1**: Both ordinary Horn formulas and dual Horn formulas are subsumed by renamable Horn formulas. What do you mean by renamable dual Horn formulas?  
> **username_1**: Also, renaming a XOR formula just yields another XOR formula. So what do you mean by renamable XOR formula?  
> **username_0**: @EmilJeřábek ah i didn't notice that both horn and dual horn are subsumed by renamable horn, thanks for the reminder. What i mean by renamable XOR is a 3-CNF formula that can be converted to XOR formula by replacing all OR gate with XOR gate and by flipping variable polarity, i haven't found any paper that can check whether a formula is renamable XOR formula in polynomial time, hence i asked about it in my question.  
> **username_1**: I still have no idea what you mean. Replacing OR gates with XOR gates is a syntactic operation that can be done with any CNF, and *always* results in a XOR formula, so there is nothing to check. Flipping polarity does not do anything here. XOR formulas are just linear systems over $\mathbb F_2$, and flipping polarity of some of the variables just changes the constant coefficients of some of the linear equations.  
> **username_0**: @EmilJeřábek if F is a renamable Horn formula, then we can obtain formula G such that G is a horn formula and for all input that satisfy G, we can obtain input that satisfy F by flipping the polarity of variable in the input that satisfy G. If H is a renamable XOR formula, then we can obtain formula J such that J is a XOR formula, and for every input that satisfy J, we can obtain input that satisfy H by flipping the polarity of variable in the input that satisfy J.  
> **username_1**: For the third time: if you can obtain a XOR formula J from a formula H by flipping polarity of some variables, then H was a XOR formula to begin with. So flipping variables is completely pointless here.  

---

## 1 answers

### Answer by username_2 on 2022-08-28. Score: -1

**SHORT ANSWER**

* The existence of a method to decide EXACTLY if "a formula can be solved in polynomial time" would prove that P=NP. It does not mean that such a method cannot exist (proving this would prove that P<>NP), but it proves that deciding if such a method exists is hard, and has not been solved yet.
* The alternative are heuristics which decide if a formula falls into some limited set of categories for which a polynomial time solver exists, which is what you described.

**LONG ANSWER**

First, let's clarify that a list of 3-CNF formula (with $n$ variables and $m$ clauses) that can be solved in polynomial time would be exponential in $n$ and $m$: I assume below that you are asking a list of *classes* of such formula.

Second, an exact characterization of all 3-CNF formula (with $n$ variables and $m$ clauses) in the form of a "black box" which, for any input coding a 3-CNF formula "f", decides EXACTLY if "f is solvable in polynomial time" would solve the P vs NP debate, which is quite unlikely or at least very very difficult:

Given such a black box you would be able to build another black box which decides that "f is not solvable in polynomial time", which would in turn imply that P<>NP (because if P=NP, there is no such f).

I hope it helped!

> **Comments:**
> **username_0**: `The alternative are heuristics which decide if a formula falls into some limited set of categories for which a polynomial time solver exist, which already exist, and is what you describe.` Yes i was asking for a list of limited set of categories for which a polynomial time solver exist, i doubt the list that i gave in my question is complete, hence i asked whether there exist another categories of 3-CNF formula for which a polynomial time solver exist but is not in the list i gave.  
> **username_2**: But the very existence of a complete list of such categories  would imply that P=NP! Maybe, rather than asking if there exist, you want to ask if some other categories are currently known?  
> **username_0**: `you want to ask if some other categories are currently known` yes this is what i was asking, perhaps i was wrong for asking a complete list  
> **username_3**: Small formulas are easy. Large formulas are hard. So you need a measure of modest size, such as under 500 variables, as part a polynomial filter. Theorem 7.18 in Garey and Johnson where language A is small and language B is large, giving the interesting theorem.  

---

