Open ghost opened 3 years ago
In Scryer Prolog, I currently also get:
?- List = [Alice, Bob, Carla, David], Alice*5-Bob*3+Carla*7-David*9 #<10, weighted_maximum([5,-3,7,-9], List, Max). false.
Definitely a wrong result.
The problem carries over to sat_count/2:
/* SWI-Prolog 8.3.20 */
?- List = [Alice, Bob, Carla, David], Alice*5-Bob*3+Carla*7-David*9 #<10, sat_count(+[1|List], Count).
List = [Alice, Bob, Carla, David],
Count = 16,
5*Alice+7*Carla#=<3*Bob+9*David+9.
?- List = [Alice, Bob, Carla, David], Alice*5-Bob*3+Carla*7-David*9 #<10, aggregate_all(count, labeling(List), Count).
List = [Alice, Bob, Carla, David],
Count = 15,
5*Alice+7*Carla#=<3*Bob+9*David+9.
Seems ok on my side:
/* Jekejeke Prolog 1.5.0 */
?- List = [Alice, Bob, Carla, David], Alice*5-Bob*3+Carla*7-David*9 #<10, sat_count(+[1|List], Count).
List = [Alice, Bob, Carla, David],
Count = 15,
9*David #> 5*Alice-3*Bob+7*Carla-10
I am not assuming that CLP(B) from SWI-Prolog uses branch and bound for weighted_maximum/2. But theoreticall CLP(B) branch and bound should work for any constraints, given as freeze/2, when/2, CLP(FD) etc..
I tried this theoretical claim. In my system I get:
But in SWI-Prolog I get:
Is this unavoidable in SWI-Prolog? Does CLP(Z) fare better?