Re-enable solution-blocking-constraint deletion (closes #59)

[ciaranm]

Counting/enumeration proofs log a solx blocking constraint per solution and keep it at the top proof level, so proof size is linear in the number of solutions. The optimisation to keep it linear in the search depth — move each backtrack nogood into the core (core id) so the blocking constraints it subsumes can be checked-deleted (del id) on backtrack — was added in #55 but reverted in #60: core id-ing those nogoods tripped an upstream VeriPB monotonicity bug (adding core id statements turned a verifying proof into a failing one), reported upstream and tracked in #59.

That VeriPB bug is now fixed. The saved minimal reproducer — a proof plus exactly two extra core id lines that previously failed a later rup — now verifies (s VERIFIED COMPLETE ENUMERATION OF 4 SOLUTIONS) on the installed VeriPB.

This PR re-applies the deletion. It is always on rather than gated behind a --count-solutions flag: the core id/del id of backtrack nogoods is sound in every mode (decision and unsat searches simply have few or no blocking constraints to delete), so there's no reason to make it an option. homomorphism.cc and proof.hh therefore go back to their pre-#60 state and the whole change is local to proof.cc, plus a proof-logging docs refresh.

Verification

• ctest 48/48 under both the release and sanitize (ASan+UBSan) presets — including decision, unsat, clique and MCS proofs (which now also core id/del id their backtrack nogoods), proof_count_loopy, and the proof_random_sweep that originally caught the regression.
• An extended 240-instance counting sweep (loopless + loopy, larger targets, more seeds) — every proof verifies.
• The cake_pb_iso pipeline tests pass, so core id/del id survive elaboration down to the formally-verified checker.

Spot checks: counting path4 → k4 (24 solutions) emits 40 core id, 60 del id, 24 solx → s VERIFIED COMPLETE ENUMERATION OF 24 SOLUTIONS; a backtracking decision proof emits core id/del id and verifies s VERIFIED SATISFIABLE.

Closes #59.

🤖 Generated with Claude Code