Dense linear order on graphs

[jakobnordstrom]

I would like to have the dense linear ordering formulas of Atserias-Dalmau (are the standard versions of DLO formulas available in CNFgen, BTW?) but relative to a (sparse) graph.

In th standard DLO formulas there are variables z_{i,j,k} for all tuples i!=j!=k!=i encoding that e_j is strictly between e_i and e_k, and the formula says that if x_{i,k} is true, then there exists a j such that z_{i,j,k} is true.

The idea in the graph formulas would be to have variables z_{i,j,k} only for j \in N(i) \cup N(k) and require that some such e_j in the neighbourhood witnesses e_i < e_j < e_k if e_i < e_k.

From a practical point of view, the reason for this to be interesting would be that there would be a second type of formula with large width complexity but small size complexity on which one could run experiments to check if the same kind of things happen as for POP. As it is now, DLO formulas blow up way too quickly, and one gets by far too few data points to be able to say anything interesting.