aig-sat

(in-package "ACL2")

(define aig-sat
  :parents (aig)
  :short "Determine whether an AIG is satisfiable."
  ((aig "The AIG to inspect.") &key
    ((config config-p "How to invoke the SAT solver.") '*default-config*)
    ((gatesimp gatesimp-p) '(default-gatesimp))
    ((transform-config) 'nil))
  :returns (mv (status "Either :sat, :unsat, or :failed")
    (env "When :sat, an (ordinary, slow) alist binding the
                        aig vars to t/nil."))
  :long "<p>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.</p>

<p>This function should only fail if there is some problem with the SAT solver,
e.g., it produces output that @(see satlink) does not understand.</p>

<p>The underlying mechanism takes advantage of @(see aignet) to carry out the
<see topic='@(url aignet::aignet-cnf)'>cnf conversion</see> and @(see satlink)
to call the SAT solver.  As a picture:</p>

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

<p>We simply trust the SAT solver if it says @('unsat'), but the other
translation and conversion steps are all verified.</p>"
  (b* (((local-stobjs env$ sat-lits aignet) (mv status
         env
         env$
         sat-lits
         aignet)) ((mv cnf ?lit vars sat-lits aignet) (aig->cnf aig
          sat-lits
          aignet
          :transform-config transform-config
          :gatesimp gatesimp))
      ((mv result env$) (sat cnf env$ :config config))
      ((unless (eq result :sat)) (mv result nil env$ sat-lits aignet))
      (env (aig-cnf-vals->env env$
          vars
          sat-lits
          aignet)))
    (mv :sat env env$ sat-lits aignet))
  ///
  (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)))
    :hints (("Goal" :in-theory (disable vars-of-aig->cnf))))
  (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))))
    :hints (("goal" :use ((:instance aig-satisfying-assign-induces-aig->cnf-satisfying-assign
          (aig aig)
          (env env)
          (gatesimp gatesimp)
          (transform-config transform-config)
          (sat-lits (create-sat-lits))
          (aignet (create-aignet))))
       :in-theory (disable aig-satisfying-assign-induces-aig->cnf-satisfying-assign)))))