Picosat SAT solver: set the propagation limit -- but what value?

Question

From the API:

/* As alternative to a decision limit you can use the number of propagations
 * as limit.  This is more linearly related to execution time. This has to
 * be called after 'picosat_init' and before 'picosat_sat'.
 */
void picosat_set_propagation_limit (PicoSAT *, unsigned long long limit);

I looked in the documentation, but could not find any details. What value should I pick? Is there any better guess than random testing? The later would possibly take days, as my execution time is up to 24h on one run.

I actually use "pycosat" the python bindings for picosat.

PS: can someone add the "picosat" tag?

my current approach is to find a value where there is a solution within an hour, and then set the propagation limit *5 then *10 then *100, *500, etc., and run all of them in parrallel. — mrsteve

mrsteve mrsteve · Accepted Answer · 2013-11-10T19:04:12

The parameter propagation_limit is the maximum size of the resulting models, for me it correlates with the disk size (1 million results in 1 MB text file).

Picosat SAT solver: set the propagation limit -- but what value?

1 Answers