# Heuristic Parameters

Several parameters control the heuristics used by the Yices SAT solver
and theory solvers. They can be set using function `yices_set_param`

.

## SAT Solver Parameters

Yices uses a CDCL SAT solver, similar to Minisat [ES2003] and Picosat [Bie2008]. The following parameters affect heuristics used by this SAT solver.

### Restart Heuristics

The following parameters control the restart strategy.

Parameter Name Type Meaning fast-restart Boolean If true, Yices will use a fast restart heuristics c-threshold Integer Number of conflict before the first restart c-factor Float Increase factor for c-threshold after every restart (must be >= 1.0) d-threshold Integer Secondary threshold used only if fast-restart is true d-factor Float Increase factor for d-threshold (must be >= 1.0)

If fast-restart is false, the following procedure is used (restart with a geometric progression):

```
c := c-threshold
while not solved
cdcl search
when number of conflicts == c
restart the search
c := c-factor * c
```

If fast-restart is true, the following procedure is used (Picosat-like restart):

```
d := d-threshold
c := c-threshold
while not solved
cdcl search
when number of conflicts == c
restart the search
c := c_factor * c
if c >= d then
c := c_threshold
d := d_factor * d
```

### Clause deletion

The CDCL SAT solver periodically deletes learned clauses that are judged useless. The deletion procedure uses the following parameter.

Parameter Name Type Meaning r-threshold Integer Initial clause-reduction threshold r-fraction Float Clause-reduction fraction (must be between 0.0 and 1.0) r-factor Float Increase factor for the reduction threshold (must be >= 1.0) clause-decay Float Clause activity decay (must be between 0.0 and 1.0)

To control clause deletion, Yices uses the same strategy as Minisat and other SAT solvers.

Each learned clause has an activity score that decays geometrically. After each conflict, the activity of all clauses not involved in this conflict is reduced by a factor equal to clause-decay (by default it’s 0.999). A smaller value accelerates the decay.

To trigger clause deletion: the solver uses a reduction-bound

Initially the bound is set as follows:

reduction-bound = max(r-threshold, r-fraction * number of clauses in initial problem)

During the search, the bound determines when clauses are deleted:

when the number of learned clauses >= reduction bound delete low-activity clauses reduction-bound := r-factor * reduction-bound

The deletion removes approximately half of the learned clauses.

### Decision heuristic

When the SAT solver makes a decision, it picks an unassigned Boolean variable of highest activity or it picks a variable randomly. Once this decision variable is picked, the solver assigns it to true or false depending on the branching mode.

Two parameters affect the choice of unassigned variable:

Parameter Name Type Meaning var-decay Float Variable activity decay factor (must be between 0 and 1.0) randomness Float Fraction of random decisions in branching (must be between 0 and 1.0)

The var-decay controls how fast variable activities go down. A smaller number makes variable activities decay faster.

The randomness parameter specifies how many random decisions are made during the search. For example, if randomness is 0.1, approximately 10% of the decision variables are picked randomly (and 90% of the decision variables are selected based on activity).

Once a decision variable *x* is selected, the branching mode
determines whether *x* is set to true or false.

Parameter Name Value Meaning branching default Default branching (as in RSAT) negative Always set xto falsepositive Always set xto truetheory Use default is xis a pure Boolean, delegate to the theory solver otherwiseth-neg Set xto false if it’s a pure Boolean, delegate to the theory solver otherwiseth-pos Set xto true if it’s a pure Boolean, delegate to the theory solver otherwise

The default branching heuristic is standard. It uses a cache to remember the last
value assigned to each Boolean variable (either true or false). When *x* is picked
as decision variable, then it is assigned the cached value (i.e., the last value
assigned to *x*). At the beginning of the search, *x* may not have had a value yet.
In this case, the decision is to set *x* to false.

