		Search-engine friendly clone of the ACL2 documentation.

Aignet

Aignet-cnf

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, A & B & ~C. We first convert their subcircuits to CNF and then add the three singleton clauses. Now, suppose that we have some assignment to the CIs that satisfies A & B & ~C. That induces a satisfying assignment for the generated part of the CNF where (in particular) the literals corresponding to A, B, and ~C are assigned true. That makes the three singleton clauses also true, so the whole CNF is satisfied. Therefore, if we prove the CNF unsatisfiable, then we've proven that no assignment to the CIs can simultaneously satisfy A & B & ~C.

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.

For both of these cases, we prove that the chunk we've just added preserves the correctness criterion we've described.

Subtopics

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