-
Notifications
You must be signed in to change notification settings - Fork 121
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Implement proofs that deletions maintain equisatisfiability? #61
Comments
Hmm, I do not think we violate that. We only drop either implied clauses (as in @kfazekas drop rule) or redundant clauses which are implied or blocked (or contain an eliminated variable etc). There were issues that we could not misuse the DRAT proofs as reconstruction stack due to optimizations in the solver. We failed to do that for RAT (see our SAT'22 paper) and therefore if this is the real goal I fear it would also not be easy to do for PB proofs either. |
We have the corresponding, slightly more general, rule in VeriPB, with a proof of validity in the full-length version of our AAAI '22 Certified Dominance paper.
And this is also implemented in the formally verified CakePB backend, so by now we are fairly confident that this is OK... ;-) I would be happy to provide more specific references if this would be helpful.
If the solver is used inside an optimization engine, then just equisatisfiability is not quite enough --- then the proof log also needs to establish that the objective function is not worsened, but this tends to follow by automatic proving (such as RUP and friends) in the proof checker in the examples we have seen so far.
Best regards,
Jakob
…________________________________
From: Armin Biere ***@***.***>
Sent: 08 July 2023 19:43:16
To: arminbiere/cadical
Cc: Jakob Nordström; Author
Subject: Re: [arminbiere/cadical] Implement proofs that deletions maintain equisatisfiability? (Issue #61)
You don't often get email from ***@***.*** Learn why this is important<https://aka.ms/LearnAboutSenderIdentification>
Hmm, I do not think we violate that. We only drop either implied clauses (as in @kfazekas<https://github.com/kfazekas> drop rule) or redundant clauses which are implied or blocked (or contain an eliminated variable etc). There were issues that we could not misuse the DRAT proofs as reconstruction stack due to optimizations in the solver. We failed to do that for RAT and therefore if this is the real goal I fear it would also not be easy to do for PB proofs either.
—
Reply to this email directly, view it on GitHub<#61 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ACICVGOX5BFVF4E4S6CKCUTXPGL3JANCNFSM6AAAAAA2CA6D3I>.
You are receiving this because you authored the thread.Message ID: ***@***.***>
|
After some longer discussion with @florianpollitt we came to the conclusion that an augmented proof format with checked deletions in order to reconstruct models through proofs would be useful for checking the result of preprocessors, as this would require indeed proving equisatisfiability. However these checked deletions are complex to implement and in our analysis would need substantial overhead during generation. We in essence would need to extract RUP proof chains consisting of irredundant clauses that imply all the deleted irredundant clauses. At least for variable elimination (with and without gates) as well as equivalent literal substitutions, this is quite challenging. We could use the CaDiCaL's internal RUP checker infrastructure to extract those though. But this is expected to at least double memory usage and probably also slow down augmented proof producing substantially on top of adding yet another mode to the proof producing code (one would need to add 'redundant' Boolean flags to the 'proof.hpp' API and trace those internally to start with). Thus doing an augmented DLRAT proof with checked deletions seems too hard, but we could support augmented DRUP proofs with checked deletions, where the VeriPB checker then will need to derive the antecedents and resolution chains. That indeed merely means adding a 'Boolean' flag 'reddunant' to 'delete_clause (uint64_t id, const vector&)' and 'add_derrived_clause (uint64_t, ...)' in 'proof.hpp' and fixing their usage. Ultimately we still think that using a separate reconstruction stack (or file) is way more efficient to obtain models (which also for optimization then can be checked to satisfy the objective function easily), way easier to implement and would work even if the solver does not trace proofs (so also supports anytime MaxSAT solving without proofs). |
On the development branch we made already quite some progress to support VeriPB including checked deletions, which is the main point except that we were not able to provide the proof chains for those checked deletions, i.e., the VeriPB checker will need to do RUP checks in this case. We plan to make this feature available soon on the master branch too in one of the upcoming releases. |
One interesting feature for proof logging --- which is supported in VeriPB, but which I don't know if it is available in LRAT --- would be to support proofs for that deletions maintain equisatisfiability, i.e., that the current constraint database is satisfiable if and only if the original input formula is satisfiable.
This might also be relevant to have for strictly internal debugging purposes.
The concept of checked deletion is discussed briefly on slide 18 in the slides http://www.jakobnordstrom.se/docs/presentations/TalkVeriPB_PoS23.pdf for the presentation of VeriPB at the Pragmatics of SAT workshop 2023.
Translated to the context of LRAT, the checked deletion rule would be the following:
The clause C can be erased from the current clause database D in the proof given that C is RAT with respect to D \ {C}.
In the VeriPB proof system, deletions that satisfy this are called "checked deletions", otherwise they are "unchecked deletions".
For a solver that only uses checked deletion, one would know that the solver maintains equisatisfiability, and if the solver is used inside an optimization engine one would also know that the values of the objective functions for all solutions reported are also guaranteed to be valid. If the only purpose of the proof logging is to certify unsatisfiability, then "unchecked deletion" can also be used given that certain specific conditions are met.
The text was updated successfully, but these errors were encountered: