I came across strange performance behavior with the propagator with the option check_only=True.
In a simple problem with a domain of size 16,17, or 1000, for one variable, depending on whether an external atom declaration is present, the performance changes dramatically. The external atom is not referenced anywhere. The discrepancy does not depend on grounding.
The presence of the external atom changes slightly the ordering of the literals clasp uses internally but the magnitude of the impact surprises me (I'd have expected a *2 factor at most).
@kstrauch94 and @MaxOstrowski , any clue what could be happening?
clingo tests/investigate/slowdown.16.next.lp -q | grep Unsat
Time : 0.082s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
clingo tests/investigate/slowdown.16.yext.lp -q | grep Unsat
Time : 0.090s (Solving: 0.01s 1st Model: 0.01s Unsat: 0.00s)
clingo tests/investigate/slowdown.17.next.lp -q | grep Unsat
Time : 9.994s (Solving: 9.92s 1st Model: 9.91s Unsat: 0.00s)
clingo tests/investigate/slowdown.17.yext.lp -q | grep Unsat
Time : 47.599s (Solving: 47.52s 1st Model: 47.52s Unsat: 0.00s)
clingo tests/investigate/slowdown.1000.next.lp -q | grep Unsat
Time : 1.914s (Solving: 1.64s 1st Model: 1.04s Unsat: 0.00s)
clingo tests/investigate/slowdown.1000.next.lp -q | grep Unsat
[interrupted after 300s]
Instance:
#const int_domain_size = 16. % or 17 or 1000
#external neverUsed. % or commented out
variable_declare(x,fromFacts).
variable_domain(x,val(int,1..int_domain_size)).
variable_define(y,operation(add,(variable(x),(val(int,1),())))).
ensure(max_domain_value,operation(eq,(variable(y),(val(int,int_domain_size+1),())))).
Tested on commit afee476
I came across strange performance behavior with the propagator with the option
check_only=True.In a simple problem with a domain of size 16,17, or 1000, for one variable, depending on whether an external atom declaration is present, the performance changes dramatically. The external atom is not referenced anywhere. The discrepancy does not depend on grounding.
The presence of the external atom changes slightly the ordering of the literals clasp uses internally but the magnitude of the impact surprises me (I'd have expected a *2 factor at most).
@kstrauch94 and @MaxOstrowski , any clue what could be happening?
Instance:
Tested on commit afee476