Parallel proofs #103
Merged
Parallel proofs #103
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
conp-solutions
force-pushed
the
parallel-proofs
branch
4 times, most recently
from
bc833f8 to
2a1c4bd
Compare
... so that more corner cases can be caught, and compared to MergeSat. Signed-off-by: Norbert Manthey <[email protected]>
... so that configuring the solver results in more meaningful runs. Signed-off-by: Norbert Manthey <[email protected]>
Signed-off-by: Norbert Manthey <[email protected]>
When disabling simplification on the CLI, we need to disable it internally before starting to parse the input formula. This change impements this difference. Signed-off-by: Norbert Manthey <[email protected]>
This object allows to lock the execution for the runtime of a function, in case locking needs to be used. This switch allows to reuse code of sequential functions also during parallel execution. Signed-off-by: Norbert Manthey <[email protected]>
When solving in parallel, we want to write proofs separately, one for each solver instance. However, we also want to write the result to a single file. Hence, we extend the proof interface to support subproofs. Subproofs can be organized in a tree, where the root note has a lock to share access to the file of the proof. The change implements the required interface extensions to support writing proofs in parallel. To reflect what is going on, also rename the flush function. Signed-off-by: Norbert Manthey <[email protected]>
... to allow testing the proof interface in the parallel environment -- but using only a single solver instance. The current code cannot handle clause sharing, not starting multiple solver instances. Different approaches for handling parallel proofs are discussed in the paper "Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers" by Marijn J. H. Heule and Norbert Manthey and Tobias Philipp, published in the Pragmatics of SAT workshop 2014. Signed-off-by: Norbert Manthey <[email protected]>
Signed-off-by: Norbert Manthey <[email protected]>
Add relevant guards to the proof object, as well as the commonly shared online proof checker. Also adapt the users of the proof interface. Signed-off-by: Norbert Manthey <[email protected]>
... and use this interface in the parallel algorithm accordingly. Signed-off-by: Norbert Manthey <[email protected]>
In case we sync from the primary, we want to also make sure we update the proof accordingly with clauses multiplied in the solver. Signed-off-by: Norbert Manthey <[email protected]>
Signed-off-by: Norbert Manthey <[email protected]>
Support proofs from the sequential solver. Furthermore, allow to check the proof on the fly. Signed-off-by: Norbert Manthey <[email protected]>
... to be able to use those flags during linking as well. Signed-off-by: Norbert Manthey <[email protected]>
Signed-off-by: Norbert Manthey <[email protected]>
... as we have implemented a conditional guard already. Signed-off-by: Norbert Manthey <[email protected]>
Match the allocation variant, and use 'free' to de-allocate the memory of the buffer. Signed-off-by: Norbert Manthey <[email protected]>
... so that the proof object works properly in the parallel setup. Signed-off-by: Norbert Manthey <[email protected]>
... as there is an issue with conditional variables when just linking with -lpthread. Signed-off-by: Norbert Manthey <[email protected]>
... so that we can check proof generation with parameterized solvers. Signed-off-by: Norbert Manthey <[email protected]>
Add checking generation of proofs from parallel solver. Signed-off-by: Norbert Manthey <[email protected]>
Signed-off-by: Norbert Manthey <[email protected]>
conp-solutions
force-pushed
the
parallel-proofs
branch
from
2a1c4bd to
847d021
Compare
Signed-off-by: Norbert Manthey <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
First stubs