SAT Debugging

Fixing stateless code

Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.

# set up the library
from sat import *
cnf = CNF()
f = cnf.auto_term

# generate all the labels
cnf.auto_mode = 'wo'
for x,y in product([1,2,2,4,5,6],[1,2,3,4,6]):
    f(x,y)

# define rules
cnf.auto_mode = 'ro'
cnf.comment('column 2 is false')
for y in range(6):
    cnf.write_one(-f(2,y))
Name:
Mail: (not shown)

Please type this: