Cheap variations/alternatives to linear models?

Stream: Equational

[Matthew House]

As a project for fun, I've been trying to search for 1-bases for certain equational theories of ortholattices, in the style of McCune. Right now, I have a theory T and 7928 candidate equations of order 15 that may be equivalent to T. T implies all of them, yet I suspect that none of them imply T (since ATPs go nowhere). My big bottleneck right now is trying to find enough "candidate + anti-T" countermodels to filter them all out.
Prior to order 15, it has sufficed to perform naive general searches, but I've pretty much exhausted what can be found in a reasonable time. So I looked into linear models, which turned out to be somewhat successful, filtering out 694/7928 candidates using $\mathbb Z/p\mathbb Z$ for $p\leq10^6$.
(T's nontrivial models are all even in size, so practically any linear model for a candidate will have odd order and automatically end up being anti-T. That means I only really have to search for linear models satisfying the positive equalities, and $\mathbb Z/p\mathbb Z$ suffices to cover any finite ring built from $\mathbb Z/p^n\mathbb Z$ or $\mathbb F_{p^n}$, if I'm not mistaken.)
However, I've also hit a wall with the naive $\mathbb Z/p\mathbb Z$ search: it has not been able to filter out any equation with more than 4 variables (presumably due to the equations for $a,b$ being overdetermined), nor is it able to solve any equation that demands a nontrivial zero divisor (e.g., $a^2=0$). I've tried switching to $\mathrm M_2(\mathbb Z/p\mathbb Z)$ to get around the zero-divisor issue, but it ends up being extremely slow in SageMath (maybe I'm doing it wrong).
Are there any cheap variations on linear models that can get around these difficulties? For zero divisors, it seems like matrix rings ought to help, but I'm not sure what software or methods work best for those, nor for noncommutative rings in general. The ETP paper gestures at rewrite systems, but I'm not nearly enough of an expert to know how to turn that into a solution search. Meanwhile, for the too-many-variables issue, I'm not sure if there's anything that could possibly work.
(Or are there nice methods outside of general searches and linear models that can be applied relatively easily to a "big bag of equations"? Greedy constructions may be workable, but many of the other methods in the ETP paper seem to involve manual effort per equation.)

[Bruno Le Floch]

It would be useful to have some examples of your equations, or even the full list in a file attachment, to take a look. In the Higman-Neumann work (order 8 laws characterizing group division) it was better to check separately whether E⊨associativity and E⊨E8 etc, rather than directly whether E⊨E42323216, an order 8 law known to characterize group division. Another intermediate question was whether E⊨cancellativity (for ortholattices this is not relevant but there may be variants). Some proofs initially took 10 CPU-hours before getting reduced to a few seconds with better parameter choices.

[Bruno Le Floch]

Since you are looking for countermodels of E⊨T for some law E and theory T that implies E, you can start with a model of T (an ortholattice) and look for cohomological extensions of it that obey E but not T. Namely, seek a countermodel with carrier L×M with L an ortholattice and (M,◇) a linear model of T (an ortholattice whose operation is linear with respect to some abelian group operation +, so (x+y)◇(z+w)=(x◇z)+(y◇w) I think), and with an operation (l₁,x₁)◇(l₂,x₂) = (l₁◇l₂,x₁◇x₂+f(l₁,l₂)). Then E and T become linear equations on the function f, and the hope is that one does not imply the other.

[Bruno Le Floch]

Actually, what operation on ortholattices are you considering as your magma operation? In our commentary files, I wrote commentary/Equation40894397952.md about x = (((y ◇ x) ◇ (x ◇ z)) ◇ w) ◇ (x ◇ ((x ◇ ((y ◇ y) ◇ y)) ◇ z)):

The ortholattice Sheffer stroke law

It was shown by McCune, Padmanabhan, Rose, Veroff that a magma operation satisfies this law if and only if it is the Sheffer stroke of an ortholattice.

This order 10 law with four variables has the lowest possible order, but there might exist equivalent three-variable laws.

[Matthew House]

Indeed, I'm taking the Sheffer stroke $x\diamond y=(x'\vee y')$ as in McCune, then defining $x'=x\diamond x$ and $x\vee y=x'\diamond y'$ when testing the lattice axioms. The specific theory T is Pavicic's & Megill's weakly orthomodular lattices (WOMLs), which are a superset of the orthomodular lattices in my McCune link. For my general searches, I'm currently using the ortholattice axiomatization (A1) $x=x''$; (A2) $x\vee y=y\vee x$; (A3) $(x\vee y)\vee z=x\vee(y\vee z)$; (A4) $x\vee(y\vee y')=y\vee y'$; (A5) $x\vee(x'\vee y)'=x$; combined with the law (WOM) $x'\vee(x'\vee y')'=x\vee x'\Rightarrow y\vee(x\vee y)'=x\vee x'$ [which can be turned into an equation at the cost of size].
What I've already been doing a lot of is checking that "ortholattice + E ⊨ WOML", by generating a very long list of all ortholattices (complete up to size 20 and a good fraction of size 22), checking whether they are WOMLs, and filtering candidates against that. Now Vampire can prove (A4) and (A5) from many of the candidates and some (WOM) implications, but it can't prove (A2) or (A3) [commutativity or associativity of $\vee$] for any of them, and for some of them it can't even prove (A1) [$x'=Sx$ is an involution].
The current list of 7928 is at list2.txt if you want it, though alas it is not necessarily complete for order 15 due to some bugs in my initial brute-force. The list of 7234 resistant to naive linear models is at list3.txt.

