egison-3.5.2: sample/3sat.egi

;;;
;;; 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]
    {[[$f _ ,0 ,0 _] <Nothing>]
     [[$f $n ,0 $r _] (random-walk-3sat f n (* n 3) (- r 1) (random-assign n))]
     [[$f $n $k $r $a]
      (match (randomize f) (multiset (R.multiset [integer bool]))
        {[<cons (& ^?(clause-satisfy? $ a) <cons [$x _] _>) _>
          (random-walk-3sat f n (- k 1) r (generate-array [$i] n (if (eq? i x) (not a_i) a_i)))]
         [_ <Just a>]})]}))

(define $R.sat-solver
  (lambda [$f $n $r]
    (random-walk-3sat f 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)
(R.sat-solver p2 4 3)