[zero_k]

Author of CryptoMiniSat here :) XOR+CNF is indeed supported by CryptoMiniSat. Which is cool, but if you _really_ think about it, the resolution operator over these two are gonna give you multivariate polynomials over GF(2). So resolution is poor in CryptoMiniSat, because it only encodes one of the constraints that this polynomial implies (i.e. one that can be encoded in a single disjunctive clause). And if you wanna do the _real_ deal, i.e. "properly" solve multivariate polynomials over GF(2) then you are in for a ride -- the all-powerful, much-feared, Grobner basis algorithms, and I am not touching those with a 100m pole, because they are hell on wheels :) I mean... it's possible to contribute to them, and I know of two people who did: https://theory.stanford.edu/~barrett/fmcad/slides/5_Kaufmann... and of course, https://link.springer.com/chapter/10.1007/978-3-031-37703-7_... i.e. Daniela and Alex. It's... rough :D

Just my 2 cents.

[js8]

Thanks for the links to those people. The GF(2) simplifies Grobner bases calculations a lot, IMHO, but I don't have much experience with them either. I am just curious, because to me it now seems to be an obvious way to go. I mean, the fact that we can represent any SAT problem as an intersection of 2SAT and XORSAT problems indicates, there must be some generalization of the both polynomial algorithms. And it seems to me this generalization is somehow related to Grobner bases methods.

I have only very quickly skimmed it, but I wouldn't be surprised if the theorem D.21 in Kaufman's thesis (https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufma...) turned out to be true for all the unsatisfiability PAC proofs, not just the circuits she is looking at. (As I commented below. If you're proving contradiction, looking for element 1 in the ideal using Grobner basis, then it seems somewhat unreasonable to require degree of basis polynomials larger than 3, if you start from all polynomials with degree less or equal than 2. If you look what e.g. 2SAT algorithm is doing algebraically, it only needs degree 3 polynomials as well, although the monomial of degree 3 is immediately eliminated. So if the Grobner basis algorithm needs to build large degree polynomials, because no small degree will help you, it's likely your system is already satisfiable. Would really like to see a counterexample.)