• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Satlink

Sat

Top-level function for running a SAT solver.

Signature

(sat formula env$ &key (config '*default-config*)) 
  → 
(mv status env$)

Arguments

formula — A cnf formula to solve.
    Guard (lit-list-listp formula).

env$ — Environment to populate with a satisfying assignment, in the case of SAT. Will be emptied, in any case.

config — Configuration for running a SAT solver.
    Guard (config-p config).

Returns

status — :sat, :unsat, or :failed.

env$ — Satisfying assignment, in the case of :sat.

This is the top-level wrapper for calling SAT. It handles the details of clearing out the env$ and checking the SAT solver's answers when there is a counterexample or an LRAT proof available.

Definitions and Theorems

Function: sat-fn

(defun sat-fn (formula env$ config)
 (declare (xargs :stobjs (env$)))
 (declare (xargs :guard (and (lit-list-listp formula)
                             (config-p config))))
 (let ((__function__ 'sat))
  (declare (ignorable __function__))
  (b*
   ((env$ (mbe :logic (non-exec nil)
               :exec (resize-bits 0 env$)))
    ((when (trivial-unsat-p formula))
     (mv :unsat env$))
    ((config config) config)
    ((mv status env$ lrat-proof)
     (time$ (satlink-run config formula env$)
            :msg "; SATLINK: round trip: ~st sec, ~sa bytes.~%"
            :mintime config.mintime))
    ((when (and (eq status :unsat)
                config.lrat-check))
     (b*
      ((lrat-formula (formula-to-lrat-formula formula 1))
       (ok
          (time$ (lrat::lrat-refutation-p$ lrat-proof lrat-formula)
                 :msg "; SATLINK: lrat check: ~st sec, ~sa bytes.~%"
                 :mintime config.mintime))
       ((unless ok)
        (cw
         "SAT: Supposedly unsatisfiable, but check of LRAT proof failed!~%")
        (mv :failed env$)))
      (mv :unsat env$)))
    ((unless (eq status :sat))
     (mv status env$))
    ((when
      (time$
        (int= 0 (eval-formula formula env$))
        :msg "; SATLINK: verifying assignment: ~st sec, ~sa bytes~%"
        :mintime config.mintime))
     (cw "SAT: Supposedly satisfiable, but assignment is wrong~%")
     (mv :failed env$)))
   (mv :sat env$))))

Theorem: sat-normalize-env

(defthm sat-normalize-env
  (implies (syntaxp (not (equal env$ ''nil)))
           (equal (sat formula env$ :config config)
                  (sat formula nil :config config))))

Theorem: sat-when-sat

(defthm sat-when-sat
  (b* (((mv status new-env$)
        (sat formula env$ :config config)))
    (implies (equal status :sat)
             (equal (eval-formula formula new-env$)
                    1))))

Theorem: sat-when-unsat

(defthm sat-when-unsat
  (b* (((mv status &)
        (sat formula env$ :config config)))
    (implies (equal (eval-formula formula env) 1)
             (not (equal status :unsat)))))