rkaminsk
commented
2 years ago Clingo (or better clasp since this is about solving) can handle weight constraints natively. By default it translates certain simple constraints. Have a look at the following example:
{ p(1..10) }.
x :- not 2 { p(X) }.
y :- 1 { p(X) }.An at most one constraint would correspond to the one in the rule deriving x. (Note that not 2 { p(X) } is strongly equivalent to { p(X) } 1.) You can actually inspect what is happening using the tools shipping with clingo:
% clingo example.lp --pre | lpconvert --text
y :- x_11.
{p(1);p(2);p(3);p(4);p(5);p(6);p(7);p(8);p(9);p(10)}.
x_11 :- p(1).
x_11 :- p(2).
x_11 :- p(3).
x_11 :- p(4).
x_11 :- p(5).
x_11 :- p(6).
x_11 :- p(7).
x_11 :- p(8).
x_11 :- p(9).
x_11 :- p(10).
x_13 :- 2{p(1); p(2); p(3); p(4); p(5); p(6); p(7); p(8); p(9); p(10)}.
x :- not x_13.The rule deriving x_13 indicates that clasp is handling the at most one constraint natively while the rules deriving x_11 show that the at least one constraint has been translated. We also published a paper about the implementation: https://link.springer.com/chapter/10.1007%2F978-3-642-02846-5_23.
robertoasin
Hi,
We're preparing a paper on our results on a new ASP and MaxSAT encoding for MAPF, which beats current state-of-the-art solvers on dense scenarios and, for that, we need to know how clingo handles cardinality (i.e. at-most-one) constraints. Can the solver handle this kind of constraints natively or are they grounded to propositional clauses. In the later case, which encoding for cardinality constraints do you use?