37 lines
1.1 KiB
Common Lisp
37 lines
1.1 KiB
Common Lisp
|
(load "utils.lisp")
|
||
|
|
|
||
|
|
(defun first-n-bits (n int)
|
||
|
|
(loop for i below n
|
||
|
|
collecting (logbitp i int)))
|
||
|
|
|
||
|
|
(defun sat (expr)
|
||
|
|
(let* ((vars (delete-duplicates
|
||
|
|
(remove-if (lambda (x) (inq x and or not xor t nil))
|
||
|
|
(flatten expr))))
|
||
|
|
(varc (length vars))
|
||
|
|
(f (eval `(lambda ,vars
|
||
|
|
(declare (type boolean ,@vars) (optimize (speed 3) (safety 0) (debug 0)))
|
||
|
|
,expr))))
|
||
|
|
(disassemble f)
|
||
|
|
(loop for n below (expt 2 varc)
|
||
|
|
do (let1 bits (first-n-bits varc n)
|
||
|
|
(when (apply f bits)
|
||
|
|
(return-from sat
|
||
|
|
(mapcar #'list vars bits)))))
|
||
|
|
:unsat))
|
||
|
|
|
||
|
|
(defmacro time-s (expr)
|
||
|
|
(with-gensyms (start end diff)
|
||
|
|
`(begin
|
||
|
|
(= ,start (get-internal-real-time))
|
||
|
|
,expr
|
||
|
|
(= ,end (get-internal-real-time))
|
||
|
|
(= ,diff (- ,end ,start))
|
||
|
|
(/ ,diff internal-time-units-per-second))))
|
||
|
|
|
||
|
|
(defparameter timings
|
||
|
|
(loop for var-count below 30
|
||
|
|
collecting
|
||
|
|
(time-s (sat `(and ,@(loop for i below var-count
|
||
|
|
collecting (symb 'v i)))))))
|