[Matthew House]

(And for reference, small-nan-woml.txt has a list of WOMLs up to size 16, in terms of their Sheffer stroke or $\diamond$-tables.)

[Bruno Le Floch]

I think our rewriting technology, at least the one described in section 6 of the ETP paper, cannot help. All equations have the form x = … with at least one of the operations on the right-hand side being of the form y◇z with y, z distinct variables (that can bex). Thus, the weak canonizer R (see Definition 6.7 in the paper, and the application to an example after the Theorem's proof) that we get from the equation fails to be non-overlapping: there is a substitution that changes y◇z into the right-hand side of the equation.

Cohomology still has a chance to help.

[Matthew House]

Yeah, I'll see if I can't break out my SAT solver to see if any of these lattices has a suitable $+$ operation.

[Bruno Le Floch]

There are still some low-hanging fruits it seems. For instance, equation 655325894518139, x = (y ◇ ((x ◇ z) ◇ (w ◇ (w ◇ ((((w ◇ w) ◇ u) ◇ u) ◇ u))))) ◇ (x ◇ ((x ◇ x) ◇ v)), which in your prefix notation is =FFpFFqrFsFsFFFFsstttFqFFqquq, has a model of size 8

        function(*(_,_), [
               1, 0, 3, 2, 5, 4, 7, 6,
               0, 0, 0, 0, 0, 0, 0, 0,
               3, 0, 3, 0, 0, 4, 0, 6,
               2, 0, 0, 2, 2, 0, 2, 0,
               5, 0, 6, 2, 5, 0, 0, 6,
               4, 0, 4, 0, 0, 4, 4, 0,
               7, 0, 4, 2, 0, 4, 7, 0,
               6, 0, 6, 0, 6, 0, 0, 6 ])

found in 0.02s by the following Mace4 code:

assign(selection_order, 2).
assign(selection_measure, 1).
formulas(sos).
(x*x)*(x*x)=x.
x*(x*((((x*x)*y)*y)*y))=0.
y=(x*((y*z)*0))*(y*((y*y)*w)).
end_of_list.
formulas(goals).
x*y=y*x.
end_of_list.

I found this by starting with the first 5-variable equation in your list3, then finding with Prover9 that it implies (A1) so I moved on to seeking counterexamples to (A2), which is equivalent to x◇y=y◇x once we know (A1). Staring at the equation showed me that all the dependence on some of the variables was together, so it made sense to assume that w*(w*((((w*w)*v)*v)*v)) takes a single value (to make the rest of the equation as weak as possible).

Another approach to finding the same model is to require the multiplication table to have a constant row/column: Mace4 finds the model in 13 seconds with the following code,

assign(selection_order, 2).
assign(selection_measure, 3).
formulas(sos).
y=(x*((y*z)*(w*(w*((((w*w)*v1)*v1)*v1)))))*(y*((y*y)*v2)).
1*x=0.
x*1=0.
end_of_list.
formulas(goals).
x*y=y*x.
end_of_list.

[Matthew House]

(It looks like for WOMLs up to size 12, none of the operations + such that (x+y)◇(z+w)=(x◇z)+(y◇w) are associative; in general this 'linearity' condition w.r.t. ◇ is proving pretty restrictive, so I don't have much hope there.)
Good ideas with the constant row/column restrictions, I hadn't thought to turn the axioms into structural constraints to shrink the table size. Even my general model searches came up with a lot of tables that looked "nearly correct", perhaps I should experiment with the "small violations" approach.

[Bruno Le Floch]

In our Higman-Neumann exploration, whenever we had an interesting countermodel it was useful to test which equations it satisfied. This specific model eliminates more than one of your equations since it eliminates at least all specializations of the equations. Of course the model with the transposed multiplication table eliminates =FFFpFqqqFFFFFrFrFrFssssFtquq and its restrictions.

[Matthew House]

Yeah, that's been my general loop for brute-forcing: (a) generate equations that aren't filtered by current models/countermodels, (b) randomly select candidates to search for countermodels, (c) test all these countermodels to see which filters the most equations, (d) add it to the general filter and repeat.
I also incorporate some filtering into the equation generation, e.g., if an equation is not valid in the Boolean model, then I skip all of its generalizations w.r.t. variable labeling. This kind of pruning becomes very necessary by order 15, though I still haven't wrung out everything I can from it.

[Matthew House]

Linear(-like) models are nice in having very fast validity testing compared to general models, but it seems much rarer for a single linear model to filter out many equations at once.

[Bruno Le Floch]

There are actually two non-isomorphic models of the equation I mentioned above, which are non-commutative (hence not WOML) and obey x◇(x◇x)=0 and (x◇x)◇x=0 and (x◇x)◇(x◇x)=x (consequence of the equation) and x◇(0◇0)=0 and (0◇0)◇x=0. I really ought to finish an unrelated paper so I won't dig into which of your equations these models eliminate.

Two countermodels

    function(*(_,_), [
        1,0,3,2,5,4,7,6,
        0,0,0,0,0,0,0,0,
        3,0,3,0,0,4,0,6,
        2,0,0,2,2,0,2,0,
        5,0,6,2,5,0,0,6,
        4,0,4,0,0,4,4,0,
        7,0,4,2,0,4,7,0,
        6,0,6,0,6,0,0,6])]).
    function(*(_,_), [
        1,0,3,2,5,4,7,6,
        0,0,0,0,0,0,0,0,
        3,0,3,0,0,4,4,6,
        2,0,0,2,2,0,2,0,
        5,0,6,2,5,0,2,6,
        4,0,4,0,0,4,4,0,
        7,0,4,2,0,4,7,0,
        6,0,6,0,6,0,0,6])]).

