# Finding simpler implied formulas while preserving contradiction

I have two Presburger formulas A and B such that A∧B≡False. From these I need to find "simpler" formula A′ (as simple as I can make it) such that A→A′ and A′∧B≡False. Is there any simple way to automate this for largish formulas in Mathematica? The formulas start off in sum of products form, with thousands of products and less than 20 variables. I'm already using FullSimplify to simplify A and B preserving equivalence, but I need to go even simpler, hence this weaker set of conditions.

-
Welcome to Mathematica.SE? Your question would be easier to answer if you included the (valid) Mathematica code that you have been using so far. – Verbeia May 13 '14 at 3:37
All I am doing so far is applying FullSimplify in an ad hoc way in the notebook. E.g. to test whether A and B contradict I evaluate FullSimplify[A&&B]. The input formulas are sums of products that look something like "(a==1&&b==3)||(a==2&&b==3)||.." – Presburger May 13 '14 at 3:55
Have you tried BooleanMinimize? – Daniel Lichtblau May 13 '14 at 14:34
Yes. That won't work, because I need to go from, say, "(a==1&&b==1)||(a==2&&b==2)" to "a==b". – Presburger May 13 '14 at 21:45