# Measure of progress towards a proof

Can one define some measure of progress towards a proof of a statement? I'm not sure if it's even possible for general first order logic statements so let's restrict ourselves to propositional statements. Assume for simplicity that we know if the statement in question is true or false beforehand.

Then if one is using the DPLL system for proving a propositional statement false (or true after taking the negation of the statement and trying to prove the unsatisfiability of that), then one can easily define a measure of progress towards the proof - if the statement has $n$ variables and we encounter failure after branching on $k$ variables, then we have made $2^{-k}$ fraction progress towards a proof of unsatisfiability.

If one works with the resolution proof system, then I can't think of a polynomial-time computable measure. For an exponential-time measure, one could examine all clauses derived so far and calculate what fraction of the search space they prune.

For more general proof systems which allow introducing new variables however (like the Extended Frege system, for instance), I can't think of any measure. (Edit: except in a very limited sense in which we explore the space of all possible proofs and then decide whether a particular step counted as progress towards a proof of unsat)

So my question is whether there exist better measures of progress towards a proof of unsatisfiability (or tautology) of a propositional formula than the ones above.

A relevant link might be this which talks about defining a measure of progress in terms of computing a function in terms of proving lower bounds. If we take the function to output 0 if the input formula is unsat and 1 if it is not, then it could be relevant to the measure in question above.

-

Vacuously it sounds unlikely that there is such a measure (i.e. that's polynomial time and tells you that you've made better than $2^{-O(n)}$ progress). Otherwise you could follow a hill-climbing strategy and solve SAT in sub-exponential time. I'd expect that the same thought occurred to you, i.e. that I'm not interpreting your question deeply enough. It might help if you went into a bit more detail about what sorts of measures you'd consider acceptable, that wouldn't let you solve SAT sub-exponentially.

-