Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: Madhu 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: References: <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 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) )