Addition chains: Difference between revisions

=={{header|Racket}}==

This implementation uses the [https://docs.racket-lang.org/rosette-guide/index.html Rosette] language in Racket. It is inefficient as it asks an SMT solver to enumerate every possible solutions. However, it is very straightforward to write, and in fact is quite efficient for computing <code>l(n)</code> and finding one example (solve n = 379 in 2 seconds).

<lang racket>#lang rosette

(define (basic-constraints xs n)

(assert (= 1 (first xs)))

(assert (= n (last xs)))

(assert (apply < xs))

(for ([x (in-list (rest xs))] [xi (in-naturals 1)])

(assert

(apply || (for*/list ([(y yi) (in-parallel (in-list xs) (in-range xi))]

[(z zi) (in-parallel (in-list xs) (in-range xi))])

(= x (+ y z)))))))

(define (next-sol xs the-mod)

(not (apply && (for/list ([x (in-list xs)]) (= x (evaluate x the-mod))))))

(define (try-len r n)

(define xs (build-list (add1 r)

(thunk* (define-symbolic* x integer?)

x)))

(basic-constraints xs n)

(define sols (let loop ([sols '()])

(define the-mod (solve #t))

(cond

[(unsat? the-mod) sols]

[else (assert (next-sol xs the-mod))

(loop (cons (evaluate xs the-mod) sols))])))

(clear-state!)

(if (empty? sols) #f (cons sols r)))

(define (brauer? xs)

(for/and ([x (in-list (rest xs))] [xi (in-naturals 1)] [x* (in-list xs)])

(for/or ([y (in-list xs)] [yi (in-range xi)]) (= x (+ x* y)))))

(define (report-chain chain name)

(printf "#~a chains: ~a\n" name (length chain))

(when (not (empty? chain)) (printf "example: ~a\n" (first chain))))

(define (compute n)

(define sols (for/or ([r (in-naturals 1)]) (try-len r n)))

(define-values (brauer-chain non-brauer-chain) (partition brauer? (car sols)))

(printf "minimal chain length l(~a) = ~a\n" n (cdr sols))

(report-chain brauer-chain "brauer")

(report-chain non-brauer-chain "non-brauer")

(newline))

(for ([x (in-list '(19 7 14 21 29 32 42 64 47 79))]) (compute x))</lang>

{{out}}

<pre>

minimal chain length l(19) = 6

#brauer chains: 31

example: (1 2 3 4 8 16 19)

#non-brauer chains: 2

example: (1 2 3 6 7 12 19)

minimal chain length l(7) = 4

#brauer chains: 5

example: (1 2 3 6 7)

#non-brauer chains: 0

minimal chain length l(14) = 5

#brauer chains: 14

example: (1 2 3 5 7 14)

#non-brauer chains: 0

minimal chain length l(21) = 6

#brauer chains: 26

example: (1 2 3 4 7 14 21)

#non-brauer chains: 3

example: (1 2 4 5 8 13 21)

minimal chain length l(29) = 7

#brauer chains: 114

example: (1 2 3 6 7 13 16 29)

#non-brauer chains: 18

example: (1 2 3 6 9 11 18 29)

minimal chain length l(32) = 5

#brauer chains: 1

example: (1 2 4 8 16 32)

#non-brauer chains: 0

minimal chain length l(42) = 7

#brauer chains: 78

example: (1 2 3 6 9 15 21 42)

#non-brauer chains: 6

example: (1 2 4 5 8 13 21 42)

minimal chain length l(64) = 6

#brauer chains: 1

example: (1 2 4 8 16 32 64)

#non-brauer chains: 0

minimal chain length l(47) = 8

#brauer chains: 183

example: (1 2 3 5 8 11 22 44 47)

#non-brauer chains: 37

example: (1 2 3 5 7 14 19 28 47)

minimal chain length l(79) = 9

#brauer chains: 492

example: (1 2 4 8 12 13 25 29 54 79)

#non-brauer chains: 129

example: (1 2 4 8 9 12 21 29 58 79)

</pre>