Avoid unit deletions in DRAT proofs

[krobelus]

Hi,

DRAT proof checkers ignore deletions of (pseudo) unit clauses for reasons stated here.

Unsatisfiability proofs by CryptoMiniSat can contain deletions of unit clauses and as a result many of these proofs are rejected by a checker that performs unit deletions [1].
Other solvers [2] do not delete a clause if it is the reason for propagating some literal. This seems to be sufficient to make their proofs valid, independent of whether unit deletion is performed by the checker.

How difficult do you think would it be to avoid deleting those clauses?
I have tried to do that but only succeeded on some instances - others' proofs are still being rejected because of reason deletions.

Thank you,
Johannes

[1]: There are rupee and rate.
[2]: From the 2018 SAT competition, solvers CaDiCaL, Lingeling, Riss and varisat do not generate reason deletions while CryptoMiniSat and MiniSat based ones do.

[msoos]

Hi,

Thanks! I have heard about this issue before, I wonder where I'm producing the unit deletions. I tried to find these with rupee but it immediately segfaulted on the very first input I gave to it, hence I cannot trust that verifier, see:

arpj-rebola/rupee#1

I am now checking rate :)

[msoos]

Unfortunately, I cannot compile rate on an extremely fresh Arch Linux install:

krobelus/rate#1

Please advise how I could debug this issue as none of the DRAT systems you have pointed me to seem to be useable on my system :( Would it be possible for you to fix up rate so I can compile it? Thanks!

PS: Please note that I must have a way to make sure I don't reintroduce this bug and I find all instances of it. For that I need a working DRAT checker that will run in my CICD pipeline so I can find this bug any time it comes back up.

PS2: Also, please note that I do VERY much appreciate your bug report and I want to fix this, but I want to make sure it's not a one-time fix but one that lasts forever and I am very happy to replace drat-trim in my pipeline with a better DRAT checker, e.g. rate :)

[krobelus]

Hi,

Thanks! I have heard about this issue before, I wonder where I'm producing the unit deletions. I tried to find these with rupee but it immediately segfaulted on the very first input I gave to it, hence I cannot trust that verifier, see:

arpj-rebola/rupee#1

Yeah, rupee is not really maintained. This segfault shouldn't affect the result but there are some other cases that could be problematic, for example comments after the CNF header.

I am now checking rate :)

That should work fine, do let me know of any issue.

[msoos]

Hi,

Actually, building rate didn't work either, please see above. Could you please make sure it works with rust that isn't literally nightly version? To me that sounds extremely flaky and I would very much not enjoy building and installing that and I believe very few would be.

[krobelus]

Hi,

Actually, building rate didn't work either, please see above. Could you please make sure it works with rust that isn't literally nightly version? To me that sounds extremely flaky and I would very much not enjoy building and installing that and I believe very few would be.

I'm pretty sure I have fixed the issue with stable cargo not being able to handle the build.
The culprit was really just the unstable default-run feature, requiring nightly cargo.

Now running cargo build will download Rust's nightly version as of 2019-02-22 and build everything using that version. So it is not an ever-changing nightly version but rather one that I pinned at some point.
I plan to switch over to stable Rust eventually - I'm currently using some features that are waiting to be stabilized. If it is a requirement I can port it to stable now.

Now that I fixed the cargo issue, something like this can be used to install Rust and build rate (Tested on Ubuntu 16 but should definitely work on Arch too)

curl https://sh.rustup.rs -sSf > /tmp/rustup.sh
chmod +x /tmp/rustup.sh
/tmp/rustup.sh -y
rm /tmp/rustup.sh
export PATH="$HOME/.cargo/bin:$PATH"
git clone https://github.com/krobelus/rate
cd rate
cargo install --path .

Once that works you can grep for reason deletions shrinking trail. They should be 0.
The other metric reason deletions also counts when for example there are two identical unit clauses and one if them is deleted, but it does not affect the assignment.

To see which units are deleted run with one verbose flag -v, then look for revision. After each unit deletion, the revision tells you which literals were unassigned as a result. If you look for reason deletions you will also find deletions that do not discard information.

[msoos]

Hi,

I am a bit lost, maybe you could help me out :) I am trying to debug this issue, but I don't seem to be deleting any unit clauses. So there are no "d UNIT" in the DRAT file produced by cryptominisat. However, your system finds 424 units deleted in this particular DRAT file. File is attached, along with original CNF:
stuff.tar.gz Must be run as:

$ rate out dr --skip-unit-deletions
c rate version: 66a3e9cb0f952d320181de39b15d5ade2f2dc4cc
c mode: RAT
c parsing formula (s):                          0.003
c binary proof mode
c parsing proof (s):                            0.043
c preprocessing proof (s):                      0.006
c verifying proof (s):                          0.891
c premise clauses:                               8300
c proof steps:                                  42496
c skipped tautologies:                              6
c RUP introductions:                            14854
c RAT introductions:                                0
c deletions:                                    20261
c skipped deletions:                              424
c reason deletions:                               296
c reason deletions shrinking trail:                 0
c total time (s):                               0.945
c memory (MB):                                  4.593
s VERIFIED

