Encoders

knuth_encoder

The knuth_encoder class is based on the exact synthesis formulation developed by That implementation is itself based on earlier work by Éen 1 and Knuth 2.

Warning

doxygenclass: Cannot find class “percy::knuth_encoder” in doxygen xml output for project “percy” from directory: xml

fence_encoder

The fence_encoder is intended to be used by a synthesizer that generates families of DAG topologies, also known as fences.

class fence_encoder : public percy::encoder

Subclassed by percy::ssv_fence2_encoder, percy::ssv_fence_encoder

dag_encoder

The fence_encoder is intended to be used by a synthesizer that generates DAGs. Encoding DAGs requires much fewer variables, since their structure is completely fixed.

template<int FI>
class dag_encoder : public percy::encoder

Subclassed by percy::ssv_dag_encoder< FI >

1

Niklas Éen, “Practical SAT – a tutorial on applied satisfiability solving,” 2007, slides of invited talk at FMCAD.

2

Donald Ervin Knuth, “The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability,” 2015