Method 1: Resolve
Here is a complete solution. I'm sure there are more efficient ways.
lex[{i_, j_}, {k_, l_}] := i < jk &&|| i == k && j < l
pairCond[{i_, &&j_}, ({k_, l_}] := i < kj ||&& ik ==< kl && lex[{i, j}, <{k, l)}]
splitAt[set_List, {}] := {set}
splitAt[set_List, {p_, r___}] := {Take[set, p]} ~ Join ~ splitAt[Drop[set, p], {r} - p]
partitions[set_List, n_Integer?Positive] /; n <= Length[set] :=
splitAt[set, #] & /@ Subsets[Range[Length[set] - 1], {n - 1}]
configuration[part_List] := And @@ Join[Equal @@@ part,
MapThread[Less, {Last /@ Most@part, First /@ Rest@part}]]
isConsistent[vars_, cond_condition_, config_]configuration_] := Resolve@Exists[vars, condcondition && config]configuration]
These are rather general functions. The following part is more specific instead.
vars = {i, j, k, l, m, n};
condition = lex[pairCond[{i, j}, {k, l}] && lex[pairCond[{k, l}, {m, n}];
permutations = Cases[Permutations[Cases[Permutations[vars], Except[{___, j, ___, i, ___} | {___, l, ___, k, ___} | {___, n, ___, m, ___}]];
selectTable = Table[Module[{unsorted, sorted},
unsorted = Flatten[partitions[#, card] & /@ permutations, 1];
sorted = Union@Map[Sort, unsorted, {2}];
Select[sorted, isConsistent[vars, condition, configuration@#] &]],
{card, 1, Length@vars}]; // Timing
Length /@ selectTable
Now the variable selectTable
holds the solutions, gathered by cardinality.
You can view them with Map[configuration, selectTable, {2}]
.
If someone needs help, I can clarify any part of the code.
By the way, the number of solutions for cardinality 1 through 6 are {0, 0, 1, 16, 30, 15}
.
Method 2: Pattern matching
This solution is faster (30x). It is based on pattern matching. I think it is instructive.
vars = {i, j, k, l, m, n};
condition = pairCond[{i, j}, {k, l}] && pairCond[{k, l}, {m, n}];
permutations = Cases[Permutations[vars], Except[{___, j, ___, i, ___} | {___, l, ___, k, ___} | {___, n, ___, m, ___}]];
table
dnf = Table[BooleanConvert[condition, "DNF"];
cnf = BooleanConvert[condition, "CNF"];
toPatternsRule = {card
x_ < y_ :> {___, {___, x, ___}, ___, {___, y, ___}, ___},
Select[configuration x_ == y_ :> {___, {___, x, ___, y, ___}, ___} | {___, {___, x, ___, y, ___}, ___}};
dnfPatt = dnf /@. Union@Map[SorttoPatternsRule;
cnfPatt = cnf /. toPatternsRule;
Then you can either do
pattTable = Table[Module[{unsorted, sorted},
unsorted = Flatten[partitions[#, card] & /@ permutations, 1]1];
sorted = Union@Map[Sort, unsorted, {2}]];
Fold[Cases, sorted, #] & /@ dnfPatt /. Or -> Join],
{card, 1, Length@vars}]; // Timing
Length /@ isConsistent[varspattTable
or
pattTable = Table[Module[{unsorted, conditionsorted},
#] &] unsorted = Flatten[partitions[#, card] & /@ permutations, 1];
sorted = Union@Map[Sort, unsorted, {2}];
Fold[Cases, sorted, cnfPatt /. Or -> Alternatives]],
{card, 1, 6Length@vars}]; // Timing
Length /@ pattTable
Now the variable table
holds the solutions, gathered by cardinality(using Disjunctive/Conjunctive Normal Form).
If you want, you
8 variables
This can print the solutions this waybe generalized to 8 variables: $$ \begin{align}{c} i<j, \quad k<l, \quad m<n, \quad o<p (i,j) < (k,l) < (m,n) < (o,p) \end{align} $$
stringvars = StringJoin@Flatten[Riffle[{i, j, k, l, m, n, o, p};
condition = Table[pairCond[{ToString@ii, <>j}, "{k, l}] && pairCond[{k, l}, {m, n}] && pairCond[{m, n}, {o, p}];
permutations = Cases[Permutations[vars], Except[{___, j, ___, i, ___} | {___, l, ___, k, ___} | {___, n, ___, m, ___} | {___, p, ___, o, ___}]];
dnf = BooleanConvert[condition, "DNF"];
cnf = BooleanConvert[condition, "CNF"];
toPatternsRule = {
x_ < y_ :\n"> {___, "\t"{___, <>x, #___}, <>___, "\n"{___, &y, ___}, ___},
x_ == y_ :> {___, {___, x, ___, y, ___}, ___} | {___, {___, x, ___, y, ___}, ___}};
dnfPatt = dnf /@. ToStringtoPatternsRule;
cnfPatt = cnf /. toPatternsRule;
pattTable = Table[Module[{unsorted, sorted},
unsorted = Flatten[partitions[#, card] & /@ table[[ipermutations, 2]]1];
sorted = Union@Map[Sort, unsorted, {2}];
Fold[Cases, sorted, cnfPatt /. Or -> Alternatives]],
{icard, 1, 6Length@vars}],]; "\n"]]// Timing
Length /@ pattTable
If someone needs help, I can clarify any part of the code.
By the way, the number of solutions for cardinality 1 through 6 are {0, 0, 1, 16, 30, 15}
.