potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
599 stars 79 forks source link

Search space difference between solving and multi-shot solving. #433

Closed Mohamed0293 closed 1 year ago

Mohamed0293 commented 1 year ago

Hi, I am new to the area of ASP. I would like to know whether multi-shot solving will affect the overall search space, more than the classical one.

Also, does the search space of the following program relies only on the choice rules?

a:-b. {b}.

If I am not mistaken, the search space is 2. as constant 'a' does not play a role in affecting the overall number of models.

Also, if considering adding '{b}' in a sub-program and 'a:-b.' in another one, would this affect the overall search space?

Thanks in advance.

Best regards, Mohamed

rkaminsk commented 1 year ago

It is hard to quantify the size of the search space. A CDCL-based solver like clingo is influenced by many factors.

Your simple program does not have any constraints. There will be no conflicts during search; just decisions. The solver's preporcessor should reduce this to a problem with just one variable, which can be made either true or false (a is equivalent to b). In multi-shot solving, it can happen that there are more variables because fewer simplifications, for example during the mentioned preprocessing, are applied. So search can be negatively affected.