[Patch] Do not delete reason clauses

[Johannes Altmanninger]

Hi,

In a SAT solver or proof checker, a reason clause denotes a clause that is
the reason for unit-propagating some literal that is in the current assignment.

DRAT proof checkers ignore deletions of reason clauses for reasons stated in
[1]. Find details about the implications of this in [6].

Unsatisfiability proofs by MiniSat can contain deletions of reason clauses and,
as a result, many of these proofs are rejected by a checker that performs
unit deletions, like [2] or [3]. Out of the solvers submitted to the 2018
SAT competition's main track, only the ones based on MiniSat or CryptoMiniSat
seem to generate reason deletions.

Here's a patch for MiniSat 2.2 to avoid deleting reason clauses [4].
Other MiniSat-based solvers can be modified in a similar fashion. To
demonstrate this I have another patch for last year's competition winner
MapleLCMDistChronoBT [5].

Maybe someone can scrutinize the first patch.
There are already some other places in the source where reason clauses
are explicitly prevented from being deleted, so it looks fine to me to do
this also in the last remaining place where reason clauses may be deleted.

With the patch, the generated proofs should have no more reason deletions
that influence the correctness under either checker[7].
If DRAT checkers can assume that a proof does not contain reason deletions,
this can resolve the ambiguity because no more deletions need to be ignored,
or, in the case of a checker that includes code to handle reason deletions,
that code can be discarded, greatly simplifying the checker.

Given that, I think it would make sense to make this change to solvers, mostly
to make it obvious as to how the proof should be checked.

Let me know what you think,
Johannes

[1]: https://github.com/marijnheule/drat-trim#clause-deletion-details
[2]: https://github.com/arpj-rebola/rupee
[3]: https://github.com/krobelus/rate/
[4]: https://github.com/krobelus/minisat/commit/keep-locked-clauses
[5]: https://github.com/krobelus/MapleLCMDistChronoBT/commit/keep-locked-clauses
[6]: https://easychair.org/publications/preprint_open/7WJp
[7]:
Note that there may still be reason deletions, visible for example in drat-trim's warnings:
`drat-trim formula.cnf proof.drat -v | grep ignoring`
however, those should be benign, being the result of a difference in the
order of propagation between the solver and drat-trim.

[Mate Soos]

Hey,

I have lots of points on this, but let's just say that "Proofs should be efficiently checkable with significantly simpler programs than SAT solvers", from the paper, is although correct, in practice is not the case unfortunately. This is relatively easy to confirm by trying to read the most used DRAT checker's code base.

As for unit deletions, the patch I have seen for MiniSat-based solvers was potentially increasing the memory usage of an efficient DRAT-Trim checker, which apparently hasn't been written yet. There is a rather long winded discussion about this on a CryptoMiniSat issue, here: https://github.com/msoos/cryptominisat/issues/554 (hah, at 554 now, nice!)

Just my two cents,

Mate

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/4e7c912f-0b00-438b-b53a-afe570269402%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Norbert Manthey]

Hi all,

in the CMS issues [1] you already discuss an alternative solution that I also would implement: adding a unit clause to the proof before deleting the reason in the proof and in the solver.

Could you provide this kind of patches instead, which first check whether the we write a proof, then check for locked, and only then emit the extra unit into the proof? I would accept such a patch. Unfortunately, most recent solvers do not come with a public repository to actually do that (and I hope that changes sooner than later).

Best,
Norbert

[1] https://github.com/msoos/cryptominisat/issues/554

PS: if you have an "add unit to proof" patch for MapleLCMDistChronoBT, I happily pick that up!

To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/CAF-zLQLQeHSE1LZCHkJtKxh6M-Fo%2Ba%3DXTuPy%2BYjDxYA2-wmLHA%40mail.gmail.com.

[Johannes Altmanninger]

On Fri, Jun 14, 2019 at 09:22:56PM +0200, Norbert Manthey wrote:
> Hi all,
>
> in the CMS issues [1] you already discuss an alternative solution that I
> also would implement: adding a unit clause to the proof before deleting
> the reason in the proof and in the solver.

Right, I agree that this is better.
While it does not make a difference in current checker's performance,
it might in future. And it feels cleaner to explicitly add the unit.

>
> Could you provide this kind of patches instead, which first check
> whether the we write a proof, then check for locked, and only then emit
> the extra unit into the proof? I would accept such a patch.

I modified both patches accordingly:

https://github.com/krobelus/minisat/commit/add-unit-before-deleting-locked-clause.patch
https://github.com/krobelus/MapleLCMDistChronoBT/commit/add-unit-before-deleting-locked-clause.patch

Obviously lacking a proper commit message, but they should work.

> Unfortunately, most recent solvers do not come with a public repository
> to actually do that (and I hope that changes sooner than later).

Yeah that would help a lot.

>
> Best,
> Norbert
>
> [1] https://github.com/msoos/cryptominisat/issues/554
>
> PS: if you have an "add unit to proof" patch for MapleLCMDistChronoBT, I
> happily pick that up!
>

On 13.06.19 13:22, Mate Soos wrote:
> > Hey,
> >
> > I have lots of points on this, but let's just say that "Proofs should
> > be efficiently checkable with significantly simpler programs than SAT
> > solvers", from the paper, is although correct, in practice is not the
> > case unfortunately. This is relatively easy to confirm by trying to
> > read the most used DRAT checker's code base.

gratgen has by far the most readable source, and they essentially do
the same thing.

> >
> > As for unit deletions, the patch I have seen for MiniSat-based solvers
> > was potentially increasing the memory usage of an efficient DRAT-Trim
> > checker, which apparently hasn't been written yet.

Yeah, current checkers are heavily optimised for speed, at the expense
of a huge memory footprint.

> > <mailto:minisat%2Bunsu...@googlegroups.com>.

> > To view this discussion on the web visit
> > https://groups.google.com/d/msgid/minisat/4e7c912f-0b00-438b-b53a-afe570269402%40googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
> >
> > --
> >
> > ---
> > You received this message because you are subscribed to the Google
> > Groups "MiniSat" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> > an email to minisat+u...@googlegroups.com

> > <mailto:minisat+u...@googlegroups.com>.

> > To view this discussion on the web visit

> > https://groups.google.com/d/msgid/minisat/CAF-zLQLQeHSE1LZCHkJtKxh6M-Fo%2Ba%3DXTuPy%2BYjDxYA2-wmLHA%40mail.gmail.com
> > <https://groups.google.com/d/msgid/minisat/CAF-zLQLQeHSE1LZCHkJtKxh6M-Fo%2Ba%3DXTuPy%2BYjDxYA2-wmLHA%40mail.gmail.com?utm_medium=email&utm_source=footer>.