latsynth - Synthesizing switching lattices

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 are known to work with version of Espresso included in the unofficial release of Berkeley SIS 1.3.6; other versions may work, although getting them to compile on recent compilers may be painful.

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- 1
To synthesize the lattice, you must first set the paths of Espresso and lingeling (or other SAT-solver) in, then run
    ./ [[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.

File Description
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.


Graeme Gange