ABC SAT

Equivalence checking with SAT

ABC uses MiniSAT to solve the SAT problem. You can learn MiniSAT and download it from the source given below. Typical usage of ABC for combinational equivalence includes commands: miter; sat (or dsat); write_cex; or "dsat -w" for writing out the result into a file in case of satisfiable instance. If the result is unSAT:

If the result is SATisfiable, you can write the result into a file, but only if this was generated from the circuit miter:

Alternatively, and this is a better choice in case when you are solving a SAT problem directly from the CNF formula, you can use "dsat -w":

More details on this topic are given later below.

Solving SAT on a CNF formula

You can also run ABC SAT on a CNF file created independently from the miter, for example for a single circuit or for some formula you need to satisfy. In this case you will first need to save the circuit (or your blif file) into an AIG format, called AIGER before converting it to CNF and applying the sat or dsat command. In the following, f_multi.blif is a multiple-output function.

Then you can generate CNF and run the SAT tool In case of a multiple-output function, ABC considers each output as individual miter, and applies an OR to these outputs. If your intention is to create a CNF instance of a multiple-output circuit, you need to generate the CNF without an OR; this is what the option "-o" before the output CNF file (f_multi.cnf above) is about.

You can then fix the polarity of the outputs by appending the CNF file with the respective assignment, for example:

where numbers 2, 3 refer to the variable IDs of the first two outputs in this example. Here the first output is set to 0 (negative polarity, literal -2) and the second output is set to 1 (positive polarity, literal 3).

ABC conveniently generates the outputs as first variables, followed by the internal signals and inputs in topological order. This way, the first N variables (starting with 2) represent N outputs. They are ordered in the order in which they appear in the blif file, so you must pay attention to it. Note that output variable IDs in the resulting CNF file begin with number 2 (not 1).

Now you can solve the CNF formula using command "sat" applied directly to the CNF file:

However, the counter-example (the satisfying assignment) is not saved, because the problem came from CNF, not from the design. At this point you can use MiniSAT externally on your CNF.

Printing SAT Solutions (new)

In order to print the solution to SAT you should use the "dsat -w" command, so there is no need to use external tools such as MiniSAT. Here is how to do it:

Recall that "dsat; write_cex " shows a counter-example ONLY if it was called on a miter present in ABC as a current network in the AIG format (after "strash"). To obtain a SAT solution you should use "dsat -w file.cnf".

IMPORTANT: if CNF was generated by the "&write_cnf" command, the outputs will start in position 2, with count starting at 0. In the case below there are 2 outputs, at positions 2, 3; and the inputs will have the last values among those listed (in this case there are 6 inputs).

MiniSAT