We implement basic support for computing unsat cores using our proof
producing capabilities.
We can obtain unsat core by logging resolution proof; the
compact version with resolution chains as logged by CDCL is sufficient.
We can then walk the resolution chains from root to the leaves, and
collect all the original clauses that participate in the proof. These
form unsat core at the clause level.
To lift the unsat core to the level of SMT-LIB assertion, we leverage
the fact that we propagate partitioning information from top-level
assertions to clauses.
We can, therefore collect the partition information from clausal unsat
core and then just take corresponding top-level assertions.
Tomaqa
commented
6 months ago
We implement basic support for computing unsat cores using our proof producing capabilities. We can obtain unsat core by logging resolution proof; the compact version with resolution chains as logged by CDCL is sufficient. We can then walk the resolution chains from root to the leaves, and collect all the original clauses that participate in the proof. These form unsat core at the clause level. To lift the unsat core to the level of SMT-LIB assertion, we leverage the fact that we propagate partitioning information from top-level assertions to clauses. We can, therefore collect the partition information from clausal unsat core and then just take corresponding top-level assertions.