;;;
;;; Randomized 3-SAT
;;;

(define $clause-satisfy?
  (lambda [$c $a]
    (any (lambda [$i $b] (if b a_i (not a_i))) c)))

(define $random-assign
  (lambda [$n]
    (generate-array [$i] n (R.car {#t #f}))))

(define $random-walk-3sat
  (match-lambda [something integer integer integer something]
    {[[$p  _ ,0 ,0  _] <Nothing>]
     [[$p $n ,0 $r  _] (R.sat-solver p n (- r 1))]
     [[$p $n $k $r $a]
      (match (randomize p) (multiset (R.multiset [integer bool]))
        {[<cons (& !?(clause-satisfy? $ a) <cons [$i _] _>) _>
          (random-walk-3sat p n (- k 1) r (A.update not i a))]
         [_ <Just a>]})]}))

(define $R.sat-solver
  (lambda [$p $n $r]
    (random-walk-3sat p n (* 3 n) r (random-assign n))))

(define $c1 {[1 #t] [2 #t] [3 #t]})
(define $c2 {[4 #t] [2 #t] [3 #f]})
(define $c3 {[1 #f] [4 #t] [3 #t]})
(define $c4 {[1 #f] [4 #f] [2 #t]})
(define $c5 {[4 #f] [2 #f] [3 #t]})
(define $c6 {[1 #f] [2 #f] [3 #f]})
(define $c7 {[1 #t] [4 #f] [3 #f]})
(define $c8 {[1 #t] [4 #t] [2 #f]})

(define $p1 {c1 c2 c3 c4 c5 c6 c7 c8})
(define $p2 {c1 c2 c3 c4 c5 c6 c8})

(R.sat-solver p1 4 3);=><Nothing>
(R.sat-solver p2 4 3);=><Just [|#f #f #t #t|]>, <Just [|#f #t #t #t|]>, or sometimes <Nothing>