Restricting the variables for branching

[jcoelho72]

Hi,

I am using cadical for solving a problem after converted to SAT. The preliminary results are very good.

In the conversion I need to create many variables, but the solution is depending only on a subset of the variables.

I would like to restrict the decision variables to a list of the first K variables, to verify if helps the solver. The auxilar variables may not generte as many implications like the first variables.

Exist a simple way to do that, in some advanced parameter?

If not, can you provide some orientation on the source code needed to change, for adding the option and how to limit the decision variables.

Thanks.

Best regards,
José Coelho

[m-fleury]

There is no option to do that, because it is in general not useful, dangerous (SAT becomes meaningless), and unclear how to do in presence of inprocessing (See #39 (comment)).

That being said, you /could/ before starting solving, add something like (untried!):

for (int v = 0; v < min(K,max_vars); ++v) {
   bump_queue (v);
  bump_variable_score(v);
}

before starting the main CDCL loop to bump the clauses that you believe are important (without running into completeness issues because you only bump the variables at the beginning instead of removing them from the queues like you are suggesting).

[arminbiere]

See #39

[jcoelho72]

Thanks for for the support.

I checked #39, and is the same issue. I can present a simpler case: scheduling problem to SAT. In Horbach2010, they convert RCPSP to SAT by creating two types of variables in SAT. The start variables (that are 1 if activity j start at time t), and the process variables (that are 1 if activity j is executing at time t). For extracting the solution, is enough the start variables, but for codify the resource restrictions in SAT is required the process variables.

The idea would be just to allow branching in the variables that are enough to get a solution, in this case, the start variables. With all the solution variables with a fixed value, the SAT instance should be SAT or UNSAT. If all solution variables have a value and does not exist a conflict, then return SAT. But, for make sure, the solver could continue to find a solution for the rest of auxiliar variables, to get a guaranty that is possible the rest of the variables. In case of my codifications, the conflicts originate always from solution variables, so no branching is needed once we have all variables in the solution set, since unit propagation will guaranty all conflicts will be active if all solution variables are set.

Of course, arbitrary just branch on the K first variables, makes no sense. But in this case, for each instance, by construction, we know that is enough to set a value for the first K variables to have a solution that can be validated by unit propagation (no need to branch). This is the base for only want to allow branching on solution variables.

Also, branching in a start time of an activity, makes more sense then in processing variable.

I am trying the m-fleury suggestion, that partial solves this and would work even if setting all solution variables, we cannot verify the solution only by unit propagation. At least it can be used to verify if has an impact or not, in my instances. Bump all solution variables before start. If I understand, the bump is to put the variable first in the queue and in the scores. An head start for these variables, may be enough to observe a positive effect. I am running now, to see if the effect is significative, in the configuration that have more extra variables.

Changed only in the file cadical.cpp:

` solver->options ();

//// jcoelho bump test: code from mfleury
for (int v = 1; v <= initial_bump && v <= max_var; ++v) {
solver->internal->bump_queue (v);
solver->internal->bump_variable_score(v);
}
`
Add also a parameter, so I can pass the correct initial_bump for each specific instance.

In case it has a significative effect, if I bump multiple times, would lead to some difference? Since bump only once, may get the variables to be used first, but after a while may get behind other variables that are not solution variables.

Best regards,
José Coelho

References:

• Horbach, A. (2010). A Boolean satisfiability approach to the resource-constrained project scheduling problem. Annals of Operations Research, 181(1), 89–107. https://doi.org/10.1007/s10479-010-0693-2

[arminbiere]

So you only want to prefer them once at the beginning (before a conflict is reached). This would be simpler to achieve, the other more general version in #39 to always prefer is much harder to implement. BTW, there a hints for value/phase assignment.

[jcoelho72]

Where can I read about phase assignment?

I already see in the code about phases, but not read any definition, and not a way to use in the cadical. Maybe is what I need. Can I define a set of phases, and put in each phase a set of variables? The solver try to set first the variables of the current phase, before passing to the next phase? This would be ideal. Could be used with just two phases (the solution variables and the rest), or try other phases to orient the search.

The test that I done yesterday, resulted in little change. In 13K instances (from different sets), with 3 configurations, improved in the best configuration, but only 6 more instances solved (under 1 minute). In one configuration became worst not solving 1 instance more. The solving time slight better, but does not justify.

I would like to check the phases.

I also go check a stronger change (probably will not work, since you say that is complicated, and this is a quite simple change, in a single function):

void Internal::bump_variable (int lit) {
if (use_scores ()) bump_variable_score (lit);
else bump_queue (lit);
}

Is just a matter of making a conditional here, to only bump variables equal or less than K. If the variables greater than K are not bump, will not be selected to branch. If something will be wrong in the SAT solver, I will know since I verify the solutions returned, so I go give it a try.

Otherwise, if fails, it means that the cadical is very well optimized, and do not need this type of help, that is interesting to know.

Regards,
José Coelho

[m-fleury]

I also go check a stronger change (probably will not work, since you say that is complicated, and this is a quite simple change, in a single function):

Not that will work, but it is complicated to get the solver correct with such restrictions, especially in combinations of inprocessing techniques.

Here is an example:
A -> B
A -> BvC
~A -> B v C
you restrict your solver to decide A. Your solver will very soon find the mode ABC.

But if your solver first eliminates A, you get BvC as formula, but your solver is not allowed to branch on anything (this crashes CaDiCaL I think, because there is the assumption that if there is a non-set variable, the decision queue is not empty).

This is why I am saying it is complicated: it might work, but it is very hard to predict if it will be in combination with inprocessing (especially variable elimination).

[m-fleury]

In case it has a significative effect, if I bump multiple times, would lead to some difference? Since bump only once, may get the variables to be used first, but after a while may get behind other variables that are not solution variables.

For solver->internal->bump_variable_score(v); bumping multiple time will make a difference. For the other (focused) phase it will not. Remark that it will mostly change the run at the beginning: the solver will bump variables based on its heuristics.

I already see in the code about phases, but not read any definition, and not a way to use in the cadical.

See this issue #56. You want to use the phase function from

cadical/src/external.hpp

Line 303 in 84b4439

void phase (int elit);

. For the general definition of phases, the paper to look is probably https://cca.informatik.uni-freiburg.de/papers/CaiZhangFleuryBiere-JAIR22.pdf.

[jcoelho72]

Thanks for the paper and the support given. I understand now the phase.

Bumpping only variables that are enough to define the solution, do not worked in my instances. Could not observe a significative difference, at least, but is good that I made the test, to convice myself. I want to left the changes made in cadical, for someone that may want to test the same in other instances. I think the changes do not make incorrect results, since the variables are not removed from any queue, are only not bumped, following the m-fleury first suggestion. At least, tried several times, and in one case with a bug where no variables are bumped, and I do not observe any crash from cadical. In the worst option, without any bump, the performance drop, but not as much as I expected, only about 5%. But, of course, the bumping would be more important in longer runs, I only used 1 minute runs.

Changes in 3 files:

analyze.cpp: --- just inserted the conditional to bump only the first variables
void Internal::bump_variable (int lit) {
if(max_bump == 0 || vidx(lit) <= max_bump) {
if (use_scores ()) bump_variable_score (lit);
else bump_queue (lit);
}
}

internal.hpp: --- create the max_bump variable in struct Internal
int max_bump;

cadical.cpp --- in main, load the paramter, and set max_bump
int initial_bump = 0;
--- insert in paramters, duplicate one of the conditionals, to add in my case parameter -B:
} else if (has_prefix (argv[i], "-B")) {
if (!parse_int_str (argv[i] + 2, initial_bump))
APPERR ("invalid bump option '%s'", argv[i]);
if (initial_bump < 0)
APPERR ("invalid argument in '%s' (expected non-negative number)",
argv[i]);
--- before start solving, set the max_bump
solver->internal->max_bump=initial_bump;

To use is a matter of calling cadical with for example "-B100", will bump only variables in conflicts, that have ID lower or equal than 100.

Is good that cadical is very well optimized, and this is not needed at least in my instances. The users from other problems, can concentrate on the transformation to SAT.

Thanks for the solver.

Best regards,
José Coelho