• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
        • Unsat-checking
        • Check-config
          • Pigeon-hole
          • Simple-sat
          • Assert-unsat
          • Assert-sat
      • 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

• Sat-solver-options

Check-config

Run some quick checks of your SAT solver configuration.

Signature

(check-config config) → *

Arguments

config — Guard (config-p config).

This is a quick check to try to ensure that ACL2 can communicate with your SAT solver correctly. If it notices any problems, it will just cause a hard-error. A basic way to use it would be, e.g.,:

(include-book "centaur/satlink/check-config" :dir :system)
(defconst *my-config* (satlink::make-config ...))
(value-triple (satlink::check-config *my-config*))

It's a good idea to run this check when you install a new SAT solver, to ensure that your paths, command-line options, etc., are being handled correctly. It should catch basic problems such as:

• Your solver isn't in your PATH
• Your solver is crashing because it wants some other libc
• Your solver doesn't like some option you're passing to it
• Your solver doesn't understand what file to process
• Your solver isn't printing counterexamples
• Your solver isn't producing DIMACS formatted output

This is not any kind of comprehensive stress test of the SAT solver itself. We just run sat on a few small formulas to see if your solver is producing the expected results.

Definitions and Theorems

Function: check-config

(defun check-config (config)
 (declare (xargs :guard (config-p config)))
 (let ((__function__ 'check-config))
  (declare (ignorable __function__))
  (b* ((la (make-lit 0 0))
       (~la (make-lit 0 1))
       (lb (make-lit 1 0))
       (~lb (make-lit 1 1))
       (lc (make-lit 2 0))
       (~lc (make-lit 2 1))
       (ld (make-lit 100 0))
       (~ld (make-lit 100 1)))
   (progn$
    (cw "*** Checking that the empty list of clauses is SAT. ***~%")
    (assert-sat nil)
    (cw "*** Checking that an empty clause is UNSAT. ***~%")
    (assert-unsat (list nil))
    (cw "*** Checking that some singleton clauses are SAT. ***~%")
    (assert-sat (list (list la)))
    (assert-sat (list (list lb)))
    (assert-sat (list (list lc)))
    (assert-sat (list (list ld)))
    (assert-sat (list (list ~la)))
    (assert-sat (list (list ~lb)))
    (assert-sat (list (list ~lc)))
    (assert-sat (list (list ~ld)))
    (cw "*** Checking that clauses (A) and (!A) are UNSAT. ***~%")
    (assert-unsat (list (list la) (list ~la)))
    (assert-unsat (list (list lb) (list ~lb)))
    (assert-unsat (list (list lc) (list ~lc)))
    (assert-unsat (list (list ld) (list ~ld)))
    (assert-unsat (list (list ~la) (list la)))
    (assert-unsat (list (list ~lb) (list lb)))
    (assert-unsat (list (list ~lc) (list lc)))
    (assert-unsat (list (list ~ld) (list ld)))
    (cw "*** A few more tests ***~%")
    (assert-sat (list (list la ~la)
                      (list lb)
                      (list lc ~lc)
                      (list ld ~ld)))
    (assert-unsat (list (list la ~la)
                        (list lb)
                        (list lc ~la)
                        (list ld ~ld)
                        (list ~lb)))
    (assert-sat (list (list la)
                      (list ~la lb)
                      (list ~lb lc)
                      (list ~lc ld)))
    (assert-unsat (list (list la)
                        (list ~la lb)
                        (list ~lb lc)
                        (list ~lc ld)
                        (list ~ld)))
    (cw "*** Some basic pigeon-hole problems ***~%")
    (assert-unsat (pigeon-hole 3 1))
    (assert-unsat (pigeon-hole 3 2))
    (assert-sat (pigeon-hole 3 3))
    (assert-sat (pigeon-hole 3 4))
    (assert-unsat (pigeon-hole 4 1))
    (assert-unsat (pigeon-hole 4 2))
    (assert-unsat (pigeon-hole 4 3))
    (assert-sat (pigeon-hole 4 4))
    (assert-sat (pigeon-hole 4 5))
    (assert-unsat (pigeon-hole 7 6))
    (assert-sat (pigeon-hole 7 7))
    (cw
     "*** Good deal -- this SATLINK configuration seems OK. ***~%")))))

Subtopics

Pigeon-hole

Simple-sat

Assert-unsat

Assert-sat