4 ms·

I don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clau

by js8 1y ago

I don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clauses, and the linear system can resolve some common contradictions, propagate literals, etc. Also Grobner basis algorithm over polynomials in Z_2 can be used to solve SAT. A SAT problem can be encoded as a set of quadratic polynomials, and if the generated ideal is all polynomials, the system is unsatisfiable (that's Nullstellenansatz). I don't understand how we can get high degree polynomials when running Grobner basis algorithm that specifically prefers low degree polynomials. It intuitively doesn't make sense.

dooglius 1y ago
SAT is NP-complete, and both gaussian elimination and 2SAT are polynomial-time, so this would suggest either you're mistaken or there is some hidden catch here (like the size of one or the other being exponential-sized).
- js8 1y ago
  There is no catch - I even describe the reduction in another comment below. You can convert a 3SAT clause to a combination of XORSAT and 2SAT clauses. I am not mistaken, either, I used this reduction many times on practical problems, so I know it works. I encourage you to try it. Unfortunately, putting the algorithms for XORSAT and 2SAT together is not trivial at all, they are quite different (but Grobner bases over GF(2) seem very promising in that). But I agree that the fact that both XORSAT and 2SAT have polynomial algorithms is quite a strong indicator that full SAT has a one too. :-) (On the other hand, there is IMHO only very little actual evidence for P!=NP.)
