• #### Re: (3-digit combination) was:

From Madhu@21:1/5 to All on Sun Mar 10 09:49:15 2024
* 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)
)

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)
• From Madhu@21:1/5 to All on Sun Mar 10 10:39:23 2024
* Lawrence D'Oliveiro <usjehr\$2pu3d\$1@dont-email.me> :
Wrote on Sun, 10 Mar 2024 04:56:28 -0000 (UTC):
On Sun, 10 Mar 2024 09:49:15 +0530, Madhu wrote:
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)?

You wanted to talk about “dicksizing” ... I would say your approach is overly long on code, and comes up short on correctness.

Well I can't see it. Maybe it is a shortcoming in the other approaches
that misses this solution.

does "0 4 2" violate any the rules posted in the original picture?

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)
• From Lawrence D'Oliveiro@21:1/5 to Madhu on Sun Mar 10 04:56:28 2024
On Sun, 10 Mar 2024 09:49:15 +0530, Madhu wrote:

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

You wanted to talk about “dicksizing” ... I would say your approach is overly long on code, and comes up short on correctness.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)
• From Paul Rubin@21:1/5 to Madhu on Sun Mar 10 03:01:21 2024
(of course i think there is no advantage in calling solver
over brute forcing it in lisp)

For 3 or 4 digits brute force is obviously fine. In that pdf that I
posted, the solver approach worked ok at 12 digits, which is a bit much
for brute force.

also this produces 2 results (0 6 2) and (0 4 2) -- the (0 4 2) result

042 was the "correct" solution to the original problem. I don't know
the situation with 062.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)
• From Madhu@21:1/5 to All on Mon Mar 11 07:39:35 2024
Wrote on Sun, 10 Mar 2024 10:39:23 +0530:

* Lawrence D'Oliveiro <usjehr\$2pu3d\$1@dont-email.me> :
Wrote on Sun, 10 Mar 2024 04:56:28 -0000 (UTC):
On Sun, 10 Mar 2024 09:49:15 +0530, Madhu wrote:
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)?

You wanted to talk about “dicksizing” ... I would say your approach is >> overly long on code, and comes up short on correctness.

Well I can't see it. Maybe it is a shortcoming in the other approaches
that misses this solution.

does "0 4 2" violate any the rules posted in the original picture?

As Paul Rubin pointed out in a parallel post (Thanks!), it is
not (0 4 2) but (0 6 2) which is wrong, and it violates the 3rd
constraint in the problem

--- (206): Two numbers are correct but wrongly placed

In the notation suggested in my first post i expressed this constraint
as

(defvar \$c3
(ONE-OF (ONE-OF '#?(.20) '#?(02.) '#?(0.2)) ;; 2 & 0 are correct
(ONE-OF '#?(62.) '#?(6.2) '#?(.62)) ;; 2 & 6 are correct
(ONE-OF '#?(06.) '#?(6.0) '#?(.60)) ;; 0 & 6 are correct
))

Which is incomplete because the rule indicates 2 numbers are incorrectly placed, the third is not placed at all.

. Instead it should look like

(ONE-OF (ONE-OF '#?([^6]20) '#?(02[^6]) '#?(0[^6]2)) ;; 2 & 0 are correct
(ONE-OF '#?(62[^0]) '#?(6[^0]2) '#?([^0]62)) ;; 2 & 6 are correct
(ONE-OF '#?(06[^2]) '#?(6[^2]0) '#?([^2]60)) ;; 0 & 6 are correct
))

the function GET-WRONGLY-PLACED (which is used in generating the
constraint) can be fixed to look like this:

```
(defun get-wrongly-placed (list indices &aux (always-excludes
(loop for i below (length list)
unless (find i indices)
collect (elt list i))))
;; 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))
,@(loop for j below (length list)
unless (find j idx)
collect `(not (or ,@(loop for x in always-excludes
collect (make-eql-clause x j)))))))))
```

Untested on problems with larger number of variables.

I think I realised this sending after my first post (and even fixed it
but the changes got lost and I forgot about it for my second post), but
yes the posted code was short on correcteness

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)