2022-06-07 19:27:22 -07:00
|
|
|
satisfy them booleans, solve them integers.
|
2022-06-07 19:54:47 -07:00
|
|
|
|
|
|
|
|
`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](https://github.com/Z3Prover/z3)
|
|
|
|
|
library's interface. it exposes classes for high-level bitvectors and
|
|
|
|
|
[unary-encoded integers.](https://en.wikipedia.org/wiki/Unary_numeral_system)
|
|
|
|
|
(unary is sometimes more efficient to solve)
|
2022-06-07 20:28:51 -07:00
|
|
|
|
|
|
|
|
`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](https://github.com/arminbiere/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.
|
