Configuration Interface: Settings for individual problem variables

[fkutzner]

Current state
Currently, the configuration interface takes key/value pairs with values of type void *. As of https://github.com/ipasir2/interface/blob/71c6b421fec064614aaeb2e7ae27123a5eaf4f76/ipasir.h, the value pointer can point to buffers of enum, int, float or char values. The length of the buffer is fixed and determined by the solver (via length in ipasir_option_type), where a length of 0 means an array of length equal to the number of variables in the formula.

The use case for length=0 is setting values per variable, e.g. initial weights. However, the current solution has a few pitfalls:

• The number of variables actually occurring in a problem can be lesser than the maximum variable of the problem. This makes it pretty cumbersome to compute the index of a given variable.
• An alternative would be to specify that the array must have N elements where N is the maximum variable occurring in the formula. However, this would make it hard to deal with the API without resorting to low-level functions like calloc (which typically supports lazy allocation of memory pages by the OS), since some problem instances use very large variable numbers.
• The solver has no way of determining which values have been changed, so it needs to update all variables. This, again, requires clients to make a copy of the current setting first, then pass a modified version back to the solver. This could become problematic if a client needs to update variable state before each call to ipasir_solve().
• The solver is only aware of variables which have already been used with ipasir_add. This requires clients to keep track of which variables have already been used with ipasir_add (in the original wording) or to add a trivially satisfied clause containing the maximum variable of the problem.

Use Cases

• Modifying heuristic weights for individual variables
• Preventing the solver from eliminating certain variables

(Rough) Proposal

Instead of supporting length=0, a dedicated function for per-variable options could be used, like void ipasir_set_option_for_var(void* S, char const* name, int var, void const* value). length = 0 should then be prohibited in ipasir_option_type.

Alternative Proposal

We could add an additional parameter size_t index to ipasir_set_option. length = 0 would then mean that arbitrary values for indices can be used. The semantics of the index are defined by the option. Then, the pointer to the value passed to ipasir_set_option could always point to a single value

[Udopia]

This is a wording error. The proposal assumes variable ids are compact, but this can easily be changed. A large number of variables should be not more of a problem to the interface than to the solver itself. The issue of non-compact variable ids is just an encoding issue and not so much our problem. It is not true that the solver has no way of determining which values have changed. This is exactly the purpose of the setter. Other ways of changing a value shall be prohibited. The only bigger issue that I see with dynamic (maxvar-bound) array-size is the missing getter.

[fkutzner]

Discussion notes:

• we decided to drop initial support for arrays, but keep the option for adding support for arrays later, if use cases are known
• support for the char type is dropped as well (see Support for setting proof filenames #16)
• two kinds of settings are offered initially: "global" settings affecting the whole solver object, and per-variable settings. Clients can set values for variables that haven't been used in the problem instance yet.