>From 135812278d74a3dd632713885ba47daa05a2b175 Mon Sep 17 00:00:00 2001 From: Hans Petter Selasky Date: Thu, 24 Nov 2016 13:35:37 +0100 Subject: [PATCH] Optimise SAT solving. Signed-off-by: Hans Petter Selasky --- libpkg/pkg_solve.c | 317 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 315 insertions(+), 2 deletions(-) diff --git a/libpkg/pkg_solve.c b/libpkg/pkg_solve.c index 9cf08e2..d50281f 100644 --- a/libpkg/pkg_solve.c +++ b/libpkg/pkg_solve.c @@ -1074,8 +1074,299 @@ pkg_solve_set_initial_assumption(struct pkg_solve_problem *problem, } } -int -pkg_solve_sat_problem(struct pkg_solve_problem *problem) +static int +pkg_solve_item_compare(const void *ppa, const void *ppb) +{ + struct pkg_solve_item *ia = *(struct pkg_solve_item **)ppa; + struct pkg_solve_item *ib = *(struct pkg_solve_item **)ppb; + int va = ia->var->order * ia->inverse; + int vb = ib->var->order * ib->inverse; + + if (va > vb) + return (1); + else if (va < vb) + return (-1); + return (0); +} + +static int +pkg_solve_rule_compare(const void *ppa, const void *ppb) +{ + struct pkg_solve_rule *ra = *(struct pkg_solve_rule **)ppa; + struct pkg_solve_rule *rb = *(struct pkg_solve_rule **)ppb; + struct pkg_solve_item *ia; + struct pkg_solve_item *ib; + size_t na = 0; + size_t nb = 0; + + LL_FOREACH(ra->items, ia) + na++; + LL_FOREACH(rb->items, ib) + nb++; + + if (na > nb) + return (1); + else if (na < nb) + return (-1); + + ia = ra->items; + ib = rb->items; + while (ia != 0 && ib != 0) { + int va = ia->var->order * ia->inverse; + int vb = ib->var->order * ib->inverse; + if (va > vb) + return (1); + else if (va < vb) + return (-1); + ia = ia->next; + ib = ib->next; + } + return (0); +} + +static int +pkg_solve_sat_problem_sub(struct pkg_solve_problem *problem) +{ + struct pkg_solve_rule **rule_array; + struct pkg_solve_rule *rule; + struct pkg_solve_item *item; + int res, iter = 0; + size_t skipped = 0; + size_t i; + size_t n; + bool need_reiterate = false; + const int *failed = NULL; + int attempt = 0; + struct pkg_solve_variable *var; + + rule_array = (struct pkg_solve_rule **)calloc(kv_size(problem->rules), sizeof(void *)); + if (rule_array == NULL) + return (EPKG_FATAL); + + n = kv_size(problem->rules); + for (i = 0; i != n; i++) { + size_t j; + size_t k; + + rule = kv_A(problem->rules, i); + rule_array[i] = rule; + + j = 0; + LL_FOREACH(rule->items, item) + j++; + + struct pkg_solve_item *item_array[j]; + + j = 0; + LL_FOREACH(rule->items, item) + item_array[j++] = item; + + mergesort(item_array, j, sizeof(void *), pkg_solve_item_compare); + + rule->items = 0; + for (k = 0; k != j; k++) { + /* if items are identical, skip them */ + if (k != j - 1 && + pkg_solve_item_compare(item_array + k, item_array + k + 1) == 0) { + free(item_array[k]); + continue; + } + item_array[k]->next = rule->items; + rule->items = item_array[k]; + } + } + + mergesort(rule_array, n, sizeof(void *), pkg_solve_rule_compare); + + for (i = 0; i != n; i++) { + /* if rules are identical, skip them */ + if (i != n - 1 && + pkg_solve_rule_compare(rule_array + i, rule_array + i + 1) == 0) { + skipped++; + continue; + } + rule = rule_array[i]; + LL_FOREACH(rule->items, item) { + picosat_add(problem->sat, item->var->order * item->inverse); + } + + picosat_add(problem->sat, 0); + pkg_debug_print_rule(rule); + } + + for (i = 0; i != n; i++) { + /* if rules are identical, skip them */ + if (i != n - 1 && + pkg_solve_rule_compare(rule_array + i, rule_array + i + 1) == 0) + continue; + rule = rule_array[i]; + pkg_solve_set_initial_assumption(problem, rule); + } + + free(rule_array); + + pkg_emit_notice("Skipped %lld identical rules", (long long)skipped); + +reiterate: + pkg_emit_notice("Reiterate"); + + res = pkg_solve_picosat_iter(problem, iter); + + if (res != PICOSAT_SATISFIABLE) { + /* + * in case we cannot satisfy the problem it appears by + * experience that the culprit seems to always be the latest of + * listed in the failed assumptions. + * So try to remove them for the given problem. + * To avoid endless loop allow a maximum of 10 iterations no + * more + */ + failed = picosat_failed_assumptions(problem->sat); + attempt++; + + /* get the last failure */ + while (*failed) { + failed++; + } + failed--; + + if (attempt >= 10) { + pkg_emit_error("Cannot solve problem using SAT solver"); + UT_string *sb; + utstring_new(sb); + + while (*failed) { + var = &problem->variables[abs(*failed) - 1]; + for (i = 0; i < kv_size(problem->rules); i++) { + rule = kv_A(problem->rules, i); + + if (rule->reason != PKG_RULE_DEPEND) { + LL_FOREACH(rule->items, item) { + if (item->var == var) { + pkg_print_rule_buf(rule, sb); + utstring_printf(sb, "%c", '\n'); + break; + } + } + } + } + + utstring_printf(sb, "cannot %s package %s, remove it from request? ", + var->flags & PKG_VAR_INSTALL ? "install" : "remove", var->uid); + + if (pkg_emit_query_yesno(true, utstring_body(sb))) { + var->flags |= PKG_VAR_FAILED; + } + + failed++; + need_reiterate = true; + } + utstring_clear(sb); + } else { + pkg_emit_notice("Cannot solve problem using SAT solver, trying another plan"); + var = &problem->variables[abs(*failed) - 1]; + + var->flags |= PKG_VAR_FAILED; + + need_reiterate = true; + } + +#if 0 + failed = picosat_next_maximal_satisfiable_subset_of_assumptions(problem->sat); + + while (*failed) { + struct pkg_solve_variable *var = &problem->variables[*failed - 1]; + + pkg_emit_notice("var: %s", var->uid); + + failed ++; + } + + return (EPKG_AGAIN); +#endif + } + else { + + /* Assign vars */ + for (i = 0; i < problem->nvars; i ++) { + int val = picosat_deref(problem->sat, i + 1); + struct pkg_solve_variable *var = &problem->variables[i]; + + if (val > 0) + var->flags |= PKG_VAR_INSTALL; + else + var->flags &= ~PKG_VAR_INSTALL; + + pkg_debug(2, "decided %s %s-%s to %s", + var->unit->pkg->type == PKG_INSTALLED ? "local" : "remote", + var->uid, var->digest, + var->flags & PKG_VAR_INSTALL ? "install" : "delete"); + } + + /* Check for reiterations */ + if ((problem->j->type == PKG_JOBS_INSTALL || + problem->j->type == PKG_JOBS_UPGRADE) && iter == 0) { + for (i = 0; i < problem->nvars; i ++) { + bool failed_var = false; + struct pkg_solve_variable *var = &problem->variables[i], *cur; + + if (!(var->flags & PKG_VAR_INSTALL)) { + LL_FOREACH(var, cur) { + if (cur->flags & PKG_VAR_INSTALL) { + failed_var = false; + break; + } + else if (cur->unit->pkg->type == PKG_INSTALLED) { + failed_var = true; + } + } + } + + /* + * If we want to delete local packages on installation, do one more SAT + * iteration to ensure that we have no other choices + */ + if (failed_var) { + pkg_debug (1, "trying to delete local package %s-%s on install/upgrade," + " reiterate on SAT", + var->unit->pkg->name, var->unit->pkg->version); + need_reiterate = true; + + LL_FOREACH(var, cur) { + cur->flags |= PKG_VAR_FAILED; + } + } + } + } + } + + if (need_reiterate) { + iter ++; + + /* Restore top-level assumptions */ + for (i = 0; i < problem->nvars; i ++) { + struct pkg_solve_variable *var = &problem->variables[i]; + + if (var->flags & PKG_VAR_TOP) { + if (var->flags & PKG_VAR_FAILED) { + var->flags ^= PKG_VAR_INSTALL | PKG_VAR_FAILED; + } + + picosat_assume(problem->sat, var->order * + (var->flags & PKG_VAR_INSTALL ? 1 : -1)); + } + } + + need_reiterate = false; + + goto reiterate; + } + + return (EPKG_OK); +} + +static int +pkg_solve_sat_problem_old(struct pkg_solve_problem *problem) { struct pkg_solve_rule *rule; struct pkg_solve_item *item; @@ -1103,6 +1394,7 @@ pkg_solve_sat_problem(struct pkg_solve_problem *problem) } reiterate: + pkg_emit_notice("Reiterate"); res = pkg_solve_picosat_iter(problem, iter); @@ -1259,6 +1551,27 @@ reiterate: return (EPKG_OK); } +int +pkg_solve_sat_problem(struct pkg_solve_problem *problem) +{ + struct timeval tv0; + gettimeofday(&tv0, NULL); + int err; + + if (getenv("PKG_NO_SORT") != NULL) + err = pkg_solve_sat_problem_old(problem); + else + err = pkg_solve_sat_problem_sub(problem); + struct timeval tv1; + gettimeofday(&tv1, NULL); + + timersub(&tv1, &tv0, &tv1); + + pkg_emit_notice("SAT solving took %llds and %lld usecs", (long long)tv1.tv_sec, (long long)tv1.tv_usec); + + return (err); +} + void pkg_solve_dot_export(struct pkg_solve_problem *problem, FILE *file) { -- 2.10.1