plaans / aries

Toolbox for automated planning and combinatorial solving.
MIT License
43 stars 6 forks source link

Fix sharing of learned clauses #35

Closed arbimo closed 7 months ago

arbimo commented 2 years ago

The support of optional values in the solver requires to give the literal that is implied by a clause (as it not necessarily obvious to determine). This might interact badly with importing clauses from other solvers running in parallel as importing them might cause backtracking and violate the conditions in which the literal is implied.

This is probably the cause of some unstable results in the sat solver's tests. It is however difficult to reproduce as it depends on precise timings in the parallel solvers.