Personally i wouldn’t use continuations for this—or for search algorithms in general. A for*/fold would be best for a fixed number of variables. Otherwise a named let loop, and a for over variables would be my choice. It could be purely functional with an accumulator, but if i needed to track many things then using set! could be simpler.

Also check: https://docs.racket-lang.org/reference/pairs.html?q=Combinations#%28def._%28%28lib._racket%2Flist..rkt%29._in-combinations%29%29\|https://docs.racket-lang.org/reference/pairs.html?q=Combinations#%28def._%28%28lib._racket%2Flist..rkt%29._in-combinations%29%29

@laurent.orseau Do you mean list-comprehension? Like this: (for*/list ([b1 '(#t #f)] [b2 '(#t #f)] [b3 '(#t #f)] #:when (or (and (not b1) b2) (and b1 (not b3)))) (list b1 b2 b3)) ;; => '((#t #t #f) (#t #f #f) (#f #t #t) (#f #t #f)) Indeed there are many ways to achieve this kind of nondeterministic computation. But my question is mainly about using delimited continuation. When we use delimited continuation (e.g. reset/shift), it seems always to cooperate well with mutation.

Someone please correct me if I’m wrong, but I’m not sure I would call continuations purely functional. So if your goal is to be more functional, list comprehension or name let loops would be the way to go. If your goal is to have the most ‘elegant’ solution (for some subjective definition of elegant) with the constraint of using continuations, then I’m probably not the right person to answer—I find the control flow of continuations somewhat difficult to keep track of in the general case. If your goal is to tackle SAT problems, then clearly continuations is the wrong tool, unless you care only about small/toy problems.

Comparing with for*/list solution, the rest/shift version is something like: (define (flip lst) (shift c (map (λ (x) (c x)) lst))) (let ((acc-lst '())) (reset (let ((b1 (flip '(#t #f))) (b2 (flip '(#t #f))) (b3 (flip '(#t #f)))) (when (or (and (not b1) b2) (and b1 (not b3))) (set! acc-lst (cons `(,b1 ,b2 ,b3) acc-lst))) )) (reverse acc-lst)) ;; => '((#t #t #f) (#t #f #f) (#f #t #t) (#f #t #f)) They are not very different in syntax, but the rest/shift version use mutation. (I’m sorry, this may not be a formal question. I’m just curious about this phenomenon and hope some comments:sweat_smile:. )

I consider continuation to still be in the realm of functional programming. However, it is a powerful construct, and as a result, it makes program reasoning difficult, which kinda kills “functional programming is easy to reason”.

It’s absolutely fine :slightly_smiling_face: Although I wouldn’t really tag this question ‘beginners’ :wink: It’s just that I’m unclear what kind of feedback you’re looking for. You say: > These two solutions return the same result, but which one is better? but there are lots of possible definitions of ‘better’, as I hinted at in my previous reply: speed efficiency, memory efficiency, readability, maintainability, compatibility, safety, and all possible dogmatic philosophies about programming styles.

That’s why I’m asking about your goal instead: Do you want to solve SAT problems, do you want to learn to use continuations, do you want to understand a particular point about continuations and mutation, do you want to share your code with other people, …?

@chansey97 If you are annoyed by the set! you could always hide in a macro :wink: The amb construct from SICP is an example of such “hiding”.

> 1. tag this question ‘beginners’ > 2. These two solutions return the same result, but which one is better? Yes, this is my fault. PS: I am a beginner to reset/shift, recently I was trying to use reset/shift and observed some phenomenon. The real question may be “understanding a particular point about continuations and mutation”.

If you refactor your Solution–2 with intermediate (reusable) constructs with good names then you may find your main test-sat as readable as Solution–1 I guess. Continuation-based accumulator?

Hiding in a macro is a great idea. This allow us to create own for*/list by using rest/shift construct and mutation. In the past, this kind of list comprehension need list monad (or applicative), but rest/shift gives us a new point.

> refactor your Solution–2 with intermediate (reusable) constructs with good names I’m not very understand. Could you explain further? Thanks.

I mean that you can also hide your structs and their usage with macros, and maybe split/extract some code from flip to make it more readable and look more ‘generic’ (that is, you’re building reusable tools, and thus these tools)

Solution–3 (functional and intuitive way, no need mutation!): (define (flip) (shift c (begin (c #t) (c #f) (void) ))) (define (test-sat) (let ((g (generator () (reset (let ((b1 (flip)) (b2 (flip)) (b3 (flip))) (let ((r (or (and (not b1) b2) (and b1 (not b3))))) (if r (yield `(,b1 ,b2 ,b3)) #f)) ))))) (for/list ([i (in-producer g (void))]) i))) (test-sat) ;; => '((#t #t #f) (#t #f #f) (#f #t #t) (#f #t #f)) We can compose generator and reset/shift.

Very nice!

If we introduce generator then the reset/shift is not necessary (In fact, the reset/shift is meaningless from the beginning). (define (test-sat_2) (let ((g (generator () (for ([b1 '(#t #f)]) (for ([b2 '(#t #f)]) (for ([b3 '(#t #f)]) (when (or (and (not b1) b2) (and b1 (not b3))) (yield `(,b1 ,b2 ,b3))))))))) (for/list ([i (in-producer g (void))]) i))) (test-sat_2) ;; => '((#t #t #f) (#t #f #f) (#f #t #t) (#f #t #f)) omg…what am I doing?

Instead of generator+reset/shift, can you do it with lambda+reset/shift?

What do you mean by “do it with lambda+reset/shift”?

The 3SAT problem may be too simple to show the expressiveness of reset/shift .

I suspect generator could be defined in terms of lambda and reset/shift .

I agree. Another way is using call/cc.

Also this 3SAT problem can be solved easily by imperative language: public static List<Tuple<bool, bool, bool>> SAT() { var resList = new List<Tuple<bool, bool, bool>>(); foreach (var b1 in new List<bool> { true, false }) { foreach (var b2 in new List<bool> { true, false }) { foreach (var b3 in new List<bool> { true, false }) { if ((!b1 && b2) \|\| (b1 && !b3)) { resList.Add(new Tuple<bool, bool, bool>(b1, b2, b3)); } } } } return resList; }

Question: are any of these (automatically or easy to make) parallel? For something boolean satisfiability, that might be something to consider (rather than just “try all combinations one at a time”)

SAT solving is known to be very hard to parallelize. IIUC, the most commonly used strategy is to solve the same problem in parallel, but with different configuration (like random seed, etc), and answer the one that finishes first.

interesting, thanks, didn’t know that. Should’ve figured you would know; I’m citing your Rosette-related paper in a report for my MS :slightly_smiling_face:

Glad to hear! :slightly_smiling_face:

Is it possible to make a predicate associative? that takes a binary operator, e.g. returns #t on + and #f on -? I suspect that’s not the case in general since: 1. associativity is defined for an operation on a set, so it requires that we specify the set 2. associativity testing would require 3 arguments So essentially, I’d have to make a catalogue if I want to test that, e.g. an assoc such as '((+ natural?) (* natural?) ...) ?

@raoul.schorer Associativity of operators has to be mathematically proven. This can be done with a program, but it requires a theorem-proving language. Although automated proof generation has come a long way, I suspect it’s not (currently) possible to simply ask if an operator is associative and get a yes-or-no answer.

You could try QuickCheck-style property testing, but that 1. Doesn’t give a definitive answer. 2. Is computationally-intensive and not suited for use in the middle of a program.

(Also note that, since Racket’s arithmetic operators also work on floating-point numbers, they don’t have the nice algebraic properties we’d expect, in the general case.)

@kellysmith12.21 Yes, referring to the docs I guess contract random generation yields QuickCheck testing. Catalogue it is, then. Thanks.