0
$\begingroup$

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

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Both ordinary Horn formulas and dual Horn formulas are subsumed by renamable Horn formulas. What do you mean by renamable dual Horn formulas? $\endgroup$
    – Emil Jeřábek
    Aug 27, 2022 at 18:14
  • $\begingroup$ Also, renaming a XOR formula just yields another XOR formula. So what do you mean by renamable XOR formula? $\endgroup$
    – Emil Jeřábek
    Aug 27, 2022 at 18:33
  • $\begingroup$ @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. $\endgroup$
    – LLL
    Aug 28, 2022 at 16:24
  • $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Aug 29, 2022 at 5:35
  • $\begingroup$ @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. $\endgroup$
    – LLL
    Aug 29, 2022 at 5:56

1 Answer 1

Reset to default
-1
$\begingroup$

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!

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ 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. $\endgroup$
    – LLL
    Aug 28, 2022 at 16:51
  • 1
    $\begingroup$ 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? $\endgroup$
    – J..y B..y
    Aug 28, 2022 at 20:08
  • $\begingroup$ 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 $\endgroup$
    – LLL
    Aug 29, 2022 at 4:21
  • $\begingroup$ 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. $\endgroup$
    – daniel pehoushek
    Aug 30, 2022 at 16:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.