Wip #12
Open
Wip #12
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
Add flag for LCM, as well as a reverse method.
The current version compiles, but does not respect the PT changes yet. The implemented parameters should be functional. By default, LCM is not active.
When a clause is modified via LCM, tracking the PT level is difficult. As an over approximation, use the level of the current node. This way, we can at least use LCM, and still share clauses downwards correctly. For now, this is good enough, compared to not being able to share clauses at all.
Track the share indexes during LCM. This way, we do not loose sharing information when doing LCM.
Move vector initialization 2 loops out, to reduce the number of re-alloactions.
When using an index to point into the learnts vector, make sure the items in that vector are valid, or in release mode are dropped to not crash the solver. This was found when using LCM which modified the learnts vector.
The tmp dir variable has been read from $3, while $2 was the actual aim.
In the old version, the wrong variable has been used as index value, leading to out of bound errors.
If there are no candidate literals to compute a score for, stop the computation, and skip.
The split variable next has to be initialized, such that in case of failures during computing the candidates, e.g. due to too small formulas, there lit_Undef value can still be returned. Consequently, make sure nobody consumes lit_Undef as an index.
As getting stuck might be due to a race condition, allow the solver to see this condition more often before actually aborting the search. On the other hand, make sure we assert before exit, so that debugging would be doable, and the problem can be identified during fuzzing.
When multiple slaves work on the same node, make sure they do not overwrite the state of each other. Only set a state to unknown, if the node actually has an unknown state.
Currently, the stopUnsatChilds option had to be set to write the unsat state for a node. However, the state should always be written. Hence, the check for the option is moved closer to actually running the related algorithm.
In the reduceDB, new clauses are added to the clauses to be shared, but no clauses are removed. This way, faulty pointers might be used, as the clauses that are shared might become invalid, or wrong indexes are used.
When we know a level does not have clauses to share, do not lock the level, but instead skip the level right away.
We should not have unit clauses as conflicts in the first place. Learnt clauses can become units. Hence, they need to be treated accordingly, especially added on level 0.
The current implementation would allow to drop first lits of clauses that are used for splitting. Do not allow this, as this might result in unsound behavior.
While learning units is good, the extra decision level jumps might be hard to maintain. Hence, for now, do not use the units right away.
To make sure we do not stop at a higher level, set the lastLevel accordingly.
When building the debug version of the solver, the added formula is most
of the time reported as unsatisfiable, although it is satisfiable.
This is the invocation to trigger the bug on a 4 core machine:
./pcasso -verb=2 -model -child-count=7 -threads=3 \
-print-tree -verbosity=6
cnfs/bug-180394467.cnf
In case a node is solved by receiving shared clauses, make sure we store the ptlevel for failing before.
As the solver is unsound, we might want to suppress unsat answers, and turn them into unknown, to result in a sound solver for satisfiable formulas again, without fixing the bug in the first place.
Show a little more info about state evaluation in verbose mode.
We need to track causalities of dropped literals. This was not implemented in original LCM. 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.
This branch merges the currently outstanding ones, and adds a few fixes on top.
However, there is still unsound behavior. The top commit adds an example where this is triggered.