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)

sugarcane4unary2.py utilizes z0 to solve a (pretty arbitrary) problem relating to farming sugarcane in Minecraft. you will need to set the environment variable SOLVER to (the path of) an external SAT solver. kissat works well.

hex_problem.py creates a hexagon grid with some colored numbers in it. it doesn't really a serve a purpose.

yices_solution.py parses a solution from a SAT solver, given the original yices-generated CNF.