1 from sat import SAT, UNARY, BINARY
    2 
    3 sat = SAT()
    4 
    5 sat.new_integer_variable('a', 0, 20)
    6 sat.new_integer_variable('b', 0, 20)
    7 sat.new_integer_variable('c', 5, 10)
    8 sat.new_integer_variable('d', 9, 10)
    9 
   10 sat.add_constraint('a < 10 -> (b > 16 | b < 2)')
   11 sat.add_constraint('(c < 6 & d = 9) -> (a = b)')
   12 
   13 sat.write_to_file('output.cnf')
   14 
   15 # or if you have picosat or compatible sat solver in /usr/local/bin/picosat
   16 if sat.solve():
   17     for i in 'abcd':
   18         print('%s = %d' % (i, sat[i]))
   19 else:
   20     print('unsatisfiable')