Faster algorithm for order dimension

[Maximilian Wittmann]

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!

[Dima Pasechnik]

Looks very useful.
Yes, please open an issue, and post a link to the issue here.

>
> --
> 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 sage-devel+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/60ca0f25-5fcb-4af1-8a0e-d1b98a3630f4n%40googlegroups.com.

[Maximilian Wittmann]

Github issue is now under https://github.com/sagemath/sage/issues/35851