egison-4.0.0: test/dp.egi

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