backyard/logic

satisfy them booleans, solve them integers.

cnf.py is a small library for creating formulas in conjunctive normal form, and also for dealing with the eponymous CNF file format. the types used internally and exposed externally are very simple: booleans, integers, and lists of each.

z0.py is a slightly larger library that builds upon cnf.py, mimicing a tiny subset of the z3 library's interface. it exposes classes for high-level bitvectors and unary-encoded integers. (unary is sometimes more efficient to solve)