Add and Fix Game-of-Life, Hamiltonian, and QBF for Grendel - Githubissues

SSoelvsten / bdd-benchmark

Benchmarking Suite for BDD packages

MIT License

11 stars 2 forks source link

Add and Fix Game-of-Life, Hamiltonian, and QBF for Grendel #100

Closed SSoelvsten closed 9 months ago

SSoelvsten commented 9 months ago

Game of Life

[x] Fix 'easy' symmetry quantification for mirror-double_diagonal ( closes #93 )
[x] Fix 'easy' symmetry quantification for rotate-90 ( closes #93 )
[x] Fix final total time lacks precision
[x] Add Grendel timings for Game of Life

Hamiltonian

[x] Fix indentation and lingering debug printing
[x] Add Grendel timings for Hamiltonian with Heule's & Bryant's n²log(n) encoding.
[x] Update Grendel timings for Hamiltonian with Bryant's n⁴ encoding

QBF

[x] Merges prenex quantifiers. Even though, in Jaco's experience, this is not always a good thing to do, it fits better with the goal of our experiments (closes #99).
[x] Moved TODOs into #78 .
[x] Fix Debug mode assertions.
[x] Ensure STATS outputs are flushed. This way, one has a working "progress bar"
[ ] Add Grendel timings for QBF

Other

[x] Extend Grendel script with partitions (default q48)
[x] Set memory limit to maximum of whatever the node has ( closes #63 )
[x] Small fixes and improvements to the Makefile