search

meelgroup / approxmc

Approximate Model Counter
Other
70 stars 26 forks source link

pyapproxmc: setting the memory/time limit #35

Closed izzayacine closed 1 year ago

izzayacine commented 1 year ago

Can we fix the memory and time limit of the Counter using the python interface?

msoos commented 1 year ago

Hi,

Currently, unfortunately, this is not supported. Would this be useful for your use-case? Is there a particular use-case you are looking for?

Thanks,

Mate

izzayacine commented 1 year ago

My program instruments a linear number of call to approxmc (on the same cnf formula + assumptions, so different sub-formulas) and I want to fix a time/memory limit for each call, as some calls consume too much resources. Therefore, in case of an expensive call, the procedure should skip it.

Yacine

msoos commented 1 year ago

Hi,

Let's talk about this once I'm back in Singapore, in about a week. It's just a lot of work and I'm not 10% sure it's needed. Let's discuss in-person and then we can see if it's indeed needed.

Cheers,

Mate

izzayacine commented 1 year ago

The issue is that when I run approxmc with python interface it stops the process (killed -9) however the binary file (c++ compiled) returns a results

msoos commented 1 year ago

Hi,

Oh, that's a bug actually. Can you please send me how to reproduce?

Thanks,

Mate

On Wed, 3 May 2023 at 18:50, Yacine Izza @.***> wrote:

The issue is that when I run approxmc with python interface it stops the process (killed -9) however the binary file (c++ compiled) returns a results

— Reply to this email directly, view it on GitHub https://github.com/meelgroup/approxmc/issues/35#issuecomment-1533973481, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKF4OO2TJVA4B2KHPYXQS3XEMDN3ANCNFSM6AAAAAAXTYWAQM . You are receiving this because you commented.Message ID: @.***>

izzayacine commented 1 year ago

Okay, I sent you an email.

Yacine

msoos commented 1 year ago

The solution is to use the projection parameter to count() in the python module. This is equivalent to the c ind parameter in the CNF. Without a projection set, ApproxMC counts significantly slower.

I am now closing this issue, since it's not a bug in ApproxMC.

Mate

izzayacine commented 1 year ago

I use the param projection when calling the function count() and I get an error. Have you tried to replicate with the formula that I've sent? and do you get an error killed -9 or it returns the solution?

izzayacine commented 1 year ago

I think that this occurs only when I call several times approxmc, and then the memory gets stuck. I try to delete the instance of Counter class but it doesn't solve the problem.