Reasoning with SAT solvers - NTU-ALComLab/LSV-PA GitHub Wiki

Key questions and commonly-used APIs

  1. How to obtain an AIG circuit (Aig_Man_t) from a network (Abc_Ntk_t)?
  • Method Abc_NtkToDar() derives an equivalent Aig_Man_t (global AIG circuit) from an Abc_Ntk_t network.
  • It does not change the original Abc_Ntk_t. On the other hand, method Abc_NtkToAig() changes the representation of a node in Abc_Ntk_t to AIGs.
  1. How to derive a CNF formula (Cnf_Dat_t) which describes an AIG circuit?
  • Method Cnf_Derive() encodes the behavior of an Aig_Man_t as a CNF formula Cnf_Dat_t.
  • It has some optimizations to derive compact formulas. It does not literally convert each AIG node to clauses.
  1. How to manipulate a CNF formula (e.g., create a fresh copy of a CNF formula)?
  • Clauses are stored in pClauses as a two-dimensional integer array.
  • Method Cnf_DataDup() duplicates a CNF formula.
  • Method Cnf_DataLift() increments variables in a formula by the specified number.
  • To create a fresh copy, first duplicate the original CNF formula and lift its variables.
  1. How to initialize an SAT solver (sat_solver)?
  • Method Cnf_DataWriteIntoSolver() takes a CNF formula Cnf_Dat_t and returns an SAT solver sat_solver with the formula.
  • Method sat_solver_new() creates an empty SAT solver.
  1. How to manipulate an SAT solver (e.g., create variables, add clauses, solve with assumptions, etc)?
  • In an SAT solver, variables and literals are just integers int (type lit is defined to be int). A positive literal of a variable is the double of it. A negative literal is a positive literal plus one. Method toLitCond() converts a variable to a literal.
  • A clause or an assumption is an array of literals.
  • Method sat_solver_addvar() creates a new variable in the solver.
  • Method sat_solver_setnvars() creates a specified number of variables.
  • Method sat_solver_addclause() adds a clause into the solver. A clause, i.e., an integer array (lit*), is specified by the beginning and end of the array.
  • Method sat_solver_add_buffer_enable() adds clauses to assert the equivalence (namely, a buffer) between two variables controlled by an enabling variable.
  • Method sat_solver_solve() solves the formula. An assumption is given in a similar way as a clause.
  • Method sat_solver_final() returns a final conflict clause.
  1. How to obtain the variable allocated for a specific gate in the AIG circuit (Aig_Man_t)?
  • Field pVarNums of Cnf_Dat_t stores a mapping from the ID of an Aig_Obj_t to its variable in Cnf_Dat_t.

To answer the above questions, command dsat is a good starting point.