Addition chains: Difference between revisions

Line 1,786:

=={{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).

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 ~3 seconds).

<lang racket>#lang rosette

Line 1,803:

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

(define (try-len r n)

(define (try-len r n enumerate?)

(define xs (build-list (add1 r)

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

Line 1,812:

(cond

[(unsat? the-mod) sols]

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

[enumerate? (assert (next-sol xs the-mod))

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

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

[else (list (evaluate xs the-mod))])))

(clear-state!)

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

Line 1,825:

Line 1,826:

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

(define (compute n)

(define (compute n enumerate?)

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

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

⚫

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

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

(cond

⚫

(report-chain brauer-chain "brauer")

[enumerate?

⚫

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

⚫

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

(newline))

⚫

(report-chain brauer-chain "brauer")

⚫

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

[else (printf "example: ~a\n" (first (car sols)))]))

(define (compute/time n #:enumerate? enumerate?)

⚫

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

(match-define-values (_ _ real _) (time-apply compute (list n enumerate?)))

(printf "total time (ms): ~a\n\n" real))

⚫

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

(compute/time x #:enumerate? #t))

(for ([x (in-list '(191 382 379 12509))])

(compute/time x #:enumerate? #f))</lang>

Line 1,842:

Line 1,853:

#non-brauer chains: 2

example: (1 2 3 6 7 12 19)

total time (ms): 245

minimal chain length l(7) = 4

Line 1,847:

Line 1,859:

example: (1 2 3 6 7)

#non-brauer chains: 0

total time (ms): 47

minimal chain length l(14) = 5

Line 1,852:

Line 1,865:

example: (1 2 3 5 7 14)

#non-brauer chains: 0

total time (ms): 95

minimal chain length l(21) = 6

Line 1,858:

Line 1,872:

#non-brauer chains: 3

example: (1 2 4 5 8 13 21)

total time (ms): 204

minimal chain length l(29) = 7

Line 1,864:

Line 1,879:

#non-brauer chains: 18

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

total time (ms): 1443

minimal chain length l(32) = 5

Line 1,869:

Line 1,885:

example: (1 2 4 8 16 32)

#non-brauer chains: 0

total time (ms): 42

minimal chain length l(42) = 7

Line 1,875:

Line 1,892:

#non-brauer chains: 6

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

total time (ms): 808

minimal chain length l(64) = 6

Line 1,880:

Line 1,898:

example: (1 2 4 8 16 32 64)

#non-brauer chains: 0

total time (ms): 52

minimal chain length l(47) = 8

Line 1,886:

Line 1,905:

#non-brauer chains: 37

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

total time (ms): 6011

minimal chain length l(79) = 9

Line 1,892:

Line 1,912:

#non-brauer chains: 129

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

total time (ms): 38038

minimal chain length l(191) = 11

example: (1 2 4 8 16 24 28 29 53 69 138 191)

total time (ms): 1601

minimal chain length l(382) = 11

example: (1 2 4 5 9 14 23 46 92 184 368 382)

total time (ms): 2313

minimal chain length l(379) = 12

example: (1 2 4 8 12 24 48 72 73 121 129 258 379)

total time (ms): 3176

minimal chain length l(12509) = 17

example: (1 2 3 6 12 13 24 48 96 192 384 768 781 1562 3124 6248 12496 12509)

total time (ms): 237617

</pre>