Skip to main content
Theoretical Computer Science

Return to Answer

replaced http://cstheory.stackexchange.com/ with https://cstheory.stackexchange.com/
Source Link
Community Bot
Community Bot
  • 1

(I was going to add a quick comment, but I'm not being allowed to.)

If you take into account equi-satisfiability, then you can get lots more Horn formulas. For example, considering $\phi \equiv (p \lor q)$, there is a reduction from $\phi$ to a Horn formula. See my answer under Translating SAT to HornSATTranslating SAT to HornSAT.

If you try using the above technique to reduce an arbitrary 3-SAT formula to a Horn formula, you cannot do it in poly time -- since two 3-clauses resolve to a 4-clause, two 4-clauses resolve to a 6-clause, and so on... the result is an exponential number of clauses.. but I digress.. I'm going off-topic, so let me stop here.

(I was going to add a quick comment, but I'm not being allowed to.)

If you take into account equi-satisfiability, then you can get lots more Horn formulas. For example, considering $\phi \equiv (p \lor q)$, there is a reduction from $\phi$ to a Horn formula. See my answer under Translating SAT to HornSAT.

If you try using the above technique to reduce an arbitrary 3-SAT formula to a Horn formula, you cannot do it in poly time -- since two 3-clauses resolve to a 4-clause, two 4-clauses resolve to a 6-clause, and so on... the result is an exponential number of clauses.. but I digress.. I'm going off-topic, so let me stop here.

(I was going to add a quick comment, but I'm not being allowed to.)

If you take into account equi-satisfiability, then you can get lots more Horn formulas. For example, considering $\phi \equiv (p \lor q)$, there is a reduction from $\phi$ to a Horn formula. See my answer under Translating SAT to HornSAT.

If you try using the above technique to reduce an arbitrary 3-SAT formula to a Horn formula, you cannot do it in poly time -- since two 3-clauses resolve to a 4-clause, two 4-clauses resolve to a 6-clause, and so on... the result is an exponential number of clauses.. but I digress.. I'm going off-topic, so let me stop here.

Source Link
Martin Seymour
Martin Seymour
  • 283
  • 2
  • 6

(I was going to add a quick comment, but I'm not being allowed to.)

If you take into account equi-satisfiability, then you can get lots more Horn formulas. For example, considering $\phi \equiv (p \lor q)$, there is a reduction from $\phi$ to a Horn formula. See my answer under Translating SAT to HornSAT.

If you try using the above technique to reduce an arbitrary 3-SAT formula to a Horn formula, you cannot do it in poly time -- since two 3-clauses resolve to a 4-clause, two 4-clauses resolve to a 6-clause, and so on... the result is an exponential number of clauses.. but I digress.. I'm going off-topic, so let me stop here.