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.
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.