[YICES-HELP] Doubts regarding functions related to max-sat in
bruno at csl.sri.com
Mon Apr 11 10:37:24 PDT 2011
sarvesh prabhu wrote:
> Hi all,
> yices C API has two functions yices_set_max_num_iterations_in_maxsat(unsigned n) and yices_set_max_num_conflicts_in_maxsat_iteration(unsigned n).
> I have following doubts regarding these functions.
> 1> What do these functions mean?
> 2> What is the effect of using these 2 functions in terms of the model generated and the time needed to get a model?
> 3> In what scenarios should these functions be used?
> 4> What are the default values?
> I would really appreciate any help in understanding this.
These functions set two parameters that are used by the max-sat
algorithm in Yices. There's usually no reason to play with
them unless you encounter issues with (max-sat).
Here is how this works.
For every weighted assertion (assert+ P_i W_i), yices introduces
an auxiliary boolean variable x_i and asserts the formula (or x_i P_i).
Then (max-sat) searches for a Boolean assignment that
maximizes Sum (W_i * (not x_i)).
Yices solves this by repeatedly trying to solve the constraints
(or x_i P_i)
+ any hard constraints
+ Sum (W_i * (not x_i)) >= K
for different values of K.
This is done in two phases. In phase 1, Yices starts
with a large K (i.e, K = W_1 + ... + W_k), then
searches for a solution using a fast/incomplete search.
If that fails, K is decreased and Yices repeats this
until it finds a solution for some value K_0.
In phase 2, Yices tries to improve K_0 by iteratively
solving instances of the problem with increasing values
of K, until it gets unsat.
Parameter 'max_num_iterations_in_maxsat' is the maximal number
of iterations in Phase 2 of this algorithm. If the bound
is reached then Yices will return unknown and print its current
best idea of K. By default, this bound is 10000. If you
reduce it, then (max-sat) should be faster but give suboptimal
Parameter 'max_num_conflicts_in_maxsat_iteration' is a bound
to stop the search also in Phase 2 of the algorithm. When
Yices searches for a solution for a specific K, then it will
give up if does not find a solution after 20 * max_num_conflicts.
By default the parameter is also 10000. As before, it you
reduce it, then (max-sat) should be faster but suboptimal. If
you increase it it will be slower but most likely to find an
More information about the YICES-HELP