2
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.