Unclear how to extract all models in cautious enumeration

[olegzaikin]

Hi. I need to find all models (satisfying assignments) of a CNF, so I run clasp with --models=0. When --enum-mode=bt or --enum-mode=record are set, then all models are found as needed - and all variables are assigned there. When --enum-mode=cautious is set, then the runtime is much lower, but in this case in the models not all variables are assigned. If I understand correctly, the cautious reasoning is applied here, so those partial models are intersections of all stable models found so far. However, I need all full models - i.e. all variables' values in all of them. Is it possible to force clasp to print all found models like it is done, in a non-cautions mode?

[BenKaufmann]

Hi @olegzaikin

If I understand correctly, the cautious reasoning is applied here, so those partial models are intersections of all stable models found so far. However, I need all full models - i.e. all variables' values in all of them. Is it possible to force clasp to print all found models like it is done, in a non-cautions mode?

No, that's not possible since brave- and cautious reasoning modes don't compute all models in the first place. They construct the consequences incrementally by strengthening a constraint representing the intersection (or union) of computed answer sets on the fly (see brief description here).

If you really need all answer sets, you have to use the regular enumeration mode.

[olegzaikin]

@BenKaufmann , thank you for a fast and detailed reply! Now I understand how it works. May I suggest adding the corresponding clarification regarding the cautious mode to the clasp documentation?

[BenKaufmann]

May I suggest adding the corresponding clarification regarding the cautious mode to the clasp documentation?

Sure. Let me transfer this issue to our guide's repo as a reminder that we should extend the corresponding section on the next update.