convert your constraints to CNF for SAT solver

	Name	Last modified	Size	Description
	Parent Directory		-
	example.py	2014-06-07 19:49	515
	logic.py	2014-06-07 17:58	11K
	sat.py	2014-06-07 18:57	14K

Dependency: python3, picosat solver (or compatible) if you want to solve() from python directly

Supported parsing of first-order formulas
  Example constraint you can use: (a = b → (c ≤ b ∨ d ≥ b)) ∧ (a < b ↔ c = d)

read example.py

method new_integer_variable(variable_name, lower_bound, upper_bound, encoding=BINARY|UNARY)
default encoding BINARY
lower_bound <= variable_name <= upper_bound

supported relations (variable + integer):
  a < b
  a > b
  a <= b
  a >= b
  a = b
  a != b

supported relations (variable + variable) variables must have same encoding and same bounds
  a = b
  a != b

supported operators:
  less than:         <
  greater than:      >
  less or equal:     <= ≤
  greater or equal:  >= ≥
  equals:            =
  differs:           != ≠
  negation:          ~ ! ¬
  conjunction:       & ∧
  disjunction:       | ∨
  implication:       -> →
  equivalnce:        <-> ↔

for more documentation, RTFS (read the fucking source) (for now)