sirwhinesalot 1y ago
I have no idea about most of the words you wrote but I'd love to see alternative approaches to SAT solving. CryptoMiniSAT has native support for Gaussian Elimination but it has to put a lot of effort into recovering XORs from the CNF. A different format (XORSAT + 2SAT) plus an efficient algorithm to exchange information from the two sides of the problem would be interesting.
- js8 1y ago
  One way to recover XORs from 3SAT (AFAIK unfortunately DIMACS doesn't support XOR natively) is to use the formula: (a | b | c) = ((a ^ ~x) | b) & (x | c) where x is a variable that can be chosen. The LHS is satisfiable iff RHS is satisfiable. This gives you extra variable per clause, but you can eliminate some of them using GE. (Probably not an ideal approach to easy problems, but IMHO worth trying for the hard ones.) Then you get a set of clauses that have what I call "generalized literals" - essentially a linear combination of literals - in clauses that only have 1 OR (I call this 2-XORSAT). These can be trivially transformed to intersection of XORSAT and 2SAT. Another thing that DIMACS is missing, it's not very modular. So you cannot represent a bunch of conditions using already pre-solved XORSAT portion, and apply that to a new problem. (For example, we could encode a generic multiplier in SAT, relating inputs and outputs. Then we could presolve the XORSAT portion of the multiplier. Then we want to factorize a number. Well, just add a bunch of constants specifying output that needs to be satisfied and you don't need to solve the XORSAT for the multiplier again.) Or, you can convert the 2-XORSAT into quadratic polynomials over Z_2 that all need to be equal to 0. Then you can use the Grobner basis algorithm to find whether these polynomials can be linearly combined (using polynomials as coefficients) to give 1 (i.e. they generate an ideal which contains the whole ring of polynomials), meaning the contradictory equation 1=0 has to be satisfied, and so the problem is unsatisfiable. What I would really like to understand, how it can happen, if you are running the Grobner basis algorithm and keep an eye on the degree, that you build the degree up from low degree polynomials. It seems to me, if the problem is unsatisfiable, you should be always able to get by with polynomials of low degree, because why carry extra variables if you're gonna eliminate the terms anyway? (If low degree polynomials are sufficient for the Grobner basis, it would imply P=NP by the way, because there is only polynomial number of polynomials of a given maximum degree.) But yeah CryptoMiniSAT looks somewhat promising.
  - fcholf 1y ago
    To efficiently encode XOR-constraint you will necessarily need extra variables (as you proposed) because we know that no bounded depth and polynomial size Boolean circuit can encode parity ("parity is not in AC0"). The problem with this kind of constraints is that they are not local and really disturb CDCL based SAT solvers because you cannot remove the constraint unless you have fixed all its variables. Now, cryptominisat has a specific focus on this kind of constraints and implements ad-hoc routines to exploit this routine. cryptominisat is hence focused toward applications where this kind of constraint naturally appears, be it circuit synthesis or cryptography. Now, CDCL solver is another beast. Gaussian elimination / Grobner basis are not implemented in these solvers simply because it is "too costly". One way of understanding why is just to reframe what one call SAT solver. This is not really a tool to solve SAT (hell, they can't even deal with the pigeon hole principle without preprocessing), the purpose of a SAT solver is to quickly solve instances coming from natural encoding of constraint systems. In this framework, unit propagation and clause learning are basically extremely efficient because they uncover hidden structure in the way, us human, encode constraint problems. Hence (CDCL) SAT solvers are highly efficient in many applications. But it is easy to kill one with a few variables by simply going out of this framework. For example, they are killers in solving packages dependencies because the structure of these problems matches this approach, CDCL solvers are then just an extremely refined way of bruteforcing your way through the search space. Now, if your application heavily contains XOR-constraints, then it is likely a (CDCL) SAT solver is not the right approach. For circuit synthesis, some people use BDD based approach (where parity can be efficiently encoded) but sometimes you will simply have to develop your dedicated solver or use other solvers for other NP-complete problem that will have a different area of specialization (as already observed in many comments).
emil-lp 1y ago
> I don't understand why SAT solvers don't use gaussian elimination more. These are the types of questions that can easily be answered by simply trying.
- js8 1y ago
  I agree they can be answered, but easily - no. The Grobner basis algorithm has been known for longer than NP problems, so it's not obvious why it wasn't used to solve SAT problems.
BigTTYGothGF 1y ago
> I don't understand how we can get high degree polynomials when running Grobner basis algorithm From the syzygies, surely?
- js8 1y ago
  Surely. Maybe you can give me a counterexample. Let's just consider GF(2). Give me a set of generators with polynomials of degree <=2 over n variables, such that, 1 is a member of the ideal (i.e. generators generate the whole ring of polynomials) - so if I understand this correctly, Grobner basis is just 1, and, during the construction of the Grobner basis, you need to construct a polynomial of an arbitrarily high degree (or let's say degree 7). And there is no way to avoid this (or same degree) polynomial during the basis construction by finding a lower degree polynomial first. See my problem? Somehow, I feel these syzygies need to be constructed from the degree 2 polynomials (the initial set), but then we can probably only work with the polynomials of the low degree instead, from which those syzygies are constructed. To me, this is a very interesting question. Because if we can find the Grobner basis (even for just those ideals that coincide with the whole ring) in GF(2) in a way that we only need to construct polynomials of bounded degree, then there is a polynomial algorithm for SAT. Since most people believe there isn't such algorithm, I would really like to see a counterexample to this situation.

by js8 1y ago

dooglius 1y ago

SAT is NP-complete, and both gaussian elimination and 2SAT are polynomial-time, so this would suggest either you're mistaken or there is some hidden catch here (like the size of one or the other being exponential-sized).

js8 1y ago
There is no catch - I even describe the reduction in another comment below. You can convert a 3SAT clause to a combination of XORSAT and 2SAT clauses. I am not mistaken, either, I used this reduction many times on practical problems, so I know it works. I encourage you to try it. Unfortunately, putting the algorithms for XORSAT and 2SAT together is not trivial at all, they are quite different (but Grobner bases over GF(2) seem very promising in that). But I agree that the fact that both XORSAT and 2SAT have polynomial algorithms is quite a strong indicator that full SAT has a one too. :-) (On the other hand, there is IMHO only very little actual evidence for P!=NP.)

sirwhinesalot 1y ago

I have no idea about most of the words you wrote but I'd love to see alternative approaches to SAT solving. CryptoMiniSAT has native support for Gaussian Elimination but it has to put a lot of effort into recovering XORs from the CNF. A different format (XORSAT + 2SAT) plus an efficient algorithm to exchange information from the two sides of the problem would be interesting.

js8 1y ago
One way to recover XORs from 3SAT (AFAIK unfortunately DIMACS doesn't support XOR natively) is to use the formula: (a | b | c) = ((a ^ ~x) | b) & (x | c) where x is a variable that can be chosen. The LHS is satisfiable iff RHS is satisfiable. This gives you extra variable per clause, but you can eliminate some of them using GE. (Probably not an ideal approach to easy problems, but IMHO worth trying for the hard ones.) Then you get a set of clauses that have what I call "generalized literals" - essentially a linear combination of literals - in clauses that only have 1 OR (I call this 2-XORSAT). These can be trivially transformed to intersection of XORSAT and 2SAT. Another thing that DIMACS is missing, it's not very modular. So you cannot represent a bunch of conditions using already pre-solved XORSAT portion, and apply that to a new problem. (For example, we could encode a generic multiplier in SAT, relating inputs and outputs. Then we could presolve the XORSAT portion of the multiplier. Then we want to factorize a number. Well, just add a bunch of constants specifying output that needs to be satisfied and you don't need to solve the XORSAT for the multiplier again.) Or, you can convert the 2-XORSAT into quadratic polynomials over Z_2 that all need to be equal to 0. Then you can use the Grobner basis algorithm to find whether these polynomials can be linearly combined (using polynomials as coefficients) to give 1 (i.e. they generate an ideal which contains the whole ring of polynomials), meaning the contradictory equation 1=0 has to be satisfied, and so the problem is unsatisfiable. What I would really like to understand, how it can happen, if you are running the Grobner basis algorithm and keep an eye on the degree, that you build the degree up from low degree polynomials. It seems to me, if the problem is unsatisfiable, you should be always able to get by with polynomials of low degree, because why carry extra variables if you're gonna eliminate the terms anyway? (If low degree polynomials are sufficient for the Grobner basis, it would imply P=NP by the way, because there is only polynomial number of polynomials of a given maximum degree.) But yeah CryptoMiniSAT looks somewhat promising.
- fcholf 1y ago
  To efficiently encode XOR-constraint you will necessarily need extra variables (as you proposed) because we know that no bounded depth and polynomial size Boolean circuit can encode parity ("parity is not in AC0"). The problem with this kind of constraints is that they are not local and really disturb CDCL based SAT solvers because you cannot remove the constraint unless you have fixed all its variables. Now, cryptominisat has a specific focus on this kind of constraints and implements ad-hoc routines to exploit this routine. cryptominisat is hence focused toward applications where this kind of constraint naturally appears, be it circuit synthesis or cryptography. Now, CDCL solver is another beast. Gaussian elimination / Grobner basis are not implemented in these solvers simply because it is "too costly". One way of understanding why is just to reframe what one call SAT solver. This is not really a tool to solve SAT (hell, they can't even deal with the pigeon hole principle without preprocessing), the purpose of a SAT solver is to quickly solve instances coming from natural encoding of constraint systems. In this framework, unit propagation and clause learning are basically extremely efficient because they uncover hidden structure in the way, us human, encode constraint problems. Hence (CDCL) SAT solvers are highly efficient in many applications. But it is easy to kill one with a few variables by simply going out of this framework. For example, they are killers in solving packages dependencies because the structure of these problems matches this approach, CDCL solvers are then just an extremely refined way of bruteforcing your way through the search space. Now, if your application heavily contains XOR-constraints, then it is likely a (CDCL) SAT solver is not the right approach. For circuit synthesis, some people use BDD based approach (where parity can be efficiently encoded) but sometimes you will simply have to develop your dedicated solver or use other solvers for other NP-complete problem that will have a different area of specialization (as already observed in many comments).

emil-lp 1y ago

> I don't understand why SAT solvers don't use gaussian elimination more. These are the types of questions that can easily be answered by simply trying.

js8 1y ago
I agree they can be answered, but easily - no. The Grobner basis algorithm has been known for longer than NP problems, so it's not obvious why it wasn't used to solve SAT problems.

BigTTYGothGF 1y ago

> I don't understand how we can get high degree polynomials when running Grobner basis algorithm From the syzygies, surely?

js8 1y ago
Surely. Maybe you can give me a counterexample. Let's just consider GF(2). Give me a set of generators with polynomials of degree <=2 over n variables, such that, 1 is a member of the ideal (i.e. generators generate the whole ring of polynomials) - so if I understand this correctly, Grobner basis is just 1, and, during the construction of the Grobner basis, you need to construct a polynomial of an arbitrarily high degree (or let's say degree 7). And there is no way to avoid this (or same degree) polynomial during the basis construction by finding a lower degree polynomial first. See my problem? Somehow, I feel these syzygies need to be constructed from the degree 2 polynomials (the initial set), but then we can probably only work with the polynomials of the low degree instead, from which those syzygies are constructed. To me, this is a very interesting question. Because if we can find the Grobner basis (even for just those ideals that coincide with the whole ring) in GF(2) in a way that we only need to construct polynomials of bounded degree, then there is a polynomial algorithm for SAT. Since most people believe there isn't such algorithm, I would really like to see a counterexample to this situation.