0
$\begingroup$

To show that any formal language is NP Complete first it must be showed that this formal language is both in NP and NP Hard.

So to show that Horn Satisfiability is NP Complete first it must be showed that Horn Satisfiability is both in NP and NP Hard.

Horn Satisfiability is definitely in NP because Horn Satisfiability is in P thanks to the Horn algorithm which decides it in deterministic linear time and it is well known that P is a subset of NP so every member of P is also a member of NP thus Horn Satisfiability is in NP.

To show that any formal language is NP Hard first it must be showed that a well known NP Hard formal language can be reduced to that formal language in deterministic polynomial time.

3-Satisfiability is a well known NP Hard formal language and this means that if 3-Satisfiability can be reduced to Horn Satisfiability in deterministic polynomial time then Horn Satisfiability is NP Hard.

There is a deterministic polynomial time reduction from 3-Satisfiability to Horn Satisfiability and this is how it works:

For each subset of 2 different clauses exactly that both contain 3 different literals exactly and own a common literal $l$:

Replace the second $l$ in this subset by $a$ where $a$ is a fresh new variable introduced to the given formula and add the following clauses:

$\lnot l\lor a$

$l\lor\lnot a$

For example if both $p\lor q\lor r$ and $r\lor s\lor t$ clauses were found, a subset of the given formula, because these two clauses both contain $r$ then let's introduce a new fresh variable $a$ and replace the second $r$ with it and after adding the two clauses that have to be added after that then this subset becomes:

$(p\lor q\lor r)\land(a\lor s\lor t)\land(\lnot r\lor a)\land(r\lor\lnot a)$

And for each subset of 2 different clauses exactly that both contain 3 different literals exactly and one owns $l$ and the other owns $\lnot l$:

Replace $\lnot l$ in this subset with $a$ where $a$ is a fresh new variable introduced to the given formula and add the following clauses:

$l\lor a$

$\lnot l\lor\lnot a$

For example if both $p\lor q\lor r$ and $\lnot r\lor s\lor t$ clauses were found, a subset of the given formula, because the first clause contains $r$ and the second clause contains $\lnot r$ then let's introduce a new fresh variable $a$ and replace $\lnot r$ with it and after adding the two clauses that have to be added after that then this subset becomes:

$(p\lor q\lor r)\land(a\lor s\lor t)\land(r\lor a)\land(\lnot r\lor\lnot a)$

These must be done while the formula contains 2 different clauses that both contain 3 different literals exactly that both have at least one literal in common or one have any literal and the other has it's negated.

After doing all this the new 3-Satisfiability formula we get is definitely not equivalent to the given 3-Satisfiability formula but the new formula is definitely equisatisfiable to the given formula.

Of course that the new formula is not a Horn formula but it can be transformed into an equisatisfiable Horn formula in deterministic polynomial time by doing the following:

For each clause $p\lor q\lor r$ add the following clauses:

$\lnot p\lor\lnot p\implies q\lor r$

$\lnot q\lor\lnot q\implies p\lor r$

$\lnot r\lor\lnot r\implies p\lor q$

$(\lnot p\lor\lnot p)\land(\lnot q\lor\lnot q)\implies(r\lor r)$

$(\lnot p\lor\lnot p)\land(\lnot r\lor\lnot r)\implies(q\lor q)$

$(\lnot q\lor\lnot q)\land(\lnot r\lor\lnot r)\implies(p\lor p)$

$(\lnot p\lor\lnot p)\land(\lnot q\lor\lnot q)\land(\lnot r\lor\lnot r)\implies\bot$

Where $\bot$ is the constant false

$\lnot p\lor q\implies q\lor r$

$\lnot p\lor r\implies q\lor r$

$\lnot q\lor p\implies p\lor r$

$\lnot q\lor r\implies p\lor r$

$\lnot r\lor p\implies p\lor q$

$\lnot r\lor q\implies p\lor q$

And for each literal $s$ in addition to the clause $p\lor q\lor r$:

$(\lnot p\lor s)\land(\lnot q\lor s)\implies r\lor s$

$(\lnot p\lor s)\land(\lnot r\lor s)\implies q\lor s$

$(\lnot q\lor s)\land(\lnot r\lor s)\implies p\lor s$

