Variants of Dense Ordering Principle (from Jakob Nordstrom)
MassimoLauria opened this issue · 0 comments
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).