Measure of decisions

[felixberliner1]

I know it's been a while since this was updated, but is there any way to get a counter of how many non-trivial decisions the solver makes? Or some way to measure the complexity of a particular problem beyond runtime.

[jix]

Internally, like many solvers, it uses the number of conflicts (how often the search had to backtrack) for this. It is used to schedule restarts and reduction of learned clauses. AFAICT I never exposed the number of conflicts publicly as part of the API, but there's no reason not to and I would accept a PR that adds this. What could be done without requiring any changes to varisat is to add a ProofProcessor to the solver that counts the number of AtClause steps which should mostly correspond to the number of conflicts, but I don't remember how much runtime overhead attaching a ProofProcessor adds.