potassco / clingo

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

Question on efficient model counting #399

Closed RenatoGeh closed 1 year ago

RenatoGeh commented 1 year ago

Hi,

Is there an efficient way to count models? The way I am doing now is simply enumerating through all possible models, e.g.

def count(_):
  global x; x += 1

import clingo

C = clingo.Control(["0"])
C.add("base", [], "{a; b; c; d}.")
C.ground()
x = 0
C.solve(on_model = count)

but I was wondering if clingo had a smarter and more efficient way to do this, as I only need the number of models for a program, and not the actual models. I looked at the documentation and couldn't find an option to only do model counting.

Thanks

PS: Thanks for developing and maintaining clingo! :)

rkaminsk commented 1 year ago

Our solver can only count models by enumerating all of them. You can probably avoid some overhead by not passing an on_model callback and simply extract the number of enumerated models from the statistics. There is some work on more clever ways to count models. Maybe @daajoe can give some pointers because he was working on this topic.

RenatoGeh commented 1 year ago

I see. Thanks for the quick reply!

You can probably avoid some overhead by not passing an on_model callback and simply extract the number of enumerated models from the statistics.

I'm actually writing everything in C, so no callbacks. Is it wrong of me to assume that passing clingo_solve_mode_yield and doing the counting within the clingo_solve_handle_model loop should be as fast as just querying from the statistics map? Or is there a more efficient way?

rkaminsk commented 1 year ago

I'm actually writing everything in C, so no callbacks. Is it wrong of me to assume that passing clingo_solve_mode_yield and doing the counting within the clingo_solve_handle_model loop should be as fast as just querying from the statistics map? Or is there a more efficient way?

Not yielding models and just calling solve+get probably has the least overhead. Whether this is noticeable depends a bit on your logic programs. If solutions can be found very quickly without much search, then I can imagine that the overhead might be noticeable.

RenatoGeh commented 1 year ago

Great. Thanks for the info. :)

Closing my question now.