Proposal of standard commands related to decisions

[Tomaqa]

Motivation

Some applications of SMT solvers focus on satisfiable rather than unsatisfiable problems. However, there is no standard way of defining preference rules that would guide the decisions. Sometimes, good decision strategies are application-specific, and such guidance might greatly benefit the search for satisfying assignments.

This year, I submitted planning benchmarks that are relevant to this issue here. These benchmarks were originally solved with some guidance of the decisions, but the submitted benchmarks lack this setting. As a result, none of these benchmarks was solved during this year's SMT-COMP, while originally they were solved quite easily in most cases.

Proposal

Add the following commands to the standard:

(add-preferred-variable <var>)
(reset-preferred-variables)

(set-preferred-values <var> (<value>*))
(reset-preferred-values)

These introduce two orthogonal approaches to guide the decision heuristics:

• configuring a list of variables that the solver must consider first, following the order, before it considers any variables outside the list based on internal heuristics,
• given a variable, once the variable is already selected for a decision, configuring a list of values that the solver must consider first, following the order, before it considers any values outside the list based on internal heuristics

Such a heuristic configuration is somewhat similar to the Mathsat5 command msat_add_preferred_for_branching, but (Boolean) variables and values are not separated there.
My proposal is more general. It also allows to configure a list of values for a given variable without affecting the selection of candidates for decisions.
Also, the proposal is not restricted to Boolean variables.

Semantics

(add-preferred-variable <var>)

Appends variable <var> to the list of variables preferred for selecting a candidate for decisions.
When the SMT solver arrives at a point of a decision, it must first try the variables from the list, starting from the first position. Only if none of the variables is viable for the decision (i.e. they are already assigned to a value), the solver is allowed to select a variable on its own.
Variable <var> must be declared before issuing this command within the current context of the assertion stack. The lifetime of variable <var> within the list of preferred variables corresponds to the lifetime of the variable itself (i.e. to the preceding command declare-fun), also respecting the option :global-declarations.
Issuing the command for the second time for the same variable within the current context must result in an error (the same way as declaring a variable twice).

The command is not treated separately from the declarations wrt. the assertion stack because one would usually not want to do sth. like

(declare-const a Bool)
(declare-const b Bool)
...
(push 1)
(add-preferred-variable a)
(add-preferred-variable b)
(check-sat)
(pop 1)
(push 1)
(add-preferred-variable b)
(add-preferred-variable a)
(check-sat)

because both results must be the same, only the models may differ.
However, if one is indeed interested in retrieving such different models, we can provide an option that would allow such behavior.

Variable <var> is not restricted to Boolean variables. SMT solvers that would implement also the cases with non-Boolean variables (e.g. MCSat solvers) must ensure that the preference of these variables within decisions is obeyed as well. In the case of CDCL solvers, this might be more difficult to implement.

(reset-preferred-variables)

Clears the list of preferred variables regardless of the assertion stack.
This is also issued by (reset-assertions) and (reset).

(set-preferred-values <var> (<value>*))

Sets the list of preferred candidate values for decisions for variable <var> to (<value>*). The values must not repeat, otherwise it is an error.
When the SMT solver arrives at a point of a decision to variable <var>, it must first try the values from the list, starting from the first position. Only if none of the values is viable for the decision, the solver is allowed to select a value on its own.
The command does not affect the selection of a candidate variable for decisions.
It overwrites any previous list of preferred values for the variable. Hence, it is not possible to consecutively append multiple such values - but I do not consider such cases useful.
Issuing (set-preferred-values <var> ()) clears the preferred values for variable <var>.

Note that in the case of Boolean variables, for example (set-preferred-values a (true false)) is equivalent to (set-preferred-values a (true)).

The command is independent of the assertion stack.

(reset-preferred-values)

Clears the list of preferred values of all variables.
This is also issued by (reset).

Boolean example

(set-logic QF_C)
(set-option :produce-models true)
(declare-const a Bool)
(declare-const b Bool)
(assert (xor a b))
(add-preferred-variable a)
(add-preferred-variable b)
(set-preferred-values a (true))
(set-preferred-values b (true))
(check-sat)
(get-value (a b))

The response must be

sat
((a true) (b false))

Note that the preferred value for b was ignored because it was not the subject of a decision.
This would not be possible to achieve using e.g. check-sat-assuming.

If the order of the variables was reversed, the values would have to be ((a false) (b true)).

Arithmetic example

(set-logic QF_LIA)
(set-option :produce-models true)
(declare-const x Int)
(assert (and (>= x 0) (<= x 3)))
(set-preferred-values x (5 2))
(check-sat)
(get-value (x))

The response must be

sat
((x 2))

[fontainep]

Hi,

Clark, Cesare, and I have been discussing shortly this topic. We moved the issue into a discussion, to better reflect the current status of the topic. We also believe it would be nice to briefly discuss with a zoom meeting. Could you send a mail to Cesare, Clark, and Pascal with all the relevant people in cc so that we can proceed finding a suitable time? We generally meet on Wednesdays 17:00 CET (not the next two weeks).

Thanks and best,

Pascal