let remove_redundant_conflicts deps confl =
  let conj_deps p =
    let f = PTbl.get deps p in
    Formula.fold
      (fun d s -> match Disj.to_lit d with Some p -> PSet.add p s | None -> s)
      f PSet.empty
  in
  Conflict.iter confl
    (fun p1 p2 ->
       let d1 = conj_deps p1 in
       let d2 = conj_deps p2 in
       if
         PSet.exists
           (fun q1 ->
              PSet.exists
                (fun q2 ->
                   (p1 <> q1 || p2 <> q2) &&
                   (p1 <> q2 || p2 <> q1) &&
                   Conflict.check confl q1 q2)
                d2)
           d1
       then begin
         Conflict.remove confl p1 p2
       end);
  let try_remove_conflict p1 p2 =
    let f1 = PTbl.get deps p1 in
    let d2 = conj_deps p2 in
    if
      Formula.exists
        (fun d1 ->
           Disj.for_all
             (fun q1 ->
                PSet.exists
                  (fun q2 ->
                     (p1 <> q1 || p2 <> q2) &&
                     (p1 <> q2 || p2 <> q1) &&
                     Conflict.check confl q1 q2)
                  d2)
             d1)
        f1
    then begin
      Conflict.remove confl p1 p2
    end
  in
  Conflict.iter confl try_remove_conflict;
  Conflict.iter confl (fun p1 p2 -> try_remove_conflict p2 p1);
  (* We may now be able to remove some dependencies *)
  PTbl.map (simplify_formula confl) deps