Finding Efficient Circuits for Ensemble Computation
This page contains the supplemental materials for the paper
- M. Järvisalo, P. Kaski, M. Koivisto, J.H. Korhonen. Finding Efficient Circuits for Ensemble Computation. SAT 2012.
The available materials are described below.
- Generators. (download) This package contains a python library for generating proposition formulas for testing whether there exists a circuit of given size for an OR- or SUM-ensemble, as described in Section 4 of the paper. The packages also contains scripts for generating instances from various fixed families; see readme file for details. You will need bc2cnf from the BC package by Tommi Junttila to convert the generated formulas to dimacs format. One of the generator scripts also relies on Brendan McKay's nauty.
- Instances. We also provide some pre-generated CNF-SAT instances in dimacs format, created using the encoding described in the paper. Currently we have three different sets available:
- Benchmarks. (download 8 MB) Smallest satisfiable instances and largest unsatisfiable instances from the benchmarks of Section 5.3 of the paper. To replicate the complete benchmarks, use the generator provided above.
- Random. (download 12 MB) Some of the more interesting and challenging instances from the experiments with random instances (see Section 5.2 of the paper).
- Challenges. (download 18 MB) Some very large instances of the type we would like to be able to solve.
If you have trouble with the generator or if you manage to solve some of the challenge instances, contact Janne Korhonen (Janne.H.Korhonen[at]cs.helsinki.fi).