Mathematica Stack Exchange is a question and answer site for users of Mathematica. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|improve this question
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.