CNF generation

Header: mockturtle/algorithms/cnf.hpp

The following code shows how to create clauses for a SAT solver based on a network.

/* derive some XAG (can be any network type) */
xag_network xag = ...;

percy::bsat_wrapper solver;
const auto output_lits = generate_cnf( xag, [&]( auto const& clause ) {
  solver.add_clause( clause );
} );
template<class Ntk, typename lit_t = uint32_t>
node_map<lit_t, Ntk> mockturtle::node_literals(Ntk const &ntk, std::optional<uint32_t> const &gate_offset = {})

Create a default node literal map.

In the default map, constants are mapped to variable 0 (literal 1 for constant-1 and literal 0 for constant-0). Then each primary input is mapped to variables 1, ..., n. Then the next variables are assigned to each gate in order, unless gate_offset is overridden which will be used for the next variable id. Therefore, this function can be used to create two independent sets of node literals for two networks, but keep the same indexes for the primary inputs.

template<class Ntk, typename lit_t = bill::lit_type>
std::vector<lit_t> mockturtle::generate_cnf(Ntk const &ntk, clause_callback_t<lit_t> const &fn, std::optional<node_map<lit_t, Ntk>> const &node_lits = {})
template<class Ntk>
std::vector<uint32_t> mockturtle::generate_cnf(Ntk const &ntk, clause_callback_t<uint32_t> const &fn, std::optional<node_map<uint32_t, Ntk>> const &node_lits = {})

Generates CNF for a logic network.

This function generates a CNF for a logic network using the Tseytin encoding for regular gates and ISOP-based CNF generation for arbitrary node functions.

Input to the function are the network ntk and a clause callback function fn. For each clause that is generated, fn is called. A clause is represented as a vector of literals std::vector<uint32_t>, following the customary literal convention, i.e., for a variable v its positive literal is 2 * v and its negative literal is 2 * v + 1. The third optional parameter can be used to pass an alternative mapping of nodes to literals. If none is given, it uses the default literal map created with the node_literals function.

The return value of the function is a vector with a literal for each primary output in the network, following the same order as the primary outputs have been created.

Parameters:

  • ntk – Logic network

  • fn – Clause creation function

  • node_lits – (optional) custom node literal map

template<class lit_t>
using mockturtle::clause_callback_t = std::function<void(std::vector<lit_t> const&)>

Clause callback function for generate_cnf.