(define $delete-literal
  (lambda [$l $cnf]
    (map (lambda [$c] (match-all c (multiset integer)
                        [<cons (and !,l $x) _> x]))
         cnf)))

(define $delete-clauses-with
  (lambda [$l $cnf]
    (match-all cnf (multiset (multiset integer))
      [<cons (& !<cons ,l _> $c) _> c])))

(define $assign-true
  (lambda [$l $cnf]
    (delete-literal (neg l) (delete-clauses-with l cnf))))

(define $assignment
  (algebraic-data-matcher
    {<deduced integer> <guessed integer something something>}))

(define $dpll'
  (lambda [$vars $cnf $trail]
    (match [vars cnf] [(multiset integer) (multiset (multiset integer))]
      {[[_ <nil>] #t]
       [[_ <cons <nil> _>]
        (match (debug trail) (list assignment)
          {[<join _ <cons <guessed $l $vars' $cnf'> $trail'>>
            (dpll' vars' (assign-true (neg l) cnf') {<Deduced (neg l)> @trail'})]
           [_ #f]})]
       [[_ <cons <cons $l <nil>> _>] (dpll' (delete (abs l) vars) (assign-true l cnf) {<Deduced l> @trail})]
       [[<cons $v $vs> !<cons <cons ,(neg v) _> _>] (dpll' vs (assign-true v cnf) {<Deduced v> @trail})]
       [[<cons $v $vs> !<cons <cons ,v _> _>] (dpll' vs (assign-true (neg v) cnf) {<Deduced (neg v)> @trail})]
       [[<cons $v $vs> _] (dpll' vs (assign-true v cnf) {<Guessed v vs cnf> @trail})]
       })))

(define $dpll
  (lambda [$vars $cnf]
    (dpll' vars cnf {})))

;"dpll start"
(dpll {1} {{1}}) ; #t
(dpll {1} {{1} {-1}}) ; #f
;(dpll {1 2 3} {{1 2} {-1 3} {1 -3}}) ; #t
;(dpll {1 2} {{1 2} {-1 -2} {1 -2}}) ; #t
;(dpll {1 2} {{1 2} {-1 -2} {1 -2} {-1 2}}) ; #f
;(dpll {1 2 3 4 5} {{-1 -2 3} {-1 -2 -3} {1 2 3 4} {-4 -2 3} {5 1 2 -3} {-3 1 -5} {1 -2 3 4} {1 -2 -3 5}}) ; #f
;(dpll {1 2} {{-1 -2} {1}}) ; #t
;"dpll end"

(define $problem20
  {{ 4 -18 19}
   {3 18 -5}
   {-5 -8 -15}
   {-20 7 -16}
   {10 -13 -7}
   {-12 -9 17}
   {17 19 5}
   {-16 9 15}
   {11 -5 -14}
   {18 -10 13}
   {-3 11 12}
   {-6 -17 -8}
   {-18 14 1}
   {-19 -15 10}
   {12 18 -19}
   {-8 4 7}
   {-8 -9 4}
   {7 17 -15}
   {12 -7 -14}
   {-10 -11 8}
   {2 -15 -11}
   {9 6 1}
   {-11 20 -17}
   {9 -15 13}
   {12 -7 -17}
   {-18 -2 20}
   {20 12 4}
   {19 11 14}
   {-16 18 -4}
   {-1 -17 -19}
   {-13 15 10}
   {-12 -14 -13}
   {12 -14 -7}
   {-7 16 10}
   {6 10 7}
   {20 14 -16}
   {-19 17 11}
   {-7 1 -20}
   {-5 12 15}
   {-4 -9 -13}
   {12 -11 -7}
   {-5 19 -8}
   {1 16 17}
   {20 -14 -15}
   {13 -4 10}
   {14 7 10}
   {-5 9 20}
   {10 1 -19}
   {-16 -15 -1}
   {16 3 -11}
   {-15 -10 4}
   {4 -15 -3}
   {-10 -16 11}
   {-8 12 -5}
   {14 -6 12}
   {1 6 11}
   {-13 -5 -1}
   {-7 -2 12}
   {1 -20 19}
   {-2 -13 -8}
   {15 18 4}
   {-11 14 9}
   {-6 -15 -2}
   {5 -12 -15}
   {-6 17 5}
   {-13 5 -19}
   {20 -1 14}
   {9 -17 15}
   {-5 19 -18}
   {-12 8 -10}
   {-18 14 -4}
   {15 -9 13}
   {9 -5 -1}
   {10 -19 -14}
   {20 9 4}
   {-9 -2 19}
   {-5 13 -17}
   {2 -10 -18}
   {-18 3 11}
   {7 -9 17}
   {-15 -6 -3}
   {-2 3 -13}
   {12 3 -2}
   {-2 -3 17}
   {20 -15 -16}
   {-5 -17 -19}
   {-20 -18 11}
   {-9 1 -5}
   {-19 9 17}
   {12 -2 17}
   {4 -16 -5}})

(define $problem50
  {{ 18 -8 29}
   {-16 3 18}
   {-36 -11 -30}
   {-50 20 32}
   {-6 9 35}
   {42 -38 29}
   {43 -15 10}
   {-48 -47 1}
   {-45 -16 33}
   {38 42 22}
   {-49 41 -34}
   {12 17 35}
   {22 -49 7}
   {-10 -11 -39}
   {-28 -36 -37}
   {-13 -46 -41}
   {21 -4 9}
   {12 48 10}
   {24 23 15}
   {-8 -41 -43}
   {-44 -2 -35}
   {-27 18 31}
   {47 35 6}
   {-11 -27 41}
   {-33 -47 -45}
   {-16 36 -37}
   {27 -46 2}
   {15 -28 10}
   {-38 46 -39}
   {-33 -4 24}
   {-12 -45 50}
   {-32 -21 -15}
   {8 42 24}
   {30 -49 4}
   {45 -9 28}
   {-33 -47 -1}
   {1 27 -16}
   {-11 -17 -35}
   {-42 -15 45}
   {-19 -27 30}
   {3 28 12}
   {48 -11 -33}
   {-6 37 -9}
   {-37 13 -7}
   {-2 26 16}
   {46 -24 -38}
   {-13 -24 -8}
   {-36 -42 -21}
   {-37 -19 3}
   {-31 -50 35}
   {-7 -26 29}
   {-42 -45 29}
   {33 25 -6}
   {-45 -5 7}
   {-7 28 -6}
   {-48 31 -11}
   {32 16 -37}
   {-24 48 1}
   {18 -46 23}
   {-30 -50 48}
   {-21 39 -2}
   {24 47 42}
   {-36 30 4}
   {-5 28 -1}
   {-47 32 -42}
   {16 37 -22}
   {-43 42 -34}
   {-40 39 -20}
   {-49 29 6}
   {-41 -3 39}
   {-16 -12 43}
   {24 22 3}
   {47 -45 43}
   {45 -37 46}
   {-9 26 5}
   {-3 23 -13}
   {5 -34 13}
   {12 39 13}
   {22 50 37}
   {19 9 46}
   {-24 8 -27}
   {-28 7 21}
   {8 -25 50}
   {20 50 4}
   {27 36 13}
   {26 31 -25}
   {39 -44 -32}
   {-20 41 -10}
   {49 -28 35}
   {1 44 34}
   {39 35 -11}
   {-50 -42 -7}
   {-24 7 47}
   {-13 5 -48}
   {-9 -20 -23}
   {2 17 -19}
   {11 23 21}
   {-45 30 15}
   {11 26 -24}
   {38 33 -13}
   {44 -27 -7}
   {41 49 2}
   {-18 12 -37}
   {-2 12 -26}
   {-19 7 32}
   {-22 11 33}
   {8 12 -20}
   {16 40 -48}
   {-2 -24 -11}
   {26 -17 37}
   {-14 -19 46}
   {5 47 36}
   {-29 -9 19}
   {32 4 28}
   {-34 20 -46}
   {-4 -36 -13}
   {-15 -37 45}
   {-21 29 23}
   {-6 -40 7}
   {-42 31 -29}
   {-36 24 31}
   {-45 -37 -1}
   {3 -6 -29}
   {-28 -50 27}
   {44 26 5}
   {-17 -48 49}
   {12 -40 -7}
   {-12 31 -48}
   {27 32 -42}
   {-27 -10 1}
   {6 -49 10}
   {-24 8 43}
   {23 31 1}
   {11 -47 38}
   {-28 26 -13}
   {-40 12 -42}
   {-3 39 46}
   {17 41 46}
   {23 21 13}
   {-14 -1 -38}
   {20 18 6}
   {-50 20 -9}
   {10 -32 -18}
   {-21 49 -34}
   {44 23 -35}
   {40 -19 34}
   {-1 6 -12}
   {6 -2 -7}
   {32 -20 34}
   {-12 43 -29}
   {24 2 -49}
   {10 -4 40}
   {11 5 12}
   {-3 47 -31}
   {43 -23 21}
   {-41 -36 -50}
   {-8 -42 -24}
   {39 45 7}
   {7 37 -45}
   {41 40 8}
   {-50 -10 -8}
   {-5 -39 -14}
   {-22 -24 -43}
   {-36 40 35}
   {17 49 41}
   {-32 7 24}
   {-30 -8 -9}
   {-41 -13 -10}
   {31 26 -33}
   {17 -22 -39}
   {-21 28 3}
   {-14 46 23}
   {29 16 19}
   {42 -32 -44}
   {-24 10 23}
   {-1 -32 -21}
   {-8 -44 -39}
   {39 11 9}
   {19 14 -46}
   {46 44 -42}
   {37 23 -29}
   {32 25 20}
   {14 -43 -12}
   {-36 -18 46}
   {14 -26 -10}
   {-2 -30 5}
   {6 -18 46}
   {-26 2 -44}
   {20 -8 -11}
   {-31 3 16}
   {-22 -9 39}
   {-49 44 -42}
   {-45 -44 31}
   {-31 50 -11}
   {-32 -46 2}
   {-6 -7 17}
   {19 -32 48}
   {39 20 -10}
   {-22 -37 38}
   {-31 9 -48}
   {40 12 7}
   {-24 -4 9}
   {-22 49 33}
   {-12 43 10}
   {25 -30 -10}
   {46 47 31}
   {13 27 -7}
   {-45 32 -35}
   {-50 34 9}
   {2 34 30}
   {3 16 2}
   {-18 45 -12}
   {33 37 10}
   {43 7 -18}
   {-22 44 -19}
   {-31 -27 -42}
   {-3 -40 8}
   {-23 -31 38}})

;(dpll (between 1 20) problem50) ;
(dpll (between 1 50) problem50) ; 3:45.34