bsubs
Joined 4 years ago
Karma
129
Submissions
20
Member since
Apr 3
CS PhD student at CMU. All info about me can be found at https://bsubercaseaux.github.io/
View on Hacker NewsRecent submissions
Comment · 5 days ago
SAT-solving expert here. No immediate applications (the results in the paper are "galactic"). The main question is whether some ideas here will snowball into other ideas, one of which could eventually be very practical.
Comment · 2 months 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
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
Comment · 2 months ago
Indeed, having a different "exotic identity" that has smaller countermodels would be awesome. Unfortunately, we tried a few alternatives to Wilkies and didn't find smaller countermodels.
Note that it's not obvious at all how to search the space of possible exotic identities, so a potential direction for future work would be to have a loop in which LLMs (perhaps through something like AlphaEvolve) propose an exotic identity, and then a SAT call tries to find a small countermodel. A big issue though, is that even with our efficient encoding the SAT calls would take at least a few minutes, so we wouldn't be able to afford testing millions of candidates. But if there were 1000 candidates that could potentially be tested...
(I'm one of the authors of the paper, thanks for the coment!).
Comment · 2 months ago
Hi! One of the authors here. Whether checking the LLM-generated Lean statements/definitions is easy or not depends heavily on the area of mathematics and the concrete definitions at play. In this case it was remarkably easy. As you can see in the repository, the definition of a countermodel is easy to parse, and the statement corresponding to their nonexistence for n <= 11 is also very easy to check. If you have any questions regarding them, I would be happy to answer them.
Personally, this is one of the cases with LLM-generated Lean that I feel most comfortable with: the proofs are all mathematically simple, and we included an example of correctness for one of the SAT constraints in the paper to show that there is nothing complicated about them. Writing them all in Lean, however, would be a very tedious task for which I see no particular benefit (i.e., it's not like some other formalization projects in which one learns something by formalizing; for an example of a human-written Lean correctness proof of a SAT encoding, you can check the paper https://arxiv.org/abs/2403.17370 in which I participated).
Regarding the byte-for-byte equality, the point is that we first had the Python code (which we wrote manually), and then asked LLMs to implement an encoder in Lean that would not only produce "equivalent" formulas but exactly equal formulas, meaning that it would use the same variable indices and the same clauses in the same order. It is well-known that such superficial factors (e.g., clause or variable ordering) can actually have large effects on solver performance (see https://www.cs.utexas.edu/~marijn/publications/pos18.pdf). The Python code is not part of the trust chain, and the Lean code does not rely on it in any way. We included the Python code in the repository since it's much shorter and easier to read.
Comment · 2 months ago
I'm one of the authors of the arXiv paper. Thanks for bringing this to our attention! We were fully unaware of this repository, and it unfortunately did not come up during our literature search. Our approaches to the lower bound are pretty similar, although some technical differences make ours more efficient. For example, to show that there is no counterexample of size 10, we generate a formula with ~50k variables and ~2.7M clauses, which takes about 85 seconds to solve with Kissat. The encoder from this repository generates a formula with ~2k variables and ~33M clauses, which takes about 50 minutes to solve. We have sent an email to the authors of the Zenodo artifact to decide how to proceed!
Comment · 2 years ago
If you’d be interested in being mentored in a research project send me an email; [email protected]
Comment · 3 years ago
I see what you’re saying, but note that as mentioned above I did edit the post based on your feedback to be precise, stating that the conjecture we disproved was that regardless of the center color the chessboard of 1s could be assumed wlog in any finite diamond . (Also this is stated correctly in the paper, which at the end is the “source of truth”)
I agree with you that just saying “D_r can be colored with k colors iff it can be done with a chessboard pattern of 1s” is a slightly different statement to which our counterexample is not a counterexample, but I think you got trapped into my initial omission in the blog post, which was a writing mistake rather a mathematical mistake. I don’t think there’s anything wrong here, but sorry for the original version of this post being sloppy in the writing.
I agree again with what you were saying some messages ago about how versions of the conjecture that do not consider the center color can be more mathematically interesting. A proof that D_r can be colored with k colors iff it can be done with the chessboard pattern would definitely be super nice.
Comment · 3 years ago
Assume you know that 13 colors aren't enough and you want to prove that 14 aren't enough either. Any 14 packing-coloring of the grid must use color 6 somewhere, as otherwise it would be only using 13 colors that are no better than colors {1, ..., 13}, and thus not enough. Now, you can imagine the diamond you're considering is centered around one of these 6s. This is breaking a different kind of symmetry; a translational one, as it's breaking the original symmetry of centering your diamond on any possible color, by choosing an arbitrary one. Granted, this is different form of symmetry-breaking as it's not about auto-morphisms on the set of solution. Also, it's totally possible that "symmetry breaking" was a bad choice of words; as long as you agree that it's a helpful idea as it significantly reduces the search space, we are on the same page.
formalizing this might be tricky, I mean something like a bijection from (the set of mappings from an infinite packing-coloring to a fixed colored sub-graph) to itself.
Comment · 3 years ago
I agree, and it would be amazing for someone to find a deeper intuitive reason for why 15 is the answer to this problem, or 8 is the answer to that other problem, or many such cases.
This is however extremely hard in my opinion (note that I say "opinion" on purpose, because I don't have any way to formalize this idea). Let me use a couple more examples: any Rubik's cube (3x3x3) can be solved in at most 20 moves (on the standard metric, counting double turns as one move), and a Sudoku needs at least 17 clues to have a unique solution. Why 20? Why 17? We (humanity) got to both answers through computation, and even though the computation requires mathematical observations to be made more efficient, at the end we still checked an in-human number of cases... So in all honesty, if I had to bet, I'd say we will probably never intuitively know why 20 moves or why 17 clues, or in my case, why 15 colors... I'd love to be proven wrong tho!
Comment · 3 years ago
I think I see what you mean, but it seems to me that you're mixing ideas about the chessboard conjecture in this particular context, with more general versions of the conjecture (a bunch of which we don't know the answer for, and might be interesting in their own right).
In particular, to show that the packing-chromatic number of the infinite grid is 15, we needed to find a finite subgraph of the infinite square grid for which 14 colors are not enough. The class of sub-graphs that seemed more amenable to do this was that of diamonds (i.e., disks in the corresponding metric) of radius r. If you simply try to determine whether D_{14} can be packing-colored with 14 colors, that instance is too hard, so we make it easier by forcing a color in the center (this is a form of symmetry breaking). Forcing the center to take color 1 is the worst possible choice (see Fig 6. of the paper https://arxiv.org/pdf/2301.09757v1.pdf), therefore we want to force it to something other than 1, let's say 6 (this seems to be the best choice in practice). Your problem then reduces to determine whether D_{14} can be packing-colored with 14 colors, when forcing a 6 in the center. It turns out again that this is not easy enough to solve naively, so it would be really nice it we could assume without loss of generality that we can enforce the chessboard pattern as well as the 6 in the center (which given that the center has even coordinates, it would imply that the 1s are at odd coordinates). I try to prove this manually and failed. But we ran the experiment assuming the conjecture to be true, and effectively there is no packing-coloring for D_{14} with 14 colors, a 6 in the center, and 1s in every odd coordinate. If Conjecture 2 had been true, then we would have ended our work there, but then we realize we couldn't assume Conjecture 2: we found a way of packing-coloring D_{14} with a 6 in the center when removing the chessboard assumption.
So the formalization in our context that made the most sense was: "is it true that given any radius r, any value of k, and any value of c, the forced center color, we can assume the chessboard pattern?" (Noting that if the center is forced to 1 as you mention in your comment, then the chessboard pattern would be 1s on the even coordinates).
This is what I meant with Conjecture 2, so hopefully now it's clear why it was of interest for this particular problem. It's not obvious at all that Conjecture 2 is false provided this! unless you have a new argument I'm unaware of!
Your last question is of course interesting, and many variations of the conjecture make sense and could be studied; we didn't really pose Conjecture 2 thinking it was the most interesting formulation, but rather a sufficiently simple one that would have justified our result of (D_{14}+6 in the center + 1s at odd coordinates)-is-not-packing-colorable-with-14-colors to imply the final result.
Comment · 3 years ago
Let me be a bit more precise here (at risk of being pedantic) to make sure we're on the same page. (Also, if you have a concrete idea of how to reformulate the text so this is clearer, I'm definitely interested!)
Here are two well-defined conjectures:
Conjecture 1. A packing-coloring of the infinite square grid exists using colors {1, ..., k} if, and only if, there exists one with a chessboard pattern (meaning that wlog all vertices (a, b) such that a+b is odd get color 1).
Conjecture 2. Let $D_{r, k, c}$ be the instance consisting of whether $D_r$ can be packing-colored with $k$ colors assuming it gets color $c$ in the center. Then enforcing that all vertices (a, b) such a+b is odd get color 1 does not change the satisfiability of the instance.
Conjecture 1 is true, based on our paper: if k <= 14, then no packing-coloring exists anyway, so the conjecture is vacuously true. If k >= 15, then we know of a packing-coloring that respects the chessboard pattern (the one in Figure 12), and so the conjecture holds.
Conjecture 2 is false, this is where the smallest counterexample in the post kicks in.
Note that given that 13 colors are not enough, we knew that if there was a solution with 14 colors, it must use color 6 somewhere, and by restricting ourselves to $D_{14}$ around such a vertex, we run into the issue!
About your last comment, we use diamond graphs to prove lower bounds (i.e., that a certain number of colors is not enough), while finite square grids are used to prove upper bounds (as in Figure 12).
About aperiodic colorings, see the other comment in this thread were we discuss about it a bit :)
Comment · 3 years ago
Thanks jxf! I just fixed some, although it's likely that some typos remain.
I agree with you about Coq, although there are some very smart folks working on it. My concern is that most of the improvements I've heard of are not about usability directly (i.e., how fun and readable it is to work with). I also don't quite now of precise low-hanging fruits that would improve it in this direction, but hopefully theorem provers will get friendlier and easier to use as time advances. Also the library of lemmas other people have proved and one can just plug in is steadily growing, so that should also reduce the pain of proving new stuff...
Comment · 3 years ago
Thanks to you for the feedback!! :) reading some positive comments here has definitely paid off the investment of time in writing the post and taking care of the figures (by far the most time-consuming part haha).
Comment · 3 years ago
This is a question I've spent significant time on! (under a more technical formalization, of course) I've proved that this is not possible in infinite 1-dimensional graphs (like the infinite path, or an infinite grid of size C x Infinity, for a finite number C).
For graphs that are infinite in two dimensions I don't have an answer yet (and it's likely that I never will). I'm very fond of this question tho, so if you give me your email (you can contact me at [email protected]), I can promise to write you back if at some future point in time I have a solution to this, or if someone else shares one with me :)
Comment · 3 years ago
Even though you're right in general, this is not the case here! We have proved that no smaller counter-example exists (again by using a computer search through optimized SAT-solving).
As for the question of why no smaller counter-examples, I'm afraid I don't have any nice answers and perhaps there simply isn't a nice answer. Let me explain what I mean. My advisor Marijn Heule finished the resolution of Keller's conjecture (a conjecture about how N-dimensional cubes work in the Euclidean N-dimensional space), and the final answer is that the conjecture fails for the first time in dimension 8. "Why 8?" Again it's the same situation: it seems that that's just the way math is, something in the way the definitions and the objects behave makes it so that is the smallest counterexample. "Why" is a hard question to answer...