XOR clauses

[mocenigo]

I am impressed by the performance of kissat and I was wondering whether it is possible to add a "native" support for XOR clauses, the way cryptominiSAT does, to kissat. This would be a great help in cryptography.

[arminbiere]

This was partially in Lingeling but already for CaDiCaL we decided not to have any specific XOR reasoning (like Gaussian elimination on GF2) and kept that decision in Kissat. We would need some substantial effort to support proofs for that (actually easier for Kissat since we will probably never have LRAT with it). So I keep this as enhancement.