I was quite hopeful when I first saw the XNF solver 2-Xornado, and then Xorricane, which solve so-called XOR-OR-AND (XNF) problems, i.e. problems written in the format “(a XOR b XOR c) or (f XOR NOT g)”. The two papers about this family of solvers were [PDF1][PDF2], and the results looked impressive. They could outdo CryptoMiniSat, my CNF-XOR solver, on a bunch of instance families. To be honest, I suspected a cutoff being fired, but I was also hopeful and didn’t want to be the annoying person in the way of new research. Then the Xorcle paper dropped [PDF] and my collaborator asked me to take a look. This led me down a rabbit hole of figuring out that in fact, all these years, XNF solvers have been comparing against CryptoMiniSat in a somewhat unflattering way.
CryptoMiniSat has to function as a regular SAT solver as well as perform XOR reasoning, while the XNF solvers only really work well for XNF inputs, and are not so competitive on CNF inputs. In order to balance the requirement of needing to also work on plain CNF input, CryptoMiniSat has a number of cutoffs. For example, it didn’t use more than 3-5 matrices at most by default, and the number of rows and columns in matrices was also limited. However, the instances that the XNF authors were using sometimes had extremely large matrices, and/or very many of them (e.g. over 1000 matrices). Furthermore, some of them contained blasted XOR constraints that are quite long, and would normally be cut up — so CryptoMiniSat’s default recovery limit didn’t check for them. This meant that CryptoMiniSat was often not running XOR reasoning (Gauss-Jordan Elimination, GJE) on many of these instances. Essentially, the defaults made it easy to run benchmarks incorrectly with CryptoMiniSat.
Performance of CryptoMiniSat vs XNF Solvers
I had a go at checking the performance of CryptoMiniSat once these limits were lifted. Unfortunately, it turns out that CryptoMiniSat had a few annoying performance bugs. Firstly, each propagation of GJE ran an algorithm linear in the number of matrices, which didn’t quite work with over 500 matrices. Oops. Secondly, there was a silly limit in the maximum discoverable XOR size, which had to be lifted. Finally, I never thought there’d be more than 1000 matrices, so 1000 was a reserved number, and caused an assertion failure. These had to be fixed.
Once fixed, running CryptoMiniSat with “--autodisablegauss 0 --presimp 1 --maxmatrixrows 100000 --maxmatrixcols 100000 --maxnummatrices 1000000 --minmatrixrows 1 --maxxorsize 12” to lift all the minimum/maximum limits, led to it outperforming all the XNF solvers by a healthy margin. The results are available here. Main graph:
As you can see, CryptoMiniSat (“cms”) with those minor performance changes (changes only needed for “lifted pebbling” and “tseitin” families) and the correct options solves many more instances than the XNF solvers. Moreover, as per the report, it solves almost every family as fast or faster than these solvers, individually, as well.
Then I thought maybe I should spend some time with an AI to fix up CryptoMiniSat, and take ideas from CaDiCaL in the process. So I pointed the AI to CaDiCaL by Armin Biere et al. (a paper on one of its best techniques is here) and let it find all the things that I missed over the past 5-6 years. The result is the “cms-improved” line in the graph above. It took two evenings with AI, and now it’s quite performant, outperforming both Xorcle and Xorricane on every benchmark family except “lifted pebbling” where both Xorcle is about 2 seconds faster. The new version of CryptoMiniSat has a better “too slow GJE” detection, so all limits have been lifted by default. So in the future, it should be easier to correctly run such benchmarks with CryptoMiniSat. While this version of CMS is of course better than the old version, it was not really tuned for these benchmarks. I need CMS to perform relatively well on all the things I use it for, and that’s mostly ApproxMC solving and Ganak preprocessing.
Bugs and Fuzzing
I was curious whether these tools were outputting correct solutions. So I took the 20 minutes to ask an AI to write an XNF fuzzer (should be about 2-3h by hand) and test the tools. Unfortunately, the tools seem not to have been tested with a fuzzer. Both had a wrong-answer bug on edge-case inputs, and both had crashes and inconsistencies. Xorricane seems to be faring worse: Xorcle had 4 bugs [here] and Xorricane had 9 [here].
CryptoMiniSat is fuzzed extensively, and has been for a long while. Also it emits a proof for GJE reasoning thanks to the work of Jiong Yang, Yong Kiam Tan et al. [paper]. Actually, I asked an AI to fix up the proof generation, and now it emits a pure XLRUP proof, without needing any refinement via frat-rs (by Mario Carneiro [paper]), which was previously required.
XNF Solving Report
The full XNF solving report is available here, the code, logs, data etc. to generate it are all available here, and the fuzzer is part of that codebase, here. It only took about a weekend to put this together, using AI. I think it’s a rather interesting set of benchmarks, gathered by the authors of Xorcle and Xorricane. All the benchmarks are of course directly sourced via git submodules, so I give credit where credit is due. I also ran Bosphorus [code][paper], our ANF solver, on the relevant problems just for fun. I keep maintaining it as well, and with the new CryptoMiniSat it was performing quite well.
The Future of Research
I have to admit that I feel disappointed by this line of XNF research. I was hoping that something really interesting would come out of it. But seeing that the tools don’t seem to have been fuzz-tested, and overall they are not well-performing on the benchmark sets used by the papers, I am somewhat less optimistic. I still hope that someone will do something really-really cool with CNF-XOR, though. I think it’s more possible than ever before, now that we have AI. In fact, I pointed the AI at the Gauss-Jordan Elimination in CryptoMiniSat, and it found a really cool way of making it several times faster, depending on the matrix size. Thanks to this, ApproxMC, our approximate model counter, is almost twice as fast as before.
However, the question is — what’s the point of research if we can just ask the AI to do a lot of things for us? Tools that are correct? Tools that people want to use and re-use for years, maybe even decades to come? CryptoMiniSat was originally published in 2009, nearly two decades ago. Will today’s CNF-XOR/XNF solvers still be around in 20 years? Would it be rightfully called research or just engineering at that point? Would it be the right use of research time? None of these questions have easy or clear answers. Maybe it’s a waste of time for researchers to write and maintain tools — maybe their job is to come up with cool ideas, and let the industry implement them well/bug-free. Sometimes, it’s best to do fire-and-forget: write the paper, and not deal with it any more, instead let others pick it up and run with it. I personally keep maintaining CryptoMiniSat nearly 2 decades later, along with Arjun, Ganak, Bosphorus, and pepin —
but of course, I never really made it in research, either.