3 ms·

> we tried a few alternatives to Wilkies and didn't find smaller countermodels. I wish you spent at least a couple words in the paper about that. Even negative

> we tried a few alternatives to Wilkies and didn't find smaller countermodels. I wish you spent at least a couple words in the paper about that. Even negative results are worth documenting! (even if you didn't get up to size 11, I'd've loved to hear about those other alternatives) --- by the way, you mentioned that decreasing HSI6/10 from O(n^6) to O(n^5) clauses was slower - how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much? --- also, have you tried reordering order of operations in symmetry break? how much did it affect the search? I wonder if unique multiplication table might've been of help had it been disambiguated stronger (or weaker)

bsubs 2mo ago
> I wish you spent at least a couple words in the paper about that. That makes sense; it just happened that we tried the other identities after having written and submitted the paper. More importantly, the variants of Wilkie's identity we tried were suggested to us by an expert on the topic; I have just sent an email asking if they are okay with us sharing them, and if so I will post a link here. > how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much? It was roughly a factor of 8 fewer clauses, and yet over 5 times slower. If you're interested in the design of compact CNF encodings, and their effects on runtime, that's exactly the topic of my PhD thesis, and this proposal might give an initial idea: https://bsubercaseaux.github.io/assets/pdf/proposal.pdf https://bsubercaseaux.github.io/assets/pdf/proposal.pdf Naturally, there could be another encoding that has fewer clauses (say, O(n^5) or even O(n^4)) and does perform better in practice. But we didn't come up with one. > also, have you tried reordering order of operations in symmetry break? how much did it affect the search? To some extent. It was of moderate impact in terms of the runtime, but presumably the enumeration up to isomorphism would have been harder if we didn't consider the addition variables first. To have some updated numbers, I just ran some experiments with the 3! = 6 permutations of {A, M, E} on n=10. AME (used in the paper) -> 92.7s AEM -> 110.8s MAE -> 139.4s MEA -> 157.4s EAM -> 297.1s EMA -> 276.8s

bsubs 2mo ago

> I wish you spent at least a couple words in the paper about that. That makes sense; it just happened that we tried the other identities after having written and submitted the paper. More importantly, the variants of Wilkie's identity we tried were suggested to us by an expert on the topic; I have just sent an email asking if they are okay with us sharing them, and if so I will post a link here. > how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much? It was roughly a factor of 8 fewer clauses, and yet over 5 times slower. If you're interested in the design of compact CNF encodings, and their effects on runtime, that's exactly the topic of my PhD thesis, and this proposal might give an initial idea: https://bsubercaseaux.github.io/assets/pdf/proposal.pdf https://bsubercaseaux.github.io/assets/pdf/proposal.pdf Naturally, there could be another encoding that has fewer clauses (say, O(n^5) or even O(n^4)) and does perform better in practice. But we didn't come up with one. > also, have you tried reordering order of operations in symmetry break? how much did it affect the search? To some extent. It was of moderate impact in terms of the runtime, but presumably the enumeration up to isomorphism would have been harder if we didn't consider the addition variables first. To have some updated numbers, I just ran some experiments with the 3! = 6 permutations of {A, M, E} on n=10. AME (used in the paper) -> 92.7s AEM -> 110.8s MAE -> 139.4s MEA -> 157.4s EAM -> 297.1s EMA -> 276.8s