solver: additional backjumping scheme

Enabled when all attempts to satisfy a name failed, we know that we
can ignore all decisions until we find a decision affecting the name
we wanted to satisfy.

2 files changed, 49 insertions, 11 deletions

diff --git a/src/apk_solver_data.h b/src/apk_solver_data.h
index fd79e65917..0327492056 100644
--- a/src/apk_solver_data.h
+++ b/src/apk_solver_data.h
@@ -40,6 +40,7 @@ struct apk_solver_name_state {
 	unsigned none_excluded : 1;
 	unsigned name_touched : 1;
 	unsigned preferred_chosen : 1;
+	unsigned backjump_enabled : 1;
 };
 
 #endif
diff --git a/src/solver.c b/src/solver.c
index 940282a10d..5d857925bb 100644
--- a/src/solver.c
+++ b/src/solver.c
@@ -921,6 +921,7 @@ static solver_result_t push_decision(struct apk_solver_state *ss,
 static int next_branch(struct apk_solver_state *ss)
 {
 	unsigned int backup_until = ss->num_decisions;
+	struct apk_name *backjump_name = NULL;
 
 	while (ss->num_decisions > 0) {
 		struct apk_decision *d = &ss->decisions[ss->num_decisions];
@@ -928,6 +929,11 @@ static int next_branch(struct apk_solver_state *ss)
 
 		undo_decision(ss, d);
 
+		/* If we undoed constraints on the backjump name, we
+		 * cannot backjump on it anymore. */
+		if (backjump_name && !backjump_name->ss.backjump_enabled)
+			backjump_name = NULL;
+
 #ifdef DEBUG_CHECKS
 		ASSERT(cmpscore(&d->saved_score, &ss->score) == 0,
 			"Saved_score "SCORE_FMT" != score "SCORE_FMT,
@@ -938,20 +944,32 @@ static int next_branch(struct apk_solver_state *ss)
 			name->name, d->saved_requirers, name->ss.requirers);
 #endif
 
-		if (backup_until >= ss->num_decisions &&
+		if ((backjump_name == NULL || backjump_name == d->name) &&
+		    backup_until >= ss->num_decisions &&
 		    d->branching_point == BRANCH_YES) {
 			d->branching_point = BRANCH_NO;
 			d->type = (d->type == DECISION_ASSIGN) ? DECISION_EXCLUDE : DECISION_ASSIGN;
 			return apply_decision(ss, d);
-		} else {
-			if (d->branching_point == BRANCH_YES)
+		} else if (d->branching_point == BRANCH_YES) {
+			if (backup_until < ss->num_decisions)
 				dbg_printf("skipping %s, %d < %d\n",
 					name->name, backup_until, ss->num_decisions);
+			else if (backjump_name != NULL && backjump_name != d->name)
+				dbg_printf("backjumping to find new assign candidate for %s\n",
+					backjump_name->name);
 		}
 
+		/* Back jump to find assign candidate for this name */
+		if (d->name->ss.backjump_enabled && backjump_name == NULL)
+			backjump_name = d->name;
+
 		/* When undoing the initial "exclude none" decision, check if
 		 * we can backjump. */
 		if (d->has_package == 0 && !d->found_solution) {
+			if (backjump_name == d->name) {
+				d->name->ss.backjump_enabled = 0;
+				backjump_name = NULL;
+			}
 			if (d->backup_until && backup_until > d->backup_until)
 				backup_until = d->backup_until;
 		}
@@ -1022,7 +1040,7 @@ static void apply_constraint(struct apk_solver_state *ss, struct apk_dependency
 				   ps0->conflicts);
 			changed |= 1;
 		} else if (requirer_pkg != NULL) {
-			dbg_printf(PKG_VER_FMT ": inheriting flags and pinning from"PKG_VER_FMT"\n",
+			dbg_printf(PKG_VER_FMT ": inheriting flags and pinning from "PKG_VER_FMT"\n",
 				   PKG_VER_PRINTF(pkg0),
 				   PKG_VER_PRINTF(requirer_pkg));
 			changed |= inherit_package_state(ss->db, pkg0, requirer_pkg);
@@ -1090,6 +1108,7 @@ static void undo_constraint(struct apk_solver_state *ss, struct apk_dependency *
 				ps0->conflicts--;
 			else
 				ps0->unsatisfied--;
+			pkg0->name->ss.backjump_enabled = 0;
 			dbg_printf(PKG_VER_FMT ": conflicts-- -> %d\n",
 				   PKG_VER_PRINTF(pkg0),
 				   ps0->conflicts);
@@ -1132,6 +1151,9 @@ static int reconsider_name(struct apk_solver_state *ss, struct apk_name *name)
 				SCORE_PRINTF(&ss->best_score));
 			return push_decision(ss, name, NULL, DECISION_EXCLUDE, BRANCH_NO, FALSE);
 		}
+
+		name->ss.backjump_enabled = 0;
+		return push_decision(ss, name, NULL, DECISION_EXCLUDE, BRANCH_YES, FALSE);
 	}
 
 	for (i = 0; i < name->providers->num; i++) {
@@ -1151,17 +1173,23 @@ static int reconsider_name(struct apk_solver_state *ss, struct apk_name *name)
 			if (!p00->name->ss.locked)
 				continue;
 			if (p00->name->ss.chosen.version != &apk_null_blob ||
-			    p00->version != &apk_null_blob)
-				break;
+			    p00->version != &apk_null_blob) {
+				dbg_printf("reconsider_name: "PKG_VER_FMT": pruning due to provides (%s) conflict\n",
+					   PKG_VER_PRINTF(pkg0), p00->name->name);
+				return push_decision(ss, name, pkg0, DECISION_EXCLUDE, BRANCH_NO, FALSE);
+			}
 		}
-		if (j < pkg0->provides->num)
-			continue;
 
 		score_locked = get_topology_score(ss, pkg0, &pkg0_score);
 
 		/* viable alternative? */
-		if (cmpscore2(&ss->score, &pkg0_score, &ss->best_score) >= 0)
+		if (cmpscore2(&ss->score, &pkg0_score, &ss->best_score) >= 0) {
+			dbg_printf("reconsider_name: "PKG_VER_FMT": pruning due to score "SCORE_FMT"+"SCORE_FMT">="SCORE_FMT"\n",
+				   PKG_VER_PRINTF(pkg0),
+				   SCORE_PRINTF(&ss->score), SCORE_PRINTF(&pkg0_score),
+				   SCORE_PRINTF(&ss->best_score));
 			return push_decision(ss, name, pkg0, DECISION_EXCLUDE, BRANCH_NO, FALSE);
+		}
 
 		if (cmpscore(&pkg0_score, &best_score) < 0) {
 			best_score = pkg0_score;
@@ -1180,14 +1208,19 @@ static int reconsider_name(struct apk_solver_state *ss, struct apk_name *name)
 
 	/* no options left */
 	if (options == 0) {
+		name->ss.backjump_enabled = 1;
+		if (name->ss.none_excluded) {
+			dbg_printf("reconsider_name: %s: no options pruning branch\n",
+				name->name);
+			return SOLVERR_PRUNED;
+		}
 		dbg_printf("reconsider_name: %s: no options locking none\n",
 			name->name);
-		if (name->ss.none_excluded)
-			return SOLVERR_PRUNED;
 		return push_decision(ss, name, NULL, DECISION_ASSIGN, BRANCH_NO, FALSE);
 	} else if (options == 1 && score_locked && name->ss.none_excluded && name == next_p->pkg->name) {
 		dbg_printf("reconsider_name: %s: only one choice left with known score, locking.\n",
 			name->name);
+		name->ss.backjump_enabled = 1;
 		return push_decision(ss, name, next_p->pkg, DECISION_ASSIGN, BRANCH_NO, FALSE);
 	}
 
@@ -1258,11 +1291,14 @@ static int expand_branch(struct apk_solver_state *ss)
 			primary_decision = DECISION_ASSIGN;
 		else
 			primary_decision = DECISION_EXCLUDE;
+		name->ss.backjump_enabled = 0;
 		return push_decision(ss, name, NULL, primary_decision, BRANCH_YES, FALSE);
 	}
 
 	if (!can_install) {
 		/* provides with no version; not eglible to auto install */
+		dbg_printf("expand_branch: "PKG_VER_FMT" not installable. excluding.",
+			   PKG_VER_PRINTF(pkg0));
 		return push_decision(ss, pkg0->name, pkg0, DECISION_EXCLUDE, BRANCH_NO, TRUE);
 	}
 
@@ -1326,6 +1362,7 @@ static void record_solution(struct apk_solver_state *ss)
 		unsigned short pinning;
 		unsigned int repos;
 
+		name->ss.backjump_enabled = 0;
 		d->found_solution = 1;
 
 		if (pkg == NULL) {