Resynthesize linear circuit

Header: mockturtle/algorithms/linear_resynthesis.hpp

These functions resynthesize a linear circuit, i.e., a circuit that only consists of XOR gates. Currently, only XAG-like networks are supported, which include xag_network, but also views on xag_network. The underlying idea of the algorithms is to first express the input/output behavior in terms of a Boolean matrix, which is then resynthesized into a new XOR network.

The following example shows how to extract a linear subcircuit from an XAG, resynthesize it and then merge back the AND gates.

xag_network xag = ...

const auto [linxag, signals] = extract_linear_circuit( xag );
linxag = linear_resynthesis_paar( linxag );
xag = merge_linear_circuit( linxag, signals.size() );

template<typename Ntk> Ntk mockturtle::linear_resynthesis_paar(Ntk const &xag)

Linear circuit resynthesis (Paar’s algorithm)

This algorithm works on an XAG that is only composed of XOR gates. It extracts a matrix representation of the linear output equations and resynthesizes them in a greedy manner by always substituting the most frequent pair of variables using the computed function of an XOR gate.

Reference: [C. Paar, IEEE Int’l Symp. on Inf. Theo. (1997), page 250]

template<class Ntk = xag_network, bill::solvers Solver = bill::solvers::glucose_41> std::optional<Ntk> mockturtle::exact_linear_resynthesis(Ntk const &ntk, exact_linear_synthesis_params const &ps = {}, exact_linear_synthesis_stats *pst = nullptr)

Optimum linear circuit resynthesis (based on SAT)

This algorithm extracts the linear matrix from an XAG that only contains of XOR gates and no inversions and returns a new XAG that has the optimum number of XOR gates to represent the same function.

Reference: [C. Fuhs and P. Schneider-Kamp, SAT (2010), page 71-84]

template<class Ntk> std::vector<std::vector<bool>> mockturtle::get_linear_matrix(Ntk const &ntk)

Extracts linear matrix from XOR-based XAG.

This algorithm can be used to extract the linear matrix represented by an XAG that only contains XOR gates and no inverters at the outputs. The matrix can be passed as an argument to exact_linear_synthesis.

template<class Ntk = xag_network, bill::solvers Solver = bill::solvers::glucose_41> std::optional<Ntk> mockturtle::exact_linear_synthesis(std::vector<std::vector<bool>> const &linear_matrix, exact_linear_synthesis_params const &ps = {}, exact_linear_synthesis_stats *pst = nullptr)

Optimum linear circuit synthesis (based on SAT)

This algorithm creates an XAG that is only composed of XOR gates. It is given as input a linear matrix, represented as vector of bool-vectors. The size of the outer vector corresponds to the number of outputs, the size of each inner vector must be the same and corresponds to the number of inputs.

Reference: [C. Fuhs and P. Schneider-Kamp, SAT (2010), page 71-84]