# Is this possible to solve 4SAT in polynomial time? [closed]

I think that this is one of the most interesting questions asked in computer science ever.

I don't expect for quick answers. Take your time to read slowly and to understand everything. I can wait. I don't rush.

In 1SAT, the turing machine needs to determine whether or not a 1CNF formula is satisfiable or not, where 1CNF formula is conjunction of clauses, where each clause is 1 literal only, which is either positive or negative variable.

This problem is known to be in $\Bbb{P}$, the class of all problems solvable in polynomial time, but it's not NP-Complete problem at all.

In 2SAT, the turing machine needs to determine whether or not a 2CNF formula is satisfiable or not, where 2CNF formula is conjunction of clauses, where each clause is disjunction of 2 literals at most, where each literal is either positive or negative variable.

Interesting is that if you turn out every disjunction into conjunction in the given 2CNF formula, then you get 1CNF formula and the problem becomes 1SAT, which is already known to be in $\Bbb{P}$ and if this formula is satisfiable, then the original 2CNF formula is satisfiable as well, but if the given 1CNF formula is unsatisfiable, this is not necessarily means that the original 2CNF formula is unsatisfiable as well.

Because the fact that in the original 2CNF formula you have disjunction between each pair of literals, instead of conjunction, you can allow one of the literals to be false in the input, but not both. So if it is not possible to set both literals to true in the same clause so the 2CNF formula evaluates to true, then the algorithm or turing machine has to decide which of them should be false, so the 2CNF formula evaluates to true.

Indeed this is a decision problem, but it's known to be in $\Bbb{P}$ as well, because it is possible just to build implications graph and finding contradiction circle to prove that the 2CNF formula is unsatisfiable. If no contradiction circle is found, then the 2CNF formula is satisfiable.

So even though from 1SAT to 2SAT the problem becomes decision problem (which literal in each clause should be set to false), the turing machine still can solve it deterministically in polynomial time, but unfortunately 2SAT isn't NP-complete too.

In 4SAT, the turing machine needs to determine whether or not a 4CNF formula is satisfiable or not, where 4CNF formula is conjunction of clauses, where each clause is disjunction of 4 literals at most, where each literal is either positive or negative variable.

Interesting is that if you turn out every disjunction into conjunction in the given 4CNF formula, then you get 1CNF formula and the problem becomes 1SAT, which is already known to be in $\Bbb{P}$, and if the given 1CNF formula is satisfiable, then the original 4CNF formula is satisfiable as well, but if the 1CNF formula is unsatisfiable, it doesn't necessarily mean that the 4CNF formula is unsatisfiable as well.

So in that case the algorithm or turing machine will have to go back to the original 4CNF formula and in each clause turn out the middle disjunction into conjunction, i.e. if

(l1 ∨ l2 ∨ l3 ∨ l4) is arbitrary clause from arbitrary 4CNF formula, then the meaning of turning out the middle disjunction into conjunction is to turn that arbitrary clause to (l1 ∨ l2) ∧ (l3 ∨ l4).

If you do that, then you get 2CNF formula and the problem becomes 2SAT, which is also known to be in $\Bbb{P}$, and if this 2CNF formula is satisfiable then the original 4CNF formula is satisfiable as well, but if the 2CNF formula is unsatisfiable then it doesn't necessarily mean that the original 4CNF formula is unsatisfiable as well, because in the original 4CNF formula there is disjunction between the two pairs of literals, but not conjunction, so the turing machine doesn't have to find an input, so both the pairs of literals evaluate to true, but it's enough if one of them evaluates to true and the other evaluates to false.

As you can see 4SAT is decision problem as 2SAT is, which pair of literals should evaluate to false in each clause and which shouldn't, i.e. should evaluate to true.

This question is similar to the previous one, when the turing machine has to solve 2SAT and it needs to determine which literal should be false in each clause, instead of pair, but turing machine can solve 2SAT deterministically in polynomial time by building implications graph and trying to find contradiction circle, so it doesn't have to determine which literal should be false in each clause.

Same here with 4SAT, I don't think that the turing machine has to decide which pair of literals should evaluate to false in each clause.

