literal := integer deleteLiteral l cnf := map (\matchAll as multiset integer with | (!#l & $x) :: _ -> x) cnf deleteClausesWith l cnf := matchAll cnf as multiset (multiset integer) with | (!(#l :: _) & $c) :: _ -> c assignTrue l cnf := deleteLiteral (neg l) (deleteClausesWith l cnf) resolveOn v cnf := matchAll cnf as multiset (multiset integer) with | {(#v :: (@ & $xs)) :: (#(neg v) :: (@ & $ys)) :: _, !($l :: _, #(neg l) :: _)} -> unique (xs ++ ys) dp vars cnf := match (vars, cnf) as (multiset literal, multiset (multiset literal)) 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)) assertEqual "dp" (dp [1] [[1]]) True assertEqual "dp" (dp [1] [[1],[-1]]) False assertEqual "dp" (dp [1,2,3] [[1,2],[-1,3],[1,-3]]) True assertEqual "dp" (dp [1,2] [[1,2],[-1,-2],[1,-2]]) True assertEqual "dp" (dp [1,2] [[1,2],[-1,-2],[1,-2],[-1,2]]) False assertEqual "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]]) True assertEqual "dp" (dp [1,2] [[-1,-2],[1]]) True