Incorrect result when using AtLeast and AtMost

[fsomenzi]

The following script produces 48 lines of output, two of which,

row 2 col 3 is safe
row 2 col 6 is safe

are incorrect (should not be there at all). If one replaces either constraint that uses AtLeast and AtMost (it does not matter which one) with an equivalent constraint that uses PbEq (currently commented out), the correct result is obtained.

""" Minesweeper deduction engine.

This script is based on Z3 (https://github.com/Z3Prover/z3) and
is inspired by Knuth's treatment.
"""

# Help to insure compatibility between python 2 and python 3.
from __future__ import print_function, division, unicode_literals
# Make all of z3 API available.
from z3 import *

# Input matrix.
matrix = [
    [' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? '],
    [' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? '],
    [' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? '],
    [' ? ',' ? ',' 2 ',' 1 ',' 1 ',' 2 ',' ? ',' ? '],
    [' ? ',' ? ',' 2 ','   ','   ',' 1 ',' ? ',' ? '],
    [' ? ',' ? ',' 1 ',' 1 ',' 1 ',' 1 ',' ? ',' ? '],
    [' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? '],
    [' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? ',' ? ']]
m = 8
n = 8
mines = 40

# Create variables and constraints.

# m x n matrix of Boolean variables.
X = [[Bool("x_%s_%s" % (i, j)) for j in range(n)] for i in range(m)]

s = Solver()

for i in range(m):
    for j in range(n):
        entry = matrix[i][j]
        if entry == ' * ':
            s.add(X[i][j])
        elif entry != ' ? ':
            s.add(Not(X[i][j]))
            # We have a number of neighboring mines: generate constraint.
            lhs = []
            # Row above current cell.
            if i > 0:
                if j > 0:
                    lhs.append(X[i-1][j-1])
                lhs.append(X[i-1][j])
                if j < n-1:
                    lhs.append(X[i-1][j+1])
            # Row of the current cell.
            if j > 0:
                lhs.append(X[i][j-1])
            if j < n-1:
                lhs.append(X[i][j+1])
            # Row below current cell.
            if i < m-1:
                if j > 0:
                    lhs.append(X[i+1][j-1])
                lhs.append(X[i+1][j])
                if j < n-1:
                    lhs.append(X[i+1][j+1])
            if entry == '   ':
                value = 0
            else:
                value = int(entry)
            constraint = And(AtMost(*lhs,value), AtLeast(*lhs,value))
            #constraint = PbEq([(x,1) for x in lhs], value)
            s.add(constraint)
            #print(i,j,constraint,'=',value) # diagnostic print

# Add cardinality constraint about number of mines.
s.add(And(AtMost(*(x for row in X for x in row), mines),
          AtLeast(*(x for row in X for x in row), mines)))
#s.add(PbEq([(x,1) for row in X for x in row], mines))

# Sanity check.
result = s.check()
if result == unsat:
    raise SystemExit("Inconsistent constraints!")
elif result == unknown:
    raise SystemExit("Unable to solve!")

# Inferences.
for i in range(m):
    for j in range(n):
        entry = matrix[i][j]
        if entry == ' ? ':
            # Check whether cell is safe by assuming X[i][j].
            result = s.check(X[i][j])
            if result == unsat:
                print('row', i, 'col', j, 'is safe')
                s.add(Not(X[i][j]))
            else:
                # Check whether cell has mine by assuming Not(X[i][j]).
                result = s.check(Not(X[i][j]))
                if result == unsat:
                    print('row', i, 'col', j, 'has a mine')
                    s.add(X[i][j])

[NikolajBjorner]

I can reproduce this. Note that when setting s = SolverFor("QF_FD") z3 uses an entirely different PB solver.

[fsomenzi]

Thanks for the tip, and glad you were able to reproduce the issue.

[NikolajBjorner]

the exposed bug has been fixed now

[NikolajBjorner]

FWIW, there is a built in method for extracting unit consequences.

_, cs = s.consequences([], [X[i][j] for i in range(m) for j in range(n) if matrix[i][j] == ' ? '])
cs = [c.arg(1) for c in cs]
for c in cs:
    print(c)

The mine-sweep example is pretty nice as an illustration. The main use cases for consequences has been in product configuration settings.