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

Question

I know and admit that this is long, but please read it slow and understand everything.

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

(l₁ ∨ l₂ ∨ l₃ ∨ l₄) 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 (l₁ ∨ l₂) ∧ (l₃ ∨ l₄).

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?

What is your opinion?