def deleteLiteral l cnf :=
  map
    (\c -> matchAll c as multiset integer with
        | ((!#l) & $x) :: _ -> x)
    cnf

def deleteClausesWith l cnf :=
  matchAll cnf as multiset (multiset integer) with
    | ((!(#l :: _)) & $c) :: _ -> c

def assignTrue l cnf := deleteLiteral (neg l) (deleteClausesWith l cnf)

def resolveOn v cnf :=
  matchAll cnf as multiset (multiset integer) with
    | {(#v :: (@ & $xs)) :: (#(neg v) :: (@ & $ys)) :: _,
       !( $l :: _, #(neg l) :: _ )} ->
      unique (xs ++ ys)

def dp vars cnf :=
  match (vars, cnf) as (multiset integer, multiset (multiset integer)) with
  -- satisfiable
  | (_, []) -> True
  -- unsatisfiable
  | (_, [] :: _) -> False
  -- 1-literal rule
  | (_, [$l] :: _) -> dp (delete (abs l) vars) (assignTrue l cnf)
  -- pure literal rule (positive)
  | ($v :: $vs, !((#(neg v) :: _) :: _)) -> dp vs (assignTrue v cnf)
  -- pure literal rule (negative)
  | ($v :: $vs, !((#v :: _) :: _)) -> dp vs (assignTrue (neg v) cnf)
  -- otherwise
  | ($v :: $vs, _) ->
    dp vs
       ((resolveOn v cnf) ++ (deleteClausesWith v (deleteClausesWith (neg v) cnf)))

assert "dp" (dp [1] [[1]])
assert "dp" (not (dp [1] [[1], [-1]]))
assert "dp" (dp [1, 2, 3] [[1, 2], [-1, 3], [1, -3]])
assert "dp" (dp [1, 2] [[1, 2], [-1, -2], [1, -2]])
assert "dp" (not (dp [1, 2] [[1, 2], [-1, -2], [1, -2], [-1, 2]]))
assert "dp" (dp [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]])
assert "dp" (dp [1, 2] [[-1, -2], [1]])