patternMinor
Definition of 2-CNF (a.k.a Krom) formula
Viewed 0 times
definitionkromformulacnf
Problem
In my lecturer's notes, the following definition for a 2-CNF wff is given:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is no mention in the notes of how one might represent clauses containing a single literal L in the wff's corresponding implication graph (although I suppose one could add an edge from every other literal to L). Looking at Krom's original paper, the definition he seems to use is:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has exactly two literals.
This definition would seem to make a lot more sense. Which definition is correct? Am I missing something?
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is no mention in the notes of how one might represent clauses containing a single literal L in the wff's corresponding implication graph (although I suppose one could add an edge from every other literal to L). Looking at Krom's original paper, the definition he seems to use is:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has exactly two literals.
This definition would seem to make a lot more sense. Which definition is correct? Am I missing something?
Solution
A unit clause of the form $p$ is the same as the clause $p \lor p$, and so corresponds to the arrow $\lnot p \to p$.
As an example, consider the unsatisfiable CNF
$$ p \land (\lnot p \lor q) \land \lnot q. $$
The implication graph contains the following edges:
$$
\lnot p \to p \\
p \to q,
\lnot q \to \lnot p \\
q \to \lnot q
$$
These can be arranged in a cycle:
$$
\lnot p \to p \to q \to \lnot q \to \lnot p
$$
This cycle contains both $p$ and $\lnot p$ (and also both $q$ and $\lnot q$), showing that the formula is unsatisfiable.
As an example, consider the unsatisfiable CNF
$$ p \land (\lnot p \lor q) \land \lnot q. $$
The implication graph contains the following edges:
$$
\lnot p \to p \\
p \to q,
\lnot q \to \lnot p \\
q \to \lnot q
$$
These can be arranged in a cycle:
$$
\lnot p \to p \to q \to \lnot q \to \lnot p
$$
This cycle contains both $p$ and $\lnot p$ (and also both $q$ and $\lnot q$), showing that the formula is unsatisfiable.
Context
StackExchange Computer Science Q#121943, answer score: 3
Revisions (0)
No revisions yet.