Github issue is now under https://github.com/sagemath/sage/issues/35851 Dima Pasechnik schrieb am Dienstag, 27. Juni 2023 um 11:14:34 UTC+2:
> On Tue, Jun 27, 2023 at 4:37 AM Maximilian Wittmann <wittm...@live.de> > wrote: > > > > 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! > > 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 > . > -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/c3f8c0d3-31a7-4629-844d-a28b32968fc0n%40googlegroups.com.
