Usually proofs are only used for UNSAT instances, as models for SAT instances can be easily checked. Nevertheless it would be possible to upgrade proof generation and checking to be precise for the SAT case. This would help self-checking to catch errors that introduce incorrect models, would be useful for the interactive setting and might help in checking SAT instances where variables are hidden and only a restricted model is generated (see #21).
The checker would need to keep track which clauses are redundant. When a non-redundant clause is removed it needs to be convinced that the removed clause has some redundancy property with the other non-redundant clauses.
Usually proofs are only used for UNSAT instances, as models for SAT instances can be easily checked. Nevertheless it would be possible to upgrade proof generation and checking to be precise for the SAT case. This would help self-checking to catch errors that introduce incorrect models, would be useful for the interactive setting and might help in checking SAT instances where variables are hidden and only a restricted model is generated (see #21).
The checker would need to keep track which clauses are redundant. When a non-redundant clause is removed it needs to be convinced that the removed clause has some redundancy property with the other non-redundant clauses.