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

Buchtipp: “Simple Guide to Japan – Customs & Etiquette”

Simple Guide to Japan
Cover of “Simple Guide to Japan”

This booklet was published in the third edition in 1997 and authored by Helmut Morsbach. It features 80 pages in total with illustrations and a medium font size. So you should be finished in few hours. I definitely need to compare it with “Darum nerven Japaner” (engl. “Why Japanese Are Annoying”), which I read recently. However, for the latter no English translation is available.

In my humble opinion, “Why Japanese Are Annoying” does a better job at presenting Japanese habits, because it contains humorous remarks to make it more enjoyable. Due to its length (compared to the booklet) it is also more exhaustive and goes to a philosophical point of view, which is entertaining also for a non-European audience. This booklet sticks to a basic comparison of European and Japanese habits. On the other hand it comes straight to the point and introduces more basic Japanese words/phrases compared to the humorous book.

In the end you will read 10 chapters:

  1. Introduction by Ronald Dore
  2. Foreword
  3. In General
  4. Wining & Dining
  5. The Japanese Home
  6. Gift-giving
  7. Out & About
  8. Conversation & Communication
  9. Business Matters
  10. Useful Phrases & Vocabulary

The final pages contains a collection of Japanese words used in the booklet, facts about Japan and an index. A nice read for an afternoon. I cannot verify its content, because I have not been to Japan, but one disclaimer remains: In some ways outdated.

Buchtipp: “Simple Guide to Japan – Customs & Etiquette”