Delegating to the theory solver means asking the theory solver to
evaluate the atom attached to *x* in the current model then branching
accordingly. This is supported by the egraph and by the Simplex
solver. For example, if *x* is attached to arithmetic atom (*n* ≤
*4*), then the Simplex solver examines the value of *n* in its current
variable assignment. If this value is more than 4, then *x* is set to
*false*, otherwise, *x* is set to *true*.

## Theory Lemmas

Yices includes heuristics to build theory lemmas. A theory lemma is a clause that’s true in a theory and get added to the clauses stored in the SAT solver. The heuristics attempt to discover useful theory lemmas and convert them into clauses. Three types of theory lemmas are considered.

**Generic lemmas:**Theory solvers communicate with the CDCL SAT solver by generating so-called theory explanations. By default, these theory explanations are temporary. Optionally, Yices can convert these theory explanations into clauses (thus making them permanent).**Simplex lemmas:**If the Simplex solver contains atoms (*n*≤*4*) and (*n*≤*3*) then a valid theory lemma is (*n*≤*3*) ⟹ (*n*≤*4*), which can be added as a clause to the SAT solver. Such a lemma is generated when assertions are processed if option*eager-arith-lemma*is active. See`yices_context_enable_option`

.**Ackermann lemmas:**If the egraph contains terms*(F x y)*and*(F x z)*then we can add the following lemma*y*=*z*⟹*(F x y)*=*(F x z)*This is a known as Ackermann’s lemma for the terms

*(F x y)*and*(F x z)*.Yices uses a variant of this lemmas for predicates. If the egraph contains

*(P x)*and*(P y)*where P is an uninterpreted predicate (i.e.,*(P x)*and*(P y)*are Boolean), then the corresponding Ackermann lemma is written as two clauses:*x*=*y*∧*(P x)*⟹*(P y)**x*=*y*∧*(P y)*⟹*(P x)*Generating Ackermann lemmas may require creating new equality atoms. For example, in the clause

*y*=*z*⟹*(F x y)*=*(F x z)*,Yices may have to create two new atoms: the atom (

*y*=*z*) and the atom (*(F x y)*=*(F x z)*). Too many of these can overwhelm the egraph so Yices provides parameters to control the number of new equality atoms generated by Ackermann lemmas.

The following parameters control generic lemma and Ackermann lemma generation.

Parameter Name Type Meaning cache-tclauses Boolean Enables the generation of generic lemmas tclause-size Integer Bound on the size of generic lemmas dyn-ack Boolean Enables the generation of Ackermann lemmas for non-Boolean terms max-ack Integer Bound on the number of Ackermann lemmas generated (for non-Boolean terms) dyn-ack-threshold Integer Heuristic threshold: A lower value causes more lemmas to be generated dyn-bool-ack Boolean Enables the generation of Ackermann lemmas for Boolean terms max-bool-ack Integer Bound on the number of Boolean Ackermann lemmas generated dyn-bool-ack-threshold Integer Heuristic threshold: as above. Lower values make lemma generation more aggressive aux-eq-quota Integer Limit on the number of equalities created for Ackermann lemmas aux-eq-ratio Float Another factor to limit the number of equalities created

If cache-tclauses is true, then only small theory explanations (that contains no more than tclause-size literals) are converted to clauses.

To bound the number of new equality atoms created by the Ackermann and Boolean Ackermann heuristics, Yices uses the two parameters aux-eq-quota and aux-eq-ratio. The limit on the number of new equality atoms is set to

```
max(aux-eq-quota, num-terms * aux-eq-ratio)
```

where num-terms is the the total number of terms initially present in the egraph. When this limit is reached, Ackermann lemmas will not be added if they require creating new equality atoms.

## Simplex Parameters

The Simplex-based solver uses the following parameters.

