Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Madhu <enometh@meer.net>
Newsgroups: comp.lang.lisp
Subject: Re: (3-digit combination) was:
Date: Sun, 10 Mar 2024 09:49:15 +0530
Organization: Motzarella
Lines: 171
Message-ID: <m3v85ubtx8.fsf_-_@leonis4.robolove.meer.net>
References: <urhtof$2grs4$1@dont-email.me> <87h6hqei3p.fsf@nightsong.com>
	<58a6bc89dcf829f6041d052ec4bd8bb4@www.novabbs.com>
	<87msrgeann.fsf@nightsong.com>
MIME-Version: 1.0
Content-Type: text/plain
Injection-Info: dont-email.me; posting-host="a3c737dd1e6adb23b0842ad931a468a6";
	logging-data="2935558"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19Gqv0+aGqcA+AS6u0rz1BaEK+5xF/+Q/4="
Cancel-Lock: sha1:c7BFLH8258OGEcHLAL4y9Furutc=
	sha1:k9iK9mniZI3ka8/Pfz8Xw+RLav8=
Bytes: 6667

* 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)
)