search

pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
381 stars 69 forks source link

`ITotalizer` does not accept an `IDPool #173

Open Jaxan opened 1 month ago

Jaxan commented 1 month ago

Hi all,

Previously I used the CardEnc class to encode size constraints. I need multiple constraints and so I used a single IDPool and passed it along all of the CardEnc instances. Then I wanted to make the size constraints incremental, and switched to ITotalizer. But this class does not take an IDPool, only a top_id.

Currently, my workaround is as follows:

vpool = IDPool()
...
with ITotalizer(lits, ubound=upper_bound, top_id=vpool.top) as cnf_optim:
  vpool.occupy(vpool.top + 1, cnf_optim.top_id)
  vpool.top = cnf_optim.top_id
  ...

Is this a correct workaround?

And would it be possible to add a vpool variable to the ITotalizer class, just like the CardEnc class? I find it much easier (and less error-prone) to use than passing around a top variable.

Thanks for the pysat package! It is really a wonderful interface to work with!

alexeyignatiev commented 1 month ago

Hi @Jaxan,

Yes, at first glance this workaround looks okay although it might be simpler to give the range from 1 to cnf_optim.top_id when declaring it as occupied. (The method should take care of the fact that the new range is a superset of the previous.)

As for adding a vpool argument to ITotalizer, this would make perfect sense to me. So I will definitely do it at some point when and if I get a chance. Thanks for the suggestion!

Best, Alexey

Jaxan commented 3 weeks ago

Hi Alexey,

thanks for confirming my workaround!

kind regards, Joshua