3
$\begingroup$

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.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

I'm not an all an expert on this, but here is what I hope is a relevant paper by Haim Gaifman:

Reasoning with limited resources and assigning probabilities to arithmetical statements

The paper describes how to develop a "local" logic involving a set of axioms and using modus ponens as the inference rule, from which one can assign probabilities to the event that arithmetical statements are true or false. This is very much along the lines of your stated intuition about satisfiability formulas and in fact he has an example concerning primality testing.

Improve this answer
$\endgroup$
2
  • $\begingroup$ It is a nice paper but I am not sure if it is relevant to the question. $\endgroup$
    – Kaveh
    Commented Feb 19, 2012 at 18:13
  • 2
    $\begingroup$ If one interprets "measure of progress towards a proof [of some claim]" as the assignment of "probability that a given claim is true" then it seems at least somewhat relevant. I agree it may not be straightforward to assign the probabilities to the axiom set or to delineate that set in the first place. In any case, as the whole point is to find a suitable formalization of an intuition it is hard to say what would count as a definite answer. I'm curious to hear if others have more appropriate candidates. $\endgroup$
    – R Hahn
    Commented Feb 19, 2012 at 18:45
3
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .