From 4f103fde6c2aca51b6628721280094e029423df4 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Sun, 21 Apr 2024 01:49:17 -0700 Subject: [PATCH 1/4] more decision hints --- src/mcsat/nra/nra_plugin.c | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 422c3a3f3..11b13870a 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -860,6 +860,7 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, } lp_value_destruct(&v); } + if (!x_in_conflict && !trail_has_value(nra->ctx->trail, x)) { const lp_feasibility_set_t *feasible_set = feasible_set_db_get(nra->feasible_set_db, x); if (lp_feasibility_set_is_point(feasible_set)) { @@ -880,6 +881,25 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, } } lp_value_destruct(&x_value); + + } else if (variable_db_is_int(nra->ctx->var_db, x) && + !lp_feasibility_set_is_full(feasible_set)) { + lp_interval_t x_interval; + lp_interval_construct_full(&x_interval); + feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval); + int interval_dist = lp_interval_size_approx(&x_interval); + if (0 < interval_dist && interval_dist <= 1) { + // interval distance 1 means that the absolute distance + // between the upper and lower bound is 1. + // interval distance 0 means that the interval is a point. + // So, we are hinting to the main mcsat solver to decide on this variable + // as the possible integer values for the variable is highly likely one. + if (ctx_trace_enabled(nra->ctx, "nra::propagate")) { + ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", x); + } + nra->ctx->hint_next_decision(nra->ctx, x); + } + lp_interval_destruct(&x_interval); } } } From d289d098c76d1e621ce7dd699d68708d6a01c3b6 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Mon, 22 Apr 2024 15:09:05 -0700 Subject: [PATCH 2/4] update comments --- src/mcsat/nra/nra_plugin.c | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 11b13870a..747f9e055 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -888,11 +888,14 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, lp_interval_construct_full(&x_interval); feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval); int interval_dist = lp_interval_size_approx(&x_interval); - if (0 < interval_dist && interval_dist <= 1) { - // interval distance 1 means that the absolute distance + if (interval_dist <= 1) { + // interval distance 1 means that the absolute log2 distance // between the upper and lower bound is 1. - // interval distance 0 means that the interval is a point. - // So, we are hinting to the main mcsat solver to decide on this variable + // Consider the the interval [3,4], the interval distance is 1, and has + // two integer value: 3 and 4. + // Now consider the interval [5.5, 6.1], the interval distance is also 1 and + // has one integer value: 6. + // Here, we are hinting to the main mcsat solver to decide on this variable // as the possible integer values for the variable is highly likely one. if (ctx_trace_enabled(nra->ctx, "nra::propagate")) { ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", x); From ccde28f5337023651a90a574e40e9c8f86f17a89 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Mon, 22 Apr 2024 20:11:47 -0700 Subject: [PATCH 3/4] more comments --- src/mcsat/nra/nra_plugin.c | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 747f9e055..20d9873ab 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -885,16 +885,20 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, } else if (variable_db_is_int(nra->ctx->var_db, x) && !lp_feasibility_set_is_full(feasible_set)) { lp_interval_t x_interval; - lp_interval_construct_full(&x_interval); + lp_interval_construct_full(&x_interval); // [-inf, +inf] + // now we over-approx the feasible set using an interval and + // the result is stored in x_interval, e.g., [1.6, 2.5] + // union [4.2, 4.6] is approximated by [1.6, 2.5]. feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval); int interval_dist = lp_interval_size_approx(&x_interval); if (interval_dist <= 1) { + // interval distance of an interval [a, b] is defined as log2(|b - a|) + 1. // interval distance 1 means that the absolute log2 distance // between the upper and lower bound is 1. // Consider the the interval [3,4], the interval distance is 1, and has // two integer value: 3 and 4. - // Now consider the interval [5.5, 6.1], the interval distance is also 1 and - // has one integer value: 6. + // Now consider the interval [5.5, 6.1], the interval distance is also 0 and + // has one integer value: 6. log2(.6) = log2(6) - log2(10). // Here, we are hinting to the main mcsat solver to decide on this variable // as the possible integer values for the variable is highly likely one. if (ctx_trace_enabled(nra->ctx, "nra::propagate")) { From 9865782584f94c16a5152bfc7d0ae74486aba1f9 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Mon, 22 Apr 2024 22:17:36 -0700 Subject: [PATCH 4/4] typos in comments --- src/mcsat/nra/nra_plugin.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 8f68c7da6..e861e1d79 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -888,7 +888,7 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, lp_interval_construct_full(&x_interval); // [-inf, +inf] // now we over-approx the feasible set using an interval and // the result is stored in x_interval, e.g., [1.6, 2.5] - // union [4.2, 4.6] is approximated by [1.6, 2.5]. + // union [4.2, 4.6] is approximated by [1.6, 4.6]. feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval); int interval_dist = lp_interval_size_approx(&x_interval); if (interval_dist <= 1) { @@ -897,7 +897,7 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, // between the upper and lower bound is 1. // Consider the the interval [3,4], the interval distance is 1, and has // two integer value: 3 and 4. - // Now consider the interval [5.5, 6.1], the interval distance is also 0 and + // Now consider the interval [5.5, 6.1], the interval distance is 0 and // has one integer value: 6. log2(.6) = log2(6) - log2(10). // Here, we are hinting to the main mcsat solver to decide on this variable // as the possible integer values for the variable is highly likely one.