Finding simpler implied formulas while preserving contradiction

Question

I have two Presburger formulas A and B such that $A\land B \equiv \text{False}$. From these I need to find shorter formula $A'$ such that $A \rightarrow A'$ and $A' \land B \equiv \text{False}.$ The size of A' does not have to be as short as is possible, but shorter is better. Is there a well-known process for calculating this? Ideally I am looking for an algorithmic simplifier that can handle largish formula (less than 10 variables, sum of products form with thousands of small products).