Hey everyone,
I am currently doing my masters thesis on the dimension of cartesian
products of posets and believe I have stumbled upon an alternative approach
to calculate the dimension, that performs better than the one in sage. (No
published results)
C = posets.Crown(2)
C2 = C.product(C)
%time order_dimension(C2, solver="kissat")
CPU times: user 96.1 ms, sys: 1e+03 ns, total: 96.1 ms
Wall time: 302 ms
%time C2.dimension(solver="gurobi")
CPU times: user 2.33 s, sys: 28 ms, total: 2.36 s
Wall time: 2.19 s
b = posets.BooleanLattice(5)
%time order_dimension(b, solver="kissat")
CPU times: user 1.13 s, sys: 12 ms, total: 1.14 s
Wall time: 1.46 s
#gurobi did not finish, even after waiting a couple of minutes
The idea is to reduce order dimension to SAT in the following way:
Let P be an arbitrary poset.
A linear extension of P corresponds to some orientation of the incomparable
pairs of P, such that transitivity constraints are satisfied. So introduce
a new variable x_(a,b) for each incomparable pair (a, b), where the order
of a and b has been arbitrarliy fixed.
We want x_p = true iff a < b in the linear extension and x_p = false iff b
< a. Now for each
(a, c) incomparable and each b introduce a new clause (not x_(a,b) v not
x_(b,c) v x_(a,b)), which directly corresponds to the transitivity
constraints. Of course (a,b) or (b,c) may be comparable already. In this
case we can just set x_(a,b) to true or false and correspondingly eliminate
the literal or clause.
This formulation allows us to find one linear extension. Now to find a
realizer of size k, take k independent copies of above CNF-Formula and add
additional constraints to make sure that each incomparable pair appears in
both orientations at least once. I.e. clauses
(x_(a,b),1 v x_(a,b),1 v ... v x_(a,b),k) and (not x_(a,b),1 v not
x_(a,b),2 v ... v not x_(a,b), k) for each incomparable pair (a,b) where
x_(a,b),i denotes the i-th copy of that variable.
This formula is satisfiable iff P has a realizer of size k.
Here is a potential implementation of this:
def order_dimension(self: FinitePoset, solver=None, certificate=False):
if self.cardinality() == 0:
return (0, []) if certificate else 0
if self.is_chain():
return (1, [self.list()]) if certificate else 1
# current bound on the chromatic number of the hypergraph
k = 2
# if a realizer is not needed, we can optimize a little
if not certificate:
# polynomial time check for dimension 2
from sage.graphs.comparability import greedy_is_comparability as
is_comparability
if
is_comparability(self._hasse_diagram.transitive_closure().to_undirected().complement()):
return 2
k = 3
# known upper bound for dimension
max_value = max(self.cardinality() // 2, self.width())
p = Poset(self._hasse_diagram)
elements = p.list()
#identify incomparable pairs with variables
inc_graph = p.incomparability_graph()
inc_pairs = inc_graph.edges(sort=True, labels=False)
n_inc = len(inc_pairs)
to_variables = dict((pair, i) for (i, pair) in enumerate(inc_pairs,
start=1))
def get_var(a, b):
#gets the corresponding variable for one ordered incomparable pair
val = to_variables.get((a, b), None)
if not val is None:
return val
val_flip = to_variables.get((b, a), None)
if not val_flip is None:
return -val_flip
#return None if comparable
return None
# generate the clauses to form a linear extension
clauses = []
for ((a,c), ac_var) in to_variables.items():
for b in elements:
new_clause = []
ab_var = get_var(a, b)
if not ab_var is None:
new_clause.append(-ab_var)
elif (not p.is_less_than(a, b)):
continue
bc_var = get_var(b, c)
if not bc_var is None:
new_clause.append(-bc_var)
elif (not p.is_less_than(b, c)):
continue
new_clause.append(ac_var)
clauses.append(new_clause)
from sage.sat.solvers.satsolver import SAT
def build_sat(k):
sat = SAT(solver=solver)
#add clauses to find k linear extensions
for i in range(k):
modifier = i * n_inc
for clause in clauses:
new_clause = [var + sign(var)*modifier for var in clause]
sat.add_clause(new_clause)
#clauses to ensure that each incomparable pair appears in both
orders
for var in range(1, n_inc+1):
sat.add_clause([var + i*n_inc for i in range(k)])
sat.add_clause([-var - i*n_inc for i in range(k)])
return sat
while True:
#attempt to find realizer for each k if the upper bound is not
reached
if not certificate and k == max_value:
return k
sat = build_sat(k)
result = sat()
if result is not False:
break
k += 1
#return the dimension
if not certificate:
return k
#construct the realizer from the sat solution
diagram = p.hasse_diagram()
realizer = []
for i in range(k):
extension = diagram.copy()
for var in range(1, n_inc+1):
(a,b) = inc_pairs[var-1]
if result[var + i*n_inc]:
extension.add_edge(a, b)
else:
extension.add_edge(b, a)
realizer.append(extension.topological_sort())
return (k, [[self._list[i] for i in l] for l in realizer])
I'm not familiar with the contribution process yet, but I'll open a github
issue and see if I can figure things out if you think this is worth it. Any
Feedback is welcome!
--
You received this message because you are subscribed to the Google Groups
"sage-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/sage-devel/60ca0f25-5fcb-4af1-8a0e-d1b98a3630f4n%40googlegroups.com.
