An empty clause represents a contradiction

The problem

I have just gone through many CNF files and come across the following file:

p cnf  150  400
     -3      -2      -1 0
      3       2      -1 0
      2       1      -3 0
[...]
    150     149      98 0
    150    -149     -98 0
    149    -150     -98 0
     98    -150    -149 0
0

available as pret150_25.cnf and originally authored by Daniel Pretolani.

To those unfamiliar with DIMACS CNF files, this file represents the boolean formula defined as

f(x1, x2, …, x150) =
(-x3 ∨ -x2 ∨ -x1) ∧
(x3 ∨ x2 ∨ -x1) ∧
(x2 ∨ x1 ∨ -x3) ∧

(x150 ∨ x149 ∨ x98) ∧
(x150 ∨ -x149 ∨ -x98) ∧
(x149 ∨ -x150 ∨ -x98) ∧
(x98 ∨ -x150 ∨ -x149)

So 0 terminates clauses which are disjunctions (denoted with ) of literals.
However, the trailing 0 triggers the question whether the boolean function actually ends with

∧ (x98 ∨ -x150 ∨ -x149) ∧ ()

or as before:

∧ (x98 ∨ -x150 ∨ -x149)

Rationale

If the former is satisfied, the question is raised, what an empty clause means. Considering that

(x98 ∨ -x150 ∨ -x149)
= (x98 ∨ -x150 ∨ -x149 ∨ ⊥)
= (x98 ∨ -x150 ∨ -x149 ∨ ⊥ ∨ ⊥ ∨ ⊥)

where ⊥ denotes boolean value false, this should apparently mean

()
= (⊥)
= (⊥ ∨ ⊥ ∨ ⊥)

This is the rationale why an empty clause should represent the boolean value false (in my humble opinion). Thus rendering the CNF file above with the former notation and specifically the problem unsatisfiable.

An empty clause represents a contradiction

2 thoughts on “An empty clause represents a contradiction

  1. Toxa says:

    “p cnf 150 400” means that CNF parser would need to read the next 400 lines/clauses, and I assume (as you skipped some clauses) that the last “0” is located on the line 401, so the parser simply won’t read it.

    But yeah, empty clause is always false, because there are no literals to satisfy it.

Leave a Reply

Your email address will not be published. Required fields are marked *