notwa/backyard
1
0
Fork 0
Code Issues Pull requests Releases Activity

logic: update readme

Browse source
This commit is contained in:
Connor Olding 2022-06-08 05:28:51 +02:00
parent b8d048a974
commit 3d7f0b4460
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
logic/README.md
View file

@ -10,3 +10,14 @@ 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)
`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.