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
>
classdag_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