Identifying techniques responsible for a quick UNSAT proof

[amatuag]

I have some CNFs where Kissat is much faster than say Cadical on some CNFs. I'd like to identify if techniques like BVA are playing a big role in speeding up the UNSAT proof.

Are there any verbose prints that could help me identify this ?

[m-fleury]

This is very tricky.

CaDiCaL (since 3.0) has the same techniques as kissat, but scheduled differently.

I'd like to identify if techniques like BVA are playing a big role in speeding up the UNSAT proof.

Measuring the effect of BVA is really hard. For some techniques (like vivification or sweeping) you can look at the statistics to see if they work well. Most techniques can be deactivated (e.g., --no-factor deactivates BVA).

[amatuag]

I can turn off individual techniques but I wasn't sure about the interactions between the various techniques.

I'll play around with the switches.

I do have a related question. Glucose had tried a version of extended resolution. Does BVA in Kissat sort of subsume that in anyway?

[m-fleury]

I do have a related question. Glucose had tried a version of extended resolution. Does BVA in Kissat sort of subsume that in anyway?

No, though we have a SAT 2026 paper on that topic :-). The short version is: Zachary Battleman reimplemented ER in CaDiCaL but it is too expensive on the SAT Competition (it works only on some families and you need many xors). Florian Pollitt implemented a BVA version that targets XORs, which is in the current development version of CaDiCaL.