6 Alternative derivations and certificate complexity
On this page · Permalink · Source line 479
When a claim admits several certified justifications, certificate extraction is no longer a backward closure problem. A local choice may be reused by several later obligations, which couples decisions across the field.
Problem 6.1: Minimum Certificate Decision
Given a finite acyclic certified proof field, a target set, nonnegative integer node and justification costs, and a budget \(B\), determine whether a certificate of total cost at most \(B\) exists.
Theorem 6.2: Minimum certificate selection is NP-complete
Minimum Certificate Decision is NP-complete, even when every nonzero cost is a unit node cost and all justification costs are zero.
Proof
The problem belongs to NP. A proposed node and justification set can be checked in polynomial time by verifying references, computing derivability in topological order, and summing costs.
For NP-hardness, reduce Set Cover. Let \(U=\{u_1,\ldots,u_m\}\) be the universe, let \(S_1,\ldots,S_n\subseteq U\) be the available sets, and let \(k\) be the cover budget. Construct one optional admissible leaf node \(s_i\) for each set \(S_i\), with unit cost. Construct one zero-cost obligation node \(e_j\) for each element \(u_j\). Whenever \(u_j\in S_i\), add a certified justification
Add a zero-cost target node \(t\) with the certified justification
The dependency graph is acyclic. A certificate for \(t\) must derive every \(e_j\). Deriving \(e_j\) requires at least one selected source node \(s_i\) with \(u_j\in S_i\). One selected \(s_i\) may discharge several obligations, and its cost is paid once. Therefore a certificate of cost at most \(k\) exists exactly when the original Set Cover instance has a cover of size at most \(k\). The reduction is polynomial.
Remark 6.3: Algorithmic consequence
Exhaustive certificate selection is useful for small fields or fields with few alternatives. The reference implementation uses branch and bound with an explicit search-state limit. Its result is optimal for the stored finite cost data when the search completes. It does not remove the exponential worst case. The decision theorem concerns integer costs, while the Python interface accepts finite floating-point costs and compares their exact stored binary values as rationals. Printed cost totals remain floating-point summaries. The input conversion does not recover an intended real or decimal value that was never represented. See [5] for the background complexity language.