Variants of Dense Ordering Principle (from Jakob Nordstrom)

[MassimoLauria]

This connects to pull request #83 issues #71

(from Jakob Nordstrom)

Here comes a feature request for variants of dense linear order formulas. If anyone of you feels this is something that could/should be implemented, then please just copy the text below to a new issue (but otherwise I am thinking it might not be worth it).

The different variants of DLO have arisen in the context of different proof complexity discussions, and it seems it would be interesting to have them implemented so that one could run experiments in practice also.

The reason this might be interesting is that results for partial ordering principle formulas are really intriguing in many ways, and so it is interesting to look for other formulas that might cause similar effects (or maybe other, also interesting, effects).

Modulo typos, please find a description below of the versions I have in mind. As always, the formula talks about a finite set of elements {e_1, e_2, ..., e_n} which is ordered, and furthermore the formula claims that this order is dense, i.e., if e_i < e_k, then there is some e_j such that e_i < e_j < e_k (which is impossible, since the set is finite).

The variables are:

(i) x_{i,j} for i,j \in [n], i != j, meaning that "e_i < e_j" holds.

(ii) z_{i,j,k} for i,j,k \in [n], i != j k != i, where z_{i,j,k}=TRUE is taken to mean "e_i < e_j and e_j < e_k definitely holds." What z_{i,j,k}=FALSE means will depend on the exact version of the formula.

Given a positive integer n, all clauses below are to be generated for all i,j,k \in [n] such that i != j k != i as applicable.

(A) STANDARD DENSE LINEAR ORDER FORMULA

The standard version consists of clauses:

(1) NOT x_{i,j} OR NOT x_{j,i} [anti-symmetry]

(2) x_{i,j} OR x_{j,i} [totality/linearity]

(3) NOT x_{i,j} OR NOT x_{j,k} OR x_{i,k} [transitivity]

(4) NOT x_{i,k} OR OR_{j \in [n]{i,k}} z_{i,j,k} [density]

(5) NOT z_{i,j,k} OR x_{i,j}

(6) NOT z_{i,j,k} OR x_{j,k}

(7) z_{i,j,k} OR NOT x_{i,j} OR NOT x_{j,k}

In this version, clauses (5)-(7) state that the z-variables are used to encode the equivalence "z_{i,j,k} <==> x_{i,j} AND x_{j,k}".

(B) WITNESSING DENSE LINEAR ORDER FORMULA

Clauses (1)-(6) above, but not clauses (7).

This means that although there may exist many triples e_i < e_j < e_k, the z-variables don't need to pick more than one j for every i,k such that e_i < e_k. It turns out that clauses (7) are not needed for short resolution proofs (as shown by Sagnik Mukhopadhyay and Susanna F. de Rezende), and so CDCL solvers should still be able to run fast on these formulas.

(C) DENSE PARTIAL ORDER FORMULA

Clauses (1) and (3)-(7) plus a new single clause

(8) OR_{i \in [n]} OR_{j \in [n]{i}} x_{i,j} ,

but not clauses (2).

This means that we have not a linear but a partial ordering, where the clause (8) guarantees that there is at least one pair e_i < e_j (because otherwise it is no fun and the formula is satisfiable). I would need to double-check the details to be perfectly sure, but I am fairly confident that the short resolution proof that works for (B) also works for this version.

(D) WITNESSING DENSE PARTIAL ORDER FORMULA

Clauses (1) and (3)-(6) plus a new single clause

(8) OR_{i \in [n]} OR_{j \in [n] \ {i}} x_{i,j} ,

but not clauses (2) or (7). This is just the natural combination of variants (B) and (D).

And then we want to do graph-based versions for all of these formulas. What this means is that we also get a an undirected graph G = (V, E) with V = [n] as input and change the density axioms to

(9) NOT x_{i,k} OR OR_{j \in N(i) \cup N(j)} z_{i,j,k}

(that is, if e_i < e_k, then the fact that the order is dense is witnessed by some e_j such that the vertex j is a neighbour of either i or k).

(E) GRAPH-BASED DENSE LINEAR ORDER FORMULA

Clauses (1)-(3) and (5)-(7) plus (9) instead of (4).

Dmitry Sokolov and Sagnik Mukhopadhyay have proven that a width lower bound Omega(n) hold for these formulas provided that the graph is a good enough expander.

(F) GRAPH-BASED WITNESSING DENSE LINEAR ORDER FORMULA

As version (B) but clauses (9) instead of clauses (4), i.e., the formula consists of clauses (1)-(3), (5)-(6), and (9).

(G) GRAPH-BASED DENSE PARTIAL ORDER FORMULA

As version (C) but clauses (9) instead of clauses (4).

(H) WITNESSING DENSE PARTIAL ORDER FORMULA

As version (D) but clauses (9) instead of clauses (4).