$(\lnot p\lor s)\land(\lnot q\lor s)\land(\lnot r\lor s)\implies s\lor s$

And for each 2 different clauses $a\lor b\lor c$ and $d\lor e\lor f$ add the following clause:

$(a\land d)\lor (a\land e)\lor (a\land f)\lor (b\land d)\lor (b\land e)\lor (b\land f)\lor (c\land d)\lor (c\land e)\lor (c\land f)$

which is equivalent to

$(\lnot a\lor\lnot d)\land(\lnot a\lor\lnot e)\land(\lnot a\lor\lnot f)\land(\lnot b\lor\lnot d)\land(\lnot b\lor\lnot e)\land(\lnot b\lor\lnot f)\land(\lnot c\lor\lnot d)\land(\lnot c\lor\lnot e)\land(\lnot c\lor\lnot f)\implies\bot$

Where $\bot$ is the constant false

And after doing all this with all the clauses that contains 3 different literals exactly then all clauses that contains 3 different literals exactly can be removed from the formula because they have already served their purpose at this time and they no longer needed anymore.

Now for each unit clause presented in the formula $l$ replace it by it's equivalent $l\lor l$

And for each proposition (variable) presented in the formula $p$ add the following clause:

$(p\lor p)\land(\lnot p\lor\lnot p)\implies\bot$

Where $\bot$ is the constant false

And for each 2 literals $p$ and $q$ add the following clauses:

$p\lor q\implies q\lor p$

And for each 3 literals $p$, $q$ and $r$ add the following clause:

$(p\lor\lnot q)\land(q\lor r)\implies p\lor r$

And now if for each 2 literals $p$ and $q$ you treat $p\lor q$ as a single proposition or variable then the whole formula becomes a Horn formula which is definitely not equivalent to the given 3-Satisfiability formula at all but it is indeed equisatisfiable to the given 3-Satisfiability formula!

And this is all the reduction from 3-Satisfiability to Horn Satisfiability!

This reduction is indeed not linear time at all but we can see that it is definitely at most polynomial time and the algorithm that does this reduction is indeed deterministic which is by definition is sufficient to prove that $\text{3SAT}\le_P\text{HornSAT}$ by definition.

Since 3-Satisfiability is a NP Hard formal language then thus Horn Satisfiability is also NP Hard formal language thanks to the reduction presented above.

And if a formal language is both in NP and NP Hard then the formal language is NP Complete by definition which means that Horn Satisfiability formal language is NP Complete!

End of proof

Is that correct?

$\endgroup$
8
  • 2
    $\begingroup$ $l \lor a$ is not a Horn clause. $\endgroup$ Commented Jun 10, 2022 at 12:05
  • $\begingroup$ If for each 2 literals $p$ and $q$ you treat $p v q$ as a single proposition or variable then the whole formula becomes a Horn formula. I have already said that right after inroducing $a$ the new formula is not Horn. Read what I said carefully. $\endgroup$ Commented Jun 10, 2022 at 15:22
  • 2
    $\begingroup$ Horn-SAT is in P, so it is extremely unlikely to be NP-complete. Whatever argument you have in mind, it has a mistake. $\endgroup$ Commented Jun 10, 2022 at 15:48
  • 1
    $\begingroup$ Checking the correctness of proofs is not really a good fit for this site. I think it's asking a lot to ask someone to read that entire post just to find the flaw (which undoubtedly exists). A critical part of our mission is building up an archive of knowledge that will be useful to others, by compiling high-quality questions and their answers. It seems unlikely to me that this question will ever be of interest to anyone else. $\endgroup$
    – D.W.
    Commented Jun 10, 2022 at 18:17
  • 2
    $\begingroup$ If you believe this works, I suggest you code it up, combine it with an off-the-shelf HornSAT solver (which runs in linear time), and use it to build a SAT solver. If you are right, your SAT solver will be able to solve SAT instances that no other SAT solver can -- such a challenge instances based on factoring, and difficult instances from recent SAT solver competitions. If you are wrong, that exercise might help you identify where you went wrong. I suggest you spend the time to do that, if you'd like to know were you've went wrong. $\endgroup$
    – D.W.
    Commented Jun 10, 2022 at 18:19

0

Your Answer

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