Discussion of CNF generation for aignets.

Generating CNF from a circuit representation is pretty simple to write, but the correctness conditions are tricky to state.

Basically, we want to show that a SAT proof corresponds to a proof about the AIG, and a SAT counterexample corresponds to a counterexample in the AIG.

Taking the proof case first. We want to show that if the CNF is unsatisfiable, then -- what? Well, the CNF we produce from just the circuit will always be satisfiable: in fact, this is the first thing we'll prove --

Every assignment of values to the CIs of the AIG can be translated to a satisfying assignment of the generated CNF by setting, for every circuit node that is assigned a SAT variable, the evaluation of the node to be the value of the variable.It's when we add additional constraints to the CNF that it may become unsatisfiable. So suppose we want to show that some cube among the nodes of the circuit is unsat -- say,

Now the counterexample case. We want to show that any satisfying assignment of the CNF is a satisfying assignment for whatever circuit constraints we've added to it. Basically, this amounts to:

Every satisfying assignment to the generated CNF induces an assignment to the CIs of the circuit, under which, for every circuit node assigned a SAT variable, the value of the SAT literal is the same as the evaluation of the circuit node.Of course, this theorem is less critical to correctness -- if we get a SAT counterexample, it can easily be verified on the circuit. Still, we'd like to prove it to show that our CNF generation is correct.

To summarize, we need to show:

An evaluation of the circuit induces a satisfying assignment, and a satisfying assignment induces an evaluation of the circuit, in which the evaluations of circuit nodes that are assigned SAT literals is the same as the values of those literals under the satisfying assignment.

To formalize this, we'll define:

- a predicate
aignet-vals-agree-with-cnf which compares a satisfying assignment to an aignet evaluation to determine whether all values agree as specified above, - a function
cnf->aignet-vals that transforms a satisfying assignment into a vals object. We'll show that the input and output satisfy`cnf/aignet-evals-agree`if the assignment satisfies the generated CNF. - a function
aignet->cnf-vals that creates a CNF variable assignment from a vals object. We'll show that this satisfies`cnf/aignet-evals-agree`and that the CNF assignment satisfies the generated CNF.

When actually converting an aignet to CNF, we of course process the AIG recursively. We do this in chunks, where each chunk is either:

- a
*supergate*, representing a single large AND or OR gate, or - a mux.

- Aignet-lit->cnf
- Add clauses encoding the fanin cone of literal
x of the aignet to the cnf. - Aignet-ipasir
- Using the ipasir interface to run SAT checks on aignet nodes