search

potassco / clingo-dl

📏 Theory propagator for difference logic using clingo's theory language and C++ API.
MIT License
6 stars 1 forks source link

Free Propagation #50

Open MaxOstrowski opened 3 years ago

MaxOstrowski commented 3 years ago 
{a}.
&diff{x} >= y+10 :- a.
&diff{x} >= y+15 :- not a.
&diff{x} <= y+9.

Given this simple sample program, clingo-dl (by default) can not determine unsat without a choice. The connection that "At least one of x>=y+10 and x>=y+15" is not yet made visible to the solver I guess. At least in the case where the same literal is used (with reversed sign) for two edges going in the same direction, one constraint can be simplified. In the example above, this would mean that &diff{x} >= y+10 is always true. This can lead to stronger propagation without changing the Algorithm, just by posting different constraints.

I could not spot this behaviour in the wild (haven't check for my multishot instances) but assume a path where you can chose to take the short route or the long route. If the literal is shared (or equality is detected by clasp) this could improve performance for such examples. Of course it would be great to have a more general "at least one of ..." restriction detection in case of multiple branches or missing equality preprocessing.

rkaminsk commented 3 years ago

If x - y <= 9 is true, then both x - y >= 10 and x - y >= 15 must be false. It is a form of bounds propagation that could easily be implemented in clingo-dl. Interestingly, this form of propagation was suggested in the SAT modulo simplex paper I was reading, recently. The partial propagation of clingo-dl should give you this kind of propagation. I do not know why clasp counts a conflict but exactly two edges are propagated false..

MaxOstrowski commented 3 years ago

Thats true, but this needs extra propagation. The method I described should capture this with the already builtin check from clingo-dl, right ? Given that you have several of these choices a long a path I think not even bound propagation can handle this. In the end, clingo-dl does not know if maybe none of x>=y+10 and x>=y+15 are true, in which case this does not give unsat.

rkaminsk commented 3 years ago

I was just looking at the example. Yes, you could equivalently write it as

{a}.
&diff{x} >= y+10.
&diff{x} >= y+15 :- not a.
&diff{x} <= y+9.

This is typically the stuff we do when encoding. Remember the last paper Torsten send around? One could probably also compute some unsatisfiable cores to find sets of literals where at least one literal is true.

rkaminsk commented 3 years ago

I keep this one open because it would be a very simple to implement preprocessing technique that just requires a hash table + one pass over the edges.