jix
Measure of decisions
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.
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.
