Re: (3-digit combination) was:

* Paul Rubin <87msrgeann.fsf @nightsong.com> :
Wrote on Sat, 02 Mar 2024 10:44:28 -0800:

HenHanna <HenHanna@dev.null> writes:

  What are some relevant sections in Knuth's book [Satisfiability] ?

>
That book discusses the algorithms used in SAT solvers, but from what
little I know, they are all tweaks and improvements on the DPLL
algorithm from the 1960s:
>
https://en.wikipedia.org/wiki/DPLL_algorithm

When I last dealt with 3-SAT there was an accessible common lisp
implementation, which I think was backed by this
https://www.math.ucdavis.edu/~deloera/TEACHING/MATH165/davisputnam.pdf

Thus, if you want to study the workings of SAT solvers, you could start
by looking at MiniSAT which is one of the simplest.  If you want to
learn how to use them, this is good:
>
https://yurichev.com/writings/SAT_SMT_by_example.pdf

I found out I have microsoft's' z3 solvers installed as part of llvm.
It became trivial to extend the lisp solution I posted on cll last month
to Hanna's problem to output SMT (which is basically lisp), but it is
also retarded on many levels, because of the complexities involved.
I understand the dicksizing challenge posted here is to minimize the
program size and expressibility but i think expressibility also comes
from symbolic processing capabilities of lisp that allow me to represent
the problem in a way that comes up with a direct solution, (though this
is retarded in other ways. but for the sake of illustration.
The code below can be trivially used to prdoduce a program in the SMTLIB
language (see DUMP-SMT) and checked against z3. this is my attempt after
reading the smt code in yurichev pdf for a few minutes, all corrections
welcome.  (of course i think there is no advantage in calling solver
over brute forcing it in lisp)
also this produces 2 results (0 6 2) and (0 4 2) -- the (0 4 2) result
wasn't reported in the solutions in the other languages, is it wrong?
(and therefore my whole approach)?
#+begin_src lisp
(defun make-eql-clause (num i &key (var-stem "N") (package *package*) (test '=))
  "I is 0 based"
  (assert (<= 0 num 9))
  (check-type test symbol)
  (let* ((n (1+ i))
(name (format nil "~A~D" var-stem n))
(sym (intern  name package)))
    `(,test ,sym ,num)))
(defun make-eql-clause (num i &key (var-stem "N") (package *package*) (test '=))
  "I is 0 based"
  (assert (<= 0 num 9))
  (check-type test symbol)
  (let* ((n (1+ i))
(name (format nil "~A~D" var-stem n))
(sym (intern  name package)))
    `(,test ,sym ,num)))
(defun get-well-placed-list (list idx)
  "LIST is a list of numbers, IDX is a list of indices. The numbers
at the indices are well placed. Return an expression which expresses
the constraint."
  `(and ,@(loop for i in idx
collect (make-eql-clause (elt list i) i))))
(defun generate-none (list)
  `(and ,@(loop for i below (length list) collect
`(not (or ,@(loop for j  below (length list)
  collect  (make-eql-clause (elt list j) i)))))))
#+nil
(require 'alexandria)
(defun get-combination-indices-list (n m)
  "Return a list of indices of n items taken m at a time"
  (let (indices)
    (alexandria:map-combinations (lambda (x) (push x indices))
(loop for i below n collect i)
:length m)
    indices))
(defun generate-well-placed (list n)
  (let* ((len (length list))
(indices (get-combination-indices-list len n)))
    (assert (<= n len))
    (if (zerop n)
(generate-none list)
`(or ,@(loop for x in indices
     collect (get-well-placed-list list x))))))
(defun get-permutations (list &optional n)
  (let (ret)
    (alexandria:map-permutations (lambda (elt) (push elt ret)) list :length n)
    ret))
(defun get-wrongly-placed (list indices)
  ;; elements of list at positions in indices are incorrectly placed
  `(or ,@(loop for idx in (get-permutations (loop for i below (length list) collect i)
    (length indices))
       unless (loop for i in idx for j in indices
    thereis (= i j))
       collect `(and ,@(loop for i in idx for j in indices
     collect (make-eql-clause (elt list j) i))))))
(defun generate-wrongly-placed (list n)
  (if (= n (length list))
      (generate-none list)
      `(or ,@(loop for i in (get-combination-indices-list (length list) n)
   collect (get-wrongly-placed list i)))))
(defun check(&optional (checker 'checker))
  (let (results)
    (loop for n1 from 0 below 10
  do (loop for n2 from 0 below 10
   do (loop for n3 from 0 below 10
    if (funcall checker n1 n2 n3)
    do (push (list n1 n2 n3) results))))
    results))
(defmacro defchecker2 (&optional (name 'checker2))
  `(defun ,name (n1 n2 n3)
     ,(list 'and
    (setq $d1 (generate-well-placed '(6 8 2) 1))
    (setq $d2 (generate-wrongly-placed '(6 1 4) 1))
    (setq $d3 (generate-wrongly-placed '(2 0 6) 2))
    (setq $d4 (generate-none '(7 3 8)))
    (setq $d5 (generate-wrongly-placed '(7 8 0) 1)))))
(defchecker2)
(time (check #'checker2))
;; => ((0 6 2) (0 4 2))
(defun dump-smt (out)
  (with-open-file (stream out :direction :output :if-exists :supersede)
    (write-string "
(declare-const n1 Int)
(declare-const n2 Int)
(declare-const n3 Int)
(declare-const x Int)
(assert (<= 0 n1 9))
(assert (<= 0 n2 9))
(assert (<= 0 n3 9))
"  stream)
  (loop for i in (list $d1 $d2 $d3 $d4 $d5) do
   (write `(assert ,i) :stream stream :pretty t :case :downcase)
    (terpri stream))
  (write-string "
(check-sat)
(get-model)
" stream)))
(dump-smt "/tmp/h2.smt")
#+end_src
$ z3 -smt2 /tmp/h2.smt
sat
(model
  (define-fun n1 () Int
    0)
  (define-fun n2 () Int
    4)
  (define-fun n3 () Int
    2)
)