User dpll - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-20T01:05:34Z http://mathoverflow.net/feeds/user/21498 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/88807/measure-of-progress-towards-a-proof Measure of progress towards a proof DPLL 2012-02-18T05:04:35Z 2012-02-19T22:29:29Z <p>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.</p> <p>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.</p> <p>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.</p> <p>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)</p> <p>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.</p> <p>A relevant link might be <a href="https://rjlipton.wordpress.com/2009/02/12/bait-and-switch-why-lower-bounds-are-so-hard/" rel="nofollow">this</a> 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.</p>