Here's some work-in-progress code I have been playing with.
First we define a helper function which attempts to combine And
ed comparisons (which result when using functions such as LogicalExpand
) into Inequality
, Equal
and Unequal
chains. It does this by making graphs of expressions, and finding paths connected components and cliques on them. It doesn't try to move components of comparison between sides of the comparison operator - there's clearly room for improvement in that regard.
ClearAll[collectInequalityChains];
collectInequalityChains[eq_] :=
Module[{
normeq,
eqExtract, eqExtractStep,
ineqExtract, ineqExtractStep,
uneqExtract, uneqExtractStep},
normeq = BooleanMinimize@LogicalExpand@eq //. {
a_ > b_ :> b < a,
a_ >= b_ :> b <= a};
ineqExtractStep[{graph_Graph, ineqs_List}] :=
Module[{largestpath, pathedges},
largestpath =
First@TakeLargestBy[
Flatten[FindPath[graph, Sequence @@ #, Infinity, All] & /@
Flatten[{#, Reverse@#} & /@ Subsets[VertexList@graph, {2}],
1], 1], Length, 1];
pathedges = DirectedEdge @@@ Partition[largestpath, 2, 1];
{Subgraph[graph,
DeleteCases[EdgeList@graph, Alternatives @@ pathedges],
EdgeLabels -> PropertyValue[graph, EdgeLabels]],
Append[ineqs,
Inequality @@
Riffle[largestpath,
PropertyValue[{graph, #}, EdgeLabels] & /@ pathedges]]}];
ineqExtract[graph_Graph] :=
And @@ Last@
NestWhile[ineqExtractStep, {graph, {}},
Not@*EmptyGraphQ@*First];
eqExtractStep[{graph_Graph, eqs_List}] :=
Module[{largestconnected},
largestconnected =
First@TakeLargestBy[ConnectedComponents@graph, Length, 1];
{GraphDifference[graph,
Subgraph[graph, largestconnected]],
Append[eqs, largestconnected]}];
eqExtract[graph_Graph, op_Symbol] :=
And @@ (op @@@
NestWhile[eqExtractStep, {graph, {}},
Not@*EmptyGraphQ@*First][[2]]);
uneqExtractStep[{graph_Graph, eqs_List}] :=
Module[{largestconnected},
largestconnected =
First@TakeLargestBy[FindClique@graph, Length, 1];
{GraphDifference[graph,
Subgraph[graph, largestconnected]],
Append[eqs, largestconnected]}];
uneqExtract[graph_Graph, op_Symbol] :=
And @@ (op @@@
NestWhile[uneqExtractStep, {graph, {}},
Not@*EmptyGraphQ@*First][[2]]);
MapAt[eqExtract[Graph[UndirectedEdge @@@ Cases[#, _Equal, {0, 1}]],
Equal] &&
uneqExtract[Graph[UndirectedEdge @@@ Cases[#, _Unequal, {0, 1}]],
Unequal] &&
ineqExtract[
Graph[Property[DirectedEdge @@ #, EdgeLabels -> Head@#] & /@
Cases[#, _Less | _LessEqual, {0, 1}]]] &, normeq,
Most /@ Position[normeq, And]]]
A simple example:
collectInequalityChains[
a < b && c >= b && a == d && d == e || b > a || x != y && y != z]
(d == a == e && a < b <= c) || (y != x && y != z) || a < b
Then we use this function as prettifier in a function which attempts to simplify inequalities by searching exhaustively for equivalence of original inequality and transformed variants of it. These variants either leave an comparison unchanged, replace it with True
or False
, or expand open inequality to closed one. The variant with smallest LeafCount
after collectInequalityChains
is given out as the solution.
ClearAll[simplifyComparisons];
simplifyComparisons[ineqtmp_, vars_] :=
Module[{ineq, eqpos, ineqpos, eqtrans, ineqtrans},
ineq = BooleanMinimize@LogicalExpand@ineqtmp;
eqpos = Position[ineq, _Equal | _Unequal];
ineqpos =
Position[ineq, _Less | _LessEqual | _Greater | _GreaterEqual];
eqtrans =
Thread[eqpos -> MapThread[#1[Extract[ineq, #2]] &, {#, eqpos}]] & /@
Tuples[{Identity, True &, False &}, Length@eqpos];
ineqtrans =
Thread[ineqpos ->
MapThread[#1[Extract[ineq, #2]] &, {#, ineqpos}]] & /@
Tuples[{Identity, # /. {Less -> LessEqual,
Greater -> GreaterEqual} &, True &, False &}, Length@ineqpos];
First@TakeSmallestBy[
collectInequalityChains@ReplacePart[ineq, #] & /@
Select[Flatten[Table[Join[a, b], {a, eqtrans}, {b, ineqtrans}],
1],
Resolve[
ForAll[vars,
Evaluate[ineq \[Equivalent] ReplacePart[ineq, #]]],
Reals] &], LeafCount, 1]]
Now we can simplify our original toy problem:
simplifyComparisons[
x == 0 && y == 0 || x > 0 && -x <= y <= x, {x, y}]
-x <= y <= x