Enable pcasso #136
Open
Enable pcasso #136
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
... to speedup the build, and avoid unnecessary rebuilds. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
We want to build different MergeSat-based Dockerfiles. Hence, this change introduce configurability. This way, multiple docker images can be build from the same Dockerfile. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Basic type to maintain a partition tree. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Implement helper methods to be able to work with the partition tree. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Support starting partitioning after some syncs. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Implement the first stubs to support partitioning the search space next. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Add a separate method to handle UNSAT cases when a solver returns from solving a partition. Note: the actual relevant code is not added yet, this change only moves the exception into a better place for future iteration. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
... so that controlling their allocation is properly jailed. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
... based on the position of each node on the path to the root among its siblings. The signature can be used to print traces during debugging, or to print the actual partition tree. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
This method allows to load the assumptions for a solver when it is asked to solver a partition of the search space. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Furthermore, wrap assigning a node to a thread in a separate method to have a single location to control this change. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
This change adds the work in progress state for solving formulas in parallel, while maintaining and assigning partitions to threads. Note: there is no option to enable or disable this functionality yet. Furthermore, the solver might be very verbose at this point. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Note: this commit should not be required in case all other commits get formatting applied. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
... so that we do not have any left-overs later on. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
... because otherwise there should not be a global conflict. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
When a partition is solved, the solver enters sync with l_False. However, we want to be able to assign this status back to l_Undef, as we might assign a new partition to the solver. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
The initial code did not iterate in the tree. Furthermore, the status of the solver, as well as the conflict of the involved solver need to be reset once we collect an unsatisfiable node. Note: this change could also be merged in the previous commit of this function. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
When a solver finds a conflict, we need to process it immediately. Otherwise, the l_False status would be propagated back to search, which then will terminate with UNSAT; leading to a wrong locking order and a deadlock. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
... instead of waiting for 1000 syncs by default. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
... as partitioning then uses assumptions, and the involved variables might have been eliminated by the time. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
When we find UNSAT during sync, e.g. by receiving clauses, make sure this status is propagated to the thread status as well, as this is used to then terminate search with the proper status as well. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Enable solver to use partitioning by default. This is mainly required to be able to partitipact in the parallel track of the SAT compeition. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
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.
No description provided.