Poset dimension SAT reduction

[tiwwi]

Is there an existing issue for this?

• [X] I have searched the existing issues for a bug report that matches the one I want to file, without success.

Problem Description

I recently came upon a SAT reduction for calculating the order dimension of a poset, that performs better than the one in sage, which I would like to contribute. This performs better than the current implementation in practice.

Instead of calculating a hypergraph colouring with potentially many edges, we calculate the order dimension by searching for transitive orientations of incomparable elements and introducing additional constraints such that each incomparable (ordered) pair is covered.

Proposed Solution

I would like to implement this algorithm.

Alternatives Considered

There is also an alternative formulation of the hypergraph colouring, which I have not tested yet.

Additional Information

See also: https://groups.google.com/g/sage-devel/c/uNhq1N3JhdI

[dimpase]

Has the maths part been run by a human already, written up?

[tscrim]

@fchapoton

[tiwwi]

Sorry for the late response, I've been down with a cold the last couple of days (still am actually).

Has the maths part been run by a human already, written up?

I've ran it past my advisor, but not in writing. I think we both considered it a pretty natural approach. I'll be having another meeting with him next week, if you prefer he checks it in more detail.

[tiwwi]

It's been a while, but I still hope to contribute this so: I have included the relevant pages of my thesis below, if you want to see the details. My thesis has now also been reviewed by my advisors and they agreed with this approach.

Part of my thesis: sat_orders.pdf

Just let me know if you want me to start up a PR!

[dimpase]

Sure, PRs like this are very much welcome. We have our own issues with SAT implementations in Sage being either slow, or buggy, or both, however, so please be extra alert with these. Do you use cryptominisat? (an optional package - should be faster than whatever built-in SAT solver we have). We have cryptominisat version 5.8.0 (from 2021), but the current one is 5.11.21.

I'll check whether this is easy to upgrade.

[tiwwi]

I was using the default SAT solver and kissat (which sage also interfaces with, if it is installed, I think). Personally, I didn't encounter any issues with SAT, so I'm reasonably optimistic that this should work out

[dimpase]

you wrote that Sage's dimension computation was slow - this could be in part due to the SAT solver

[tiwwi]

Currently, sage uses a MILP formulation that mostly uses different ideas. This performs worse than the SAT version when

• comparing the default MIP solver to the default SAT solver
• comparing gurobi to kissat

If you prefer, I could also encode the ideas from the SAT formulation as a MILP. I have not tested this yet, but I am optimistic that our formulation performs better.

[dimpase]

@tiwwi - could you try an update of cryptominisat here: #37669 (and try your SAT computations with cryptominisat rather than other SAT solvers)?

[tiwwi]

@dimpase Yeah sure, I'll see if I can get this to work and then hopefully provide some more detailed benchmarks.