So I am a bit lost. What do you mean by unit deletion? Am I doing something wrong and somehow there really are some "d UNIT"'-s in the "dr" file? I can't seem to find them... sorry, I am really lost, a bit of help would be nice. Thanks!

[krobelus]

There are indeed no deletions of size-one clauses, but there are deletions of clauses that are unit under the current assignment in the proof checker. This assignment is computed by performing unit propagation exhaustively after each lemma is added. Meaning that after each proof step the checker should always have the same assignment as the solver at the corresponding point in time (at decision level 0). So they should also be unit under the solver's assignment.

A reason clause is a unit clause that was propagated. We primarily care about those since the others don't directly influence the assignment.

In drat-trim clauses that are unit w.r.t. the assignment are called pseudo-unit clauses, the command
drat-trim out dr -v | grep ignoring | wc -l
should give the same number as "reason deletions" in the output of rate --skip-unit-deletions

[msoos]

Hi,

Thanks, that makes sense :) I'm looking into this. I am keeping this issue open until I get a satisfactory fix for this, and will mark the commits so you can see the updates here. Thanks again, and I will fix, I promise :)

Mate

[krobelus]

I think I have two working patches for MiniSat 2.2 demonstrating ways to fix this.

As @jix suggested, the first patch removes deletions of satisfied clauses in DRAT proofs (they are still deleted in the solver). This works because every reason clause is satisfied.

Additionally there is a second patch which removes deletions of reason clauses only.

[msoos]

Hi,

Those most likely will significantly damage CryptoMiniSat, as DRAT-Trim and all DRAT verifiers will take a lot more memory to run. Instead, I believe I should do a different setup, where unit clauses are added to the system as a separate clause before the clause leading to the unit is deleted. Then I can delete all the clauses as I do today. In other words, what you are suggesting is I believe the wrong fix and would significantly hamper verifying proofs that CMS emits. Please let me know if what I wrote made any sense. I believe it's the right approach, but I can always be wrong :)

[krobelus]

Hi,

Those most likely will significantly damage CryptoMiniSat, as DRAT-Trim and all DRAT verifiers will take a lot more memory to run. Instead, I believe I should do a different setup, where unit clauses are added to the system as a separate clause before the clause leading to the unit is deleted. Then I can delete all the clauses as I do today. In other words, what you are suggesting is I believe the wrong fix and would significantly hamper verifying proofs that CMS emits. Please let me know if what I wrote made any sense. I believe it's the right approach, but I can always be wrong :)

Well, it would not decrease the performance of current implementations of DRAT checkers for reasons described here. Current checkers keep the entire proof in memory because it is checked backwards (after preprocessing), that's why there is no garbage collection. Backwards checking is essential for only checking necessary lemmas. It would be possible for checkers to stream the proof backwards to lower the memory footprint.

Anyway, it can't hurt to add units before deleting the propagating clauses like you suggest.
It's also exactly what varisat does for its internal proof format and LRAT, and it makes the conflict analysis more efficient.

That being said, my patches were definitely not right, here is a proper fix for Minisat: krobelus/minisat@keep-locked-clauses, which avoids deletions of reason clauses.

[jix]

It might be clear from the context, but to avoid confusion, I'd like to clarify that my conflict analysis isn't more efficient compared to other solvers. Adding propagated unit clauses just avoids extra work I'd otherwise have to do during conflict analysis to generate LRAT proofs.

[msoos]

I see! Thanks for the clarification to both of you :) It's good to know that my idea wouldn't help current DRAT verifiers. However, I want to make sure that whatever I do it is the best for the future. I try not to do the same work twice. On a larger project like this, that's an important principle. I will get back to this in a few weeks. Let me know if this is a blocker for anyone, then I might schedule it earlier. In the meanwhile, I have so many things that others are asking me :( I hope that's OK. Please let me know if this is a blocker. Thanks!

[msoos]

We have now moved to FRAT, and the frat-rs verifier, here: https://github.com/digama0/frat/issues This removes the issues of deleting unit clauses from the proofs, since FRAT does not allow for that. Hence, this has been fixed, yay!

[krobelus]

On Sun, Oct 30, 2022 at 03:08:34AM -0700, Mate Soos wrote: We have now moved to FRAT, and the `frat-rs` verifier, here: https://github.com/digama0/frat/issues This removes the issues of deleting unit clauses from the proofs, since FRAT does not allow for that. Hence, this has been fixed, yay!

awesome! I've been meaning to check out FRAT for a while but I'm not really active in this area these days

…

-- Reply to this email directly or view it on GitHub: #554 (comment) You are receiving this because you authored the thread. Message ID: ***@***.***>