I believe that there is a method that the turing machine can do deterministically to solve 4SAT in polynomial time, maybe similar to the method to solve 2SAT in polynomial time.

I don't think that 4SAT is so difficult problem.

When you turn out the middle disjunction to conjunction in each clause, you get 2CNF formula and the turing machine can deterministic-ally build the implications graph for it in polynomial time.

If the turing machine doesn't find contradiction circle, then the original 4CNF formula is satisfiable.

But if the turing machine did find contradiction circle, then the turing machine will have to modify the graph, so there is no contradiction circle in the graph.

If there is a way to do this modification, so there is no contradiction circle in the graph, then the 4CNF formula is satisfiable, even though the given 2CNF formula isn't.

But if the turing machine proves that does not exist such modification to the implications graph, so every contradiction circle can be resolved, then the original 4CNF formula is unsatisfiable.

In each 4CNF clause, deciding which pair of literals should be true and which should be false is to decide which edge should be in the implications graph and which edge shouldn't be in the implication graph.

If the turing machine assumes that all pairs can be true, then all edges are in the graph, but then if it finds contradiction circle, then to decide in each clause which pair of literals should be false is to decide which edge should be removed from the implications graph, so there is no contradiction.

Interesting that moving from 1SAT to 2SAT, the problem becomes decision problem, but both 1SAT and 2SAT aren't np-complete, even though both can be solved in polynomial time.

When moving from 2SAT to 4SAT, the problem again becomes decision problem, but 4SAT is np-complete, unlike 2SAT, because boolean satisfiability problem, which was the first problem to be proved np-complete in cook's and karp's paper, can be reduced to 4SAT in polynomial time.

My interesting question is can turing machine solves 4SAT deterministic-ally in polynomial time as it can in 2SAT?

I don't think that the turing machine really needs to decide in each clause which edge should be removed from the implications graph as in 2SAT the turing machine doesn't have to decide which literal should be false in each clause.

I think there should be a much efficient method that the turing machine can use to solve 4SAT deterministic ally in polynomial time as it does in 2SAT.

What do you think?

## closed as primarily opinion-based by Tom van der Zanden, Yuval Filmus, Kyle Jones, Juho, EvilJul 18 '17 at 17:12

Many good questions generate some degree of opinion based on expert experience, but answers to this question will tend to be almost entirely based on opinions, rather than facts, references, or specific expertise. If this question can be reworded to fit the rules in the help center, please edit the question.

• "if the 2CNF formula is unsatisfiable then it doesn't necessarily mean that the original 4CNF formula is unsatisfiable" - this is the case. It does not solve all instances, so, it does not give an idea to solve 4SAT. – rus9384 Jul 18 '17 at 11:27
• Note that he outlines some idea how to get around that by having the algorithm pick which clauses don't need to be satisfied, but he does not go into details how those decisions are made, nor does he give more details on that algorithm. Therefore the complexity is unknown, and the actual challenge remains unsatisfied. – Mike B. Jul 18 '17 at 12:31
• It is very probable that 4SAT cannot be solved in polynomial time. Unfortunately P=NP proofs are beyond the scope of this site. – Yuval Filmus Jul 18 '17 at 15:05
• What exactly is your question? We need a specific, answerable, technical question about CS. "What do you think?" is not specific enough. "What is your opinion?" is not specific enough, and we don't deal in opinions; subjective questions and open-ended invitations to discussion aren't a good fit here (see our help center). "Can a Turing machine solve 4SAT in polynomial time?" isn't something anyone here can answer, as it's an open problem whose answer is not known. The rest is speculation about an algorithm that you think will work, but you don't ask any question about that algorithm. – D.W. Jul 18 '17 at 16:04
• It sounds like maybe you are claiming to have a solution for a well-known, difficult open problem. This is an extraordinary claim requiring extraordinary evidence. You have not provided such so there is not much to talk about. Even if you had, this would not be a good post for SE; it is not our goal here to make broad advances to science in a single post. See here for a related discussion. – D.W. Jul 18 '17 at 16:05

The problem is that when you split your clauses, you don't transform your $4SAT$ problem to a $2SAT$ problem. You still have an $NP$-complete problem to which an efficient $2SAT$-algorithm cannot be applied. You need to prove separately that your new problem is in $P$.