Expansion proof minimization via unsatisfiable cores

[gebner]

Conceptually, minimal expansion proofs are the first-order analogue to unsat cores in propositional logic. The current method for expansion proof minimization in GAPT (minimalExpansionSequent) uses a very simple approach that iteratively removes one weak quantifier node after another and checks whether the resulting expansion tree's deep formula is still tautological. This procedure has quadratically many calls to the SAT solver, if I'm not mistaken, and it is infeasible to run it on expansion proofs with many unnecessary instances.

There has been considerable interest in unsat cores from the SAT community, and a number of efficient and optimized algorithms have been developed that solve this problem. Many of these algorithms analyze the proof traces produced by a SAT solver. Most SMT solvers support the get-unsat-core command, and this is already usable from gapt (not yet very user-friendly though). PicoSAT can also produce unsat cores natively, Sat4j should be able to produce them as well.

We can directly use these optimized algorithms to minimize expansion proofs, with a single query to the external solver. For simplicity, assume that all nodes in the expansion tree (except for the atoms) have negative polarity. The translation is somewhat akin to a Plaisted-Greenbaum transformation of the deep formula: we introduce a new propositional atom for every subtree, and add clauses such that in the end the introduced atom implies the deep formula of the subtree. For example, for a conjunction E₁ = E₂ ∧ E₃ we would add the clauses A₁ ⊃ A₂ and A₁ ⊃ A₃ if A₁, A₂, A₃ are the introduced atoms. We also add the introduced atom for the whole tree as a clause. The resulting clause set is unsatisfiable. Given an unsat core, we get the minimized expansion tree by only keeping the nodes that are mentioned in the unsat core.

By using a MaxSAT solver, we can also find (globally) minimal unsat cores.

[gebner]

There is actually an even easier encoding by adding assumptions to the atoms in the deep formula. Assume again for simplicity that all nodes have negative polarity. We compute the deep formula as usual, except that we produce implications for the atoms:

• dp(A) = l_i ⊃ A, where l_i is a different fresh propositional atom for every atom node.

We then generate an unsat core for l₁ ∧ ‥ ∧ l_n ∧ dp(E). The minimized expansion tree is then obtained by:

1. Replacing every atom node with a weakening if the corresponding l_i does not show up in the unsat core.
2. Run cleanStructureET.