hilben/sudoku-dimacs-creator

Missing clauses under "each number at most once in each block"

Opened this issue · 0 comments

grlks commented

There is a typing error in line 70 (the first 1 should be an i). This is easy to fix.

The result is that the clauses like -136 -316 0 appear twice or more while -236 -316 0 is missing. This means that the constraint "each number at most once in each block" is not fully implemented–6 may appear in (2,3) and (3,1).
However, I have not prepared a dedicated counter example where minisat would return a wrong assignment.