Add QBF example programs using DepQBF

aswiridoff commented 2 months ago

I added two example programs (Coloring.hs, Synthesis.hs) to examples/qbf. The first one solves a graph coloring problem, and the second one solves a circuit synthesis problem.

jwaldmann commented 2 months ago

just as a general comment: I endorse this PR.

ersatz can encode QBFSAT, but did not have any test case so far (that I know of).
I can use this in teaching
the circuit synthesizer could be helpful to find smaller formulas for some operations in Ersatz.Bits, Ersatz.Counting, or other numerical encodings.

This needs depqbf installed (version >= 6.03? this should be checked, and be mentioned someplace), which needs to be built from source (Debian packages depqbf-5.01, Fedora does not have it at all).

RyanGlScott commented 2 months ago

Yes, the need for a specific version of depqbf is unfortunate. I wonder if there is a way we can query the version number and pass different default flags to depqbf to make it work for both old and new versions. (This isn't something that we need to do in this PR, but it would be a nice improvement for later.)

ekmett / ersatz

Add QBF example programs using DepQBF #93