Parameter Name Type Meaning simplex-prop Boolean Enables theory propagation in the Simplex solver prop-threshold Integer Bound on the number of variables in rows of the simplex tableau: if a row contains more than this number of variables, it’s not considered during theory propagation. simplex-adjust Boolean Uses a heuristic to adjust the simplex model bland-threhsold Integer Number of pivoting steps before activation of Bland’s pivoting rule icheck Boolean Enables periodic checking for integer feasibility If this flag is false, checking for integer feasibility is done only at the end of the search. icheck-period Integer If icheck is true, this parameter specifies how often the integer-feasibility check is called.

## Array-solver Parameters

The array solver uses the following parameters.

Parameter Name Type Meaning max-update-conflicts Integer Bound on the number of ‘update axioms’ instantiated per call to the array solver’s final check max-extensionality Integer Bound on the number of extensionality axioms instantiated per call to the arrays solver’s final check.

## Model Reconciliation Parameters

Final check is called when the search completes. In this state,
all Boolean atoms are assigned a value and all solvers have a
local model that assigns values to variables managed by each
solver. A model-reconciliation procedure is then called to check
whether these local models are compatible: if two variables
*x* and *y* are shared between the egraph and a theory solver, then
both the egraph and the solver must agree on whether *x* and *y* are
equal.

If they are not, then Yices instantiate an interface lemma for *x* and
*y*, to force agreement. Semantically, such a lemmas encodes the rule

*x = y*in the theory solver implies

*x = y*in the egraph.

For example, if *x* and *y* are shared between the egraph and the Simplex solver,
then the interface lemma for *x* and *y* is

*x*=

*y*) ∨ (

*x*<

*y*) ∨ (

*y*<

*x*)

where (*x* = *y*) is an equality atom in the egraph and (*x* < *y*) and
(*y* < *x*) are arithmetic atoms in the Simplex solver.

Optionally, before generating any interface lemma, Yices can attempt
to modify the egraph to locally solve the conflicts. This procedure is
explained in [Dut2014]. We call it the *optimistic*
model-reconciliation procedure.

Model reconciliation is controlled by two parameters.

Parameter Name Type Meaning optimistic-final-check Boolean Enable the optimistic model-reconciliation procedure max-interface-eqs Integer Bound on the number of interface lemmas in each call to final check

## Parameters Used by the Exists/Forall Solver

Yices includes a solver for exists/forall problems, that is, problems of the form

_{1}… x

_{n}∀ y

_{1}… y

_{m}P(x

_{1}… x

_{n}, y

_{1}… y

_{m})

The algorithm used by Yices is explained in [Dut2015]. It repeatedly
attempts to guess values for the existential variables x_{1} …
x_{n}, then checks whether these guesses are correct, by searching for
a counterexample in the variables y_{1} … y_{m}.

The following parameters control this algorithm.

Parameter Name Type Meaning ef-max-iters Integer Maximal number of iterations (this is a bound on the number of guesses before Yices gives up) ef-gen-mode Enum Selects the model-based generalization method (see below). ef-max-samples Integer Limit on the number of samples used in the exists/forall solver’s initializatio ef-flatten-iff Boolean Preprocessing option ef-flatten-ite Boolean Preprocessing option

The generalization mode can take one of the following values:

- none: no generalization is used
- substitution: generalization by substitution
- projection: model-based projection
- auto: automatic. This is either generalization by substitution or model-based projection depending on the type of the universal variables.

The default setting is ‘auto’. In this mode, Yices uses model-based projection if the problems has arithmetic variables (i.e., integer or real-valued). Otherwise, it uses generalization by substitution. See [Dut2015] and the references therein for more details on model generalization.

Parameter ef-max-samples is used in the algorithm’s initialization. In
this phase, Yices heuristically learns initial constraints on the existential
variables *x*. This is done by sampling values of the universal
variables *y*. The parameter is a bound on the number of these
samples.

The parameters ef-flatten-iff and ef-flatten-ite enable or disable flattening of if-and-only-if and if-then-else terms, respectively.

Flattening *(<=> p q)* rewrites the term to *(and (=> p q) (=> q p))*

Flattening *(ite c p q)* rewrites the term to *(and (=> c p) (=> (not c) q)*