A collection of scripts for computing minimum-area switching lattices following the model of Altun and Riedel, using transformation to a series of SAT problems.
The scripts take input in a PLA-alike sum-of-products form, restricted to a single output. For example, the first output of the b12 circuit is encoded as:
0-110- 1 011--1 1 0101-- 1 011-0- 1To synthesize the lattice, you must first set the paths of Espresso and lingeling (or other SAT-solver) in paths.py, then run
./latsynth.py [[input_file]]Be warned, the scripts make use of Python's subprocess module; so use at your own risk. It uses relative paths, so make sure it's executed from the same directory as the other scripts.
|latsynth.tar.gz||Scripts for constructing minimum-size lattices using SAT.|
|synth_insts.tar.gz||A set of Boolean functions used for testing the synthesis method. Derived from instances in the espresso and LGSynth93 data-sets.|