# list of 3-CNF formula that can be solved in polynomial time

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

• Both ordinary Horn formulas and dual Horn formulas are subsumed by renamable Horn formulas. What do you mean by renamable dual Horn formulas? Aug 27, 2022 at 18:14
• Also, renaming a XOR formula just yields another XOR formula. So what do you mean by renamable XOR formula? Aug 27, 2022 at 18:33
• @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
Aug 28, 2022 at 16:24
• 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. Aug 29, 2022 at 5:35
• @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
Aug 29, 2022 at 5:56

• 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.

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!

• 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
Aug 28, 2022 at 16:51
• 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? Aug 28, 2022 at 20:08
• 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
Aug 29, 2022 at 4:21
• 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. Aug 30, 2022 at 16:53