		Search-engine friendly clone of the ACL2 documentation.

Aig-sat

Determine whether an AIG is satisfiable.

Signature
(aig-sat aig &key (config 'satlink::*default-config*) (gatesimp '(aignet::default-gatesimp)) (transform-config 'nil)) → (mv status env)
Arguments: aig — The AIG to inspect.; config — How to invoke the SAT solver.
Guard (satlink::config-p config).; gatesimp — Guard (aignet::gatesimp-p gatesimp).
Returns: status — Either :sat, :unsat, or :failed.; env — When :sat, an (ordinary, slow) alist binding the aig vars to t/nil.

This is a convenient, high level way to ask a SAT solver whether a Hons AIG is satisfiable. When the AIG is satisfiable, you get back a satisfying assignment in terms of the Hons AIG's variables.

This function should only fail if there is some problem with the SAT solver, e.g., it produces output that satlink does not understand.

The underlying mechanism takes advantage of aignet to carry out the cnf conversion and satlink to call the SAT solver. As a picture:

         convert                export              dimacs
  AIG -------------> AIGNET -----------------> CNF -------> Solver
   ||                  ||                       ||            |
   ||                  ||                       ||            | interpret
satisfying          satisfying               satisfying       |  output
 alist or  <-------  array or   <-----------  assign or  <----'
 'unsat'    convert  'unsat'      translate   'unsat'

We simply trust the SAT solver if it says unsat, but the other translation and conversion steps are all verified.

Definitions and Theorems

Function: aig-sat-fn

(defun
 aig-sat-fn
 (aig config gatesimp transform-config)
 (declare (xargs :guard (and (satlink::config-p config)
                             (aignet::gatesimp-p gatesimp))))
 (let
  ((__function__ 'aig-sat))
  (declare (ignorable __function__))
  (b*
    (((local-stobjs satlink::env$ aignet::sat-lits aignet)
      (mv status env
          satlink::env$ aignet::sat-lits aignet))
     ((mv cnf ?lit vars aignet::sat-lits aignet)
      (aignet::aig->cnf aig aignet::sat-lits aignet
                        :transform-config transform-config
                        :gatesimp gatesimp))
     ((mv result satlink::env$)
      (satlink::sat cnf satlink::env$
                    :config config))
     ((unless (eq result :sat))
      (mv result nil
          satlink::env$ aignet::sat-lits aignet))
     (env (aignet::aig-cnf-vals->env satlink::env$
                                     vars aignet::sat-lits aignet)))
    (mv :sat env satlink::env$
        aignet::sat-lits aignet))))

Theorem: aig-sat-when-sat

(defthm aig-sat-when-sat
        (b* (((mv status env)
              (aig-sat aig
                       :config config
                       :transform-config transform-config
                       :gatesimp gatesimp)))
            (implies (equal status :sat)
                     (aig-eval aig env))))

Theorem: aig-sat-when-unsat

(defthm aig-sat-when-unsat
        (b* (((mv status &)
              (aig-sat aig
                       :config config
                       :transform-config transform-config
                       :gatesimp gatesimp)))
            (implies (aig-eval aig env)
                     (not (equal status :unsat)))))