[Matthew House]

Small extensions of WOMLs are proving very fruitful. I took the first 10 equations in the list and got a countermodel for all 10 of them, just by adding 2 rows/columns to a size-6 WOML. Thanks for all the advice, it's given me enough tools to keep me busy for a good while.

[Matthew House]

(In fact, "fruitful" was an understatement: every single one of the 7928 order-15 candidates is filtered out by the anti-(A3) countermodel 1,0,3,2,5,4,7,6;0,0,0,0,0,0,0,0;3,0,3,0,0,0,0,3;2,0,0,2,0,0,7,0;5,0,0,0,5,0,0,5;4,0,0,0,0,4,7,0;7,0,0,7,0,7,7,0;6,0,3,0,5,0,0,6. I guess I'll have to move on to order 16, and upgrade my pruning methods.)

[Bruno Le Floch]

When looking for the set of equations with full spectrum it was useful to first determine which shapes the equations could have (namely the restriction to all variables being equal x=y=z=...) and separately some restrictions on the rhyming schemes, and only afterwards combine them and start testing concrete models. But for very high order equations of the kind you look at, I'm curious how you can be exhaustive.

Do you have an upper bound on the order? Do you even know that the variety of WOML is 1-generated?

[Bruno Le Floch]

Maybe an intermediate question of interest could be: under the conditions (A1)–(A5), what is the shortest characterization of (WOM)?

[Matthew House]

Bruno Le Floch said:

But for very high order equations of the kind you look at, I'm curious how you can be exhaustive.

With great effort. My order-15 enumeration, testing against models/countermodels of size ≤ 8, took 34 days on 8 cores. Currently, my main pruning methods are (a) forcing the overall equation to be of form T = x for some term T and variable x, to avoid the 0000 countermodel; (b) testing that each 'shape' is valid in the Boolean model 1000/1110 when all variables are set equal; and (c) testing that each LHS variable assignment is valid in the Boolean model (for some RHS variable) before continuing to its child assignments. For each assignment with ≥ 2 variables, I define its parent assignment to be the one that sets the last variable equal to the second-to-last variable, e.g., (x◇y)◇(z◇(x◇y)) → (x◇y)◇(y◇(x◇y)) → (x◇x)◇(x◇(x◇x)), so that the children are generalizations of the parent, and they will all be invalid if the parent is invalid.
In this case, I'm pruning generalizations of equations invalid in a positive model, but if I want to get to order 16, I'll have to start pruning specializations of equations valid in countermodels.
Bruno Le Floch said:

Do you have an upper bound on the order? Do you even know that the variety of WOML is 1-generated?

Kinda? McCune et al. claim that any ortholattice variety finitely generated from "absorption equations" of form T = x has a 1-basis. Since (WOM) can be expressed in the form T = 1 (e.g., Pavičić/Megill's woml6), we should just have to take T∧x = x to get it in the form of an absorption equation. Supposedly the naive 1-basis construction is exponentially long.

[Matthew House]

Bruno Le Floch said:

Maybe an intermediate question of interest could be: under the conditions (A1)–(A5), what is the shortest characterization of (WOM)?

As an upper bound, that woml6 characterization gives an order-15 law in terms of the Sheffer stroke, x◇Sx = (x◇(x◇Sy))◇S(y◇(Sx◇y)), if I'm not mistaken.

[Bruno Le Floch]

Thanks for the details of your approach. I don't see obvious speed-ups.

Shuffling the squares around a little bit and using commutativity, there is an order-13 characterization of WOML among ortholattices, law 1429371630589266 x◇(x◇x) = ((y◇y)◇((y◇y)◇(x◇x)))◇((x◇(x◇y))◇(x◇(x◇y))). I have no idea whether it is minimal but at least it seems within reach of the kinds of techniques you used so far.

I think the exponential growth of the order is relevant when one tries to impose more than one equation, not so much here, so I would expect the order of a full characterization of WOML among magmas to be ≤25 or so.

[Bruno Le Floch]

Law 406361976666119588177911 x = (((y ◇ x) ◇ (x ◇ z)) ◇ w) ◇ (x ◇ ((x ◇ (((u ◇ (u ◇ v)) ◇ (u ◇ (u ◇ v))) ◇ ((v ◇ v) ◇ ((v ◇ v) ◇ (u ◇ u))))) ◇ z)), of order 19 and with 6 variables, characterizes the WOML Sheffer stroke among arbitrary magmas. I had to do it in three Prover9 runs, this can probably be improved.

• woml19a.p proves (A1)­–(A5) and the fact that cubes x◇(x◇x) are constant (consequence of (A1)–(A5) actually) and that this constant 1 is such that x◇1=1◇x=x' and x◇(1')=1;
• woml19b.p uses these properties to prove x = ((u * (u * v)) * (u * (u * v))) * ((v * v) * ((v * v) * (u * u))) -> (1 * w) * x' = 1., basically by setting x=y=z=1 in law 406361976666119588177911 (the new x now has nothing to do with x there);
• woml19c.p concludes very easily by restricting the previous equation to w=x to learn that such an x is equal to 1.

I have no intuition on whether this order or number of variables is optimal.

[Bruno Le Floch]

I got this law by taking the characterization of ortholattices upthread, law 40894397952 x = (((y ◇ x) ◇ (x ◇ z)) ◇ w) ◇ (x ◇ ((x ◇ ((y ◇ y) ◇ y)) ◇ z)), noticing the subexpression (y◇y)◇y which is constant in ortholattices, checking with Prover9 that ∃1, x = (((y ◇ x) ◇ (x ◇ z)) ◇ w) ◇ (x ◇ ((x ◇ 1) ◇ z)) was also a characterization of ortholattices, and then replacing 1 by the minimal-order version of the equation "woml6" you pointed to, with fresh variables. Then it was pretty much guaranteed to work: set the fresh variables to any value to get ∃1, x = (((y ◇ x) ◇ (x ◇ z)) ◇ w) ◇ (x ◇ ((x ◇ 1) ◇ z)), and set the variables x,y,z,w to suitable values (x=y=z=1, w=1' works I think) to show the "woml6" expression is equal to 1.

[Matthew House]

Whoops, I've actually been misunderstanding the 'order' this whole time, it's actually the number of ◇s instead of the number of variables. So my list of 7928 was really for order 13 by that metric. (In my own notes, I've been measuring everything by the full prefix-notation length, which for order 13 is length 29.)

[Bruno Le Floch]

Ouch, that means we're still very far being able to exhaust orders up to 18 to see order 19 is minimal.

The number of one-variable laws (shapes) of the form x=… that hold in the Boolean model 1000 appears to be [1, 0, 0, 1, 4, 8, 36, 84, 368, 1030, 4216, 12952, 51148, 167808, 648896, 2226873, 8505604, 30106840, 114283852] for successive orders 0 to 18, which means that there are 660 times more shapes to look at of order up to 18 than shapes of order up to 13.

The number of two-variable laws (useful as specializations of candidate characterizations) that hold in the Boolean model 1000 and neither in 0000 nor 0011 nor 0101 appears to be [0, 0, 0, 0, 4, 12, 152, 616, 6232, 33092, 292808, 1746268, 14429504, 93070684, 740501152, 5035427540, 39175853084, 276002982308, 2120987371896] for orders 0 to 18, so by this measure there are 22000 times more of order up to 18 than order up to 13.