boolean_circuit

Function generate_cnf

Source 
pub fn generate_cnf<'a>(
    gate: &'a Gate,
    new_var: &mut impl FnMut() -> String,
) -> impl Iterator<Item = Vec<Literal>> + 'a
Expand description

Turns the circuit represented by the ouput gate gate into a conjunctive normal form (CNF) formula.

The function uses the Tseitin transformation, so it needs a way to generate new unique variables, which is done by the function new_var.

Parameters

  • gate: The output gate of the circuit.
  • new_var: A function that can be used to generate new unique variable names. Each call has to return a new variable name not returned before and not used in the circuit.

Returns an iterator over the clauses of the CNF formula. Each clause is a vector of literals.