Fixing some problems found by testSolver.py from https://github.com/t…

…obipaxe/MaxSATRegressionSuite

.github/workflows/macos-build.yml

@@ -34,13 +34,20 @@ jobs:
         USESCIP= CXXFLAGS=$(pkg-config --cflags gmp) LDFLAGS=$(pkg-config --libs gmp) make r
     - name: test executable
       run: |
+        set +e
         build/release/bin/uwrmaxsat -of Examples/unsat.opb
+        if ! [ $? -eq 20 ] ; then exit 1 ; fi
         build/release/bin/uwrmaxsat -of Examples/garden9x9.opb
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi
         build/release/bin/uwrmaxsat -bm Examples/satellite02ac.wcsp.wcnf
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi
         build/release/bin/uwrmaxsat -maxpre -bm Examples/satellite02ac.wcsp.wcnf
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi
     - name: build and test BIGWEIGHTS
       run: |
         USESCIP= make clean
         sed -i '' 's/BIGWEIGHTS?=#/BIGWEIGHTS?=/' config.mk
         USESCIP= CXXFLAGS=$(pkg-config --cflags gmp) LDFLAGS=$(pkg-config --libs gmp) make r
+        set +e
         build/release/bin/uwrmaxsat -of Examples/stein27_bignum.opb
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi

.github/workflows/msys2-build.yml

@@ -42,13 +42,20 @@ jobs:
         USESCIP= make r
     - name: test executable
       run: |
+        set +e
         build/release/bin/uwrmaxsat -of Examples/unsat.opb
+        if ! [ $? -eq 20 ] ; then exit 1 ; fi
         build/release/bin/uwrmaxsat -of Examples/garden9x9.opb
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi
         build/release/bin/uwrmaxsat -bm Examples/satellite02ac.wcsp.wcnf
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi
         build/release/bin/uwrmaxsat -maxpre -bm Examples/satellite02ac.wcsp.wcnf
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi
     - name: build and test BIGWEIGHTS  
       run: |
         USESCIP= make clean
         sed -i 's/BIGWEIGHTS?=#/BIGWEIGHTS?=/' config.mk
         USESCIP= make r
+        set +e
         build/release/bin/uwrmaxsat -of Examples/stein27_bignum.opb
+        if ! [ $? -eq 30 ] ; then exit 1 ; fi

MsSolver.cc

@@ -411,20 +411,33 @@ void MsSolver::maxsat_solve(solve_Command cmd)
     if (opt_verbosity >= 1) sat_solver.verbEveryConflicts = 100000;
     sat_solver.setIncrementalMode();
 #endif
+    // Convert PB constraints:
     pb_n_vars = nVars();
     pb_n_constrs = nClauses();
+    if (constrs.size() > 0) {
+        if (opt_verbosity >= 1)
+            reportf("Converting %d PB-constraints to clauses...\n", constrs.size());
+        propagate();
+        if (!convertPbs(true)){
+            if (opt_verbosity >= 1) sat_solver.printVarsCls(constrs.size() > 0);
+            assert(!okay()); return;
+        }
+        if (opt_convert_goal != ct_Undef)
+            opt_convert = opt_convert_goal;
+    }
     if (soft_cls.size() == 0) {
         extern bool opt_satisfiable_out;
         Minisat::vec<Lit> assump_ps;
         Lit assump_lit = lit_Undef;
-        if (global_assumptions.size() == 0) {
+        if (global_assumptions.size() == 0 && ipamir_used) {
             assump_lit = mkLit(sat_solver.newVar(VAR_UPOL, !opt_branch_pbvars), true);
             assump_ps.push(assump_lit);
         }
         if (opt_verbosity >= 1) sat_solver.printVarsCls();
         lbool status = satSolveLimited(assump_ps);
-        best_goalvalue = (status == l_True ? fixed_goalval : INT_MAX);
+        best_goalvalue = (status == l_True ? fixed_goalval : Int_MAX);
         if (status == l_True) {
+            satisfied = true;
             best_model.clear();
             for (Var x = 0; x < pb_n_vars; x++)
                 assert(sat_solver.modelValue(x) != l_Undef),
@@ -435,18 +448,6 @@ void MsSolver::maxsat_solve(solve_Command cmd)
         if (!ipamir_used) opt_satisfiable_out = false;
         return;
     }
-    // Convert constraints:
-    if (constrs.size() > 0) {
-        if (opt_verbosity >= 1)
-            reportf("Converting %d PB-constraints to clauses...\n", constrs.size());
-        propagate();
-        if (!convertPbs(true)){
-            if (opt_verbosity >= 1) sat_solver.printVarsCls(constrs.size() > 0);
-            assert(!okay()); return;
-        }
-        if (opt_convert_goal != ct_Undef)
-            opt_convert = opt_convert_goal;
-    }
 
     // Freeze goal function variables (for SatELite):
     for (int i = 0; i < soft_cls.size(); i++) {
@@ -549,6 +550,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
             pj = p; j++; min_weight = 0;
         }
     }
+    if (j > 0 && soft_cls[j-1].fst == 0) j--;
     if (j < soft_cls.size()) soft_cls.shrink(soft_cls.size() - j);
     top_for_strat = top_for_hard = soft_cls.size();
     Sort::sort(soft_cls);
@@ -644,7 +646,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
     extern bool opt_use_scip_slvr;
     ScipSolver scip_solver;
     int sat_orig_vars = sat_solver.nVars(), sat_orig_cls = sat_solver.nClauses();
-    if (opt_use_scip_slvr && UB_goalval < Int(uint64_t(2) << std::numeric_limits<double>::digits) && l_True == 
+    if (opt_use_scip_slvr && UB_goalval * goal_gcd < Int(uint64_t(1) << std::numeric_limits<double>::digits - 3) && l_True == 
       scip_solve(&assump_ps, &assump_Cs, &delayed_assump, weighted_instance, sat_orig_vars, sat_orig_cls, scip_solver)) {
         if (ipamir_used) reset_soft_cls(soft_cls, fixed_soft_cls, modified_soft_cls, goal_gcd);
         return;
@@ -1194,16 +1196,16 @@ void MsSolver::maxsat_solve(solve_Command cmd)
     if (ipamir_used) reset_soft_cls(soft_cls, fixed_soft_cls, modified_soft_cls, goal_gcd);
 #ifdef USE_SCIP
     char test = OPT_NONE;
-    bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < INT_MAX
+    bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < Int_MAX
                           && opt_finder.compare_exchange_strong(test, OPT_MSAT);
 #else
-    bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < INT_MAX;
+    bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < Int_MAX;
 #endif
 			  ;
     if (opt_verbosity >= 1 && opt_output_top < 0){
         if      (!satisfied)
             reportf(asynch_interrupt ? "\bUNKNOWN\b\n" : "\bUNSATISFIABLE\b\n");
-        else if (soft_cls.size() == 0 && best_goalvalue == INT_MAX)
+        else if (soft_cls.size() == 0 && best_goalvalue == Int_MAX)
             reportf("\bSATISFIABLE: No goal function specified.\b\n");
         else if (cmd == sc_FirstSolution){
             char* tmp = toString(best_goalvalue);

PbSolver.h

@@ -32,10 +32,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifdef BIG_WEIGHTS
 using weight_t = Int;
 #define toweight(x) (x)
+#define fromweight(x) tolong(x)
 #define WEIGHT_MAX Int_MAX
 #else
 using weight_t = int64_t;
 #define toweight(x) tolong(x)
+#define fromweight(x) (x)
 static inline const char *toString(weight_t x) { static char buf[30]; sprintf(buf, "%" PRId64, x); return buf;  }
 #define WEIGHT_MAX std::numeric_limits<weight_t>::max()
 #endif

ScipSolver.cc

@@ -88,7 +88,7 @@ void uwrLogMessage(FILE *file, const char *msg)
 }
 SCIP_DECL_MESSAGEINFO(uwrMessageInfo) { (void)(messagehdlr); uwrLogMessage(file, msg); }
 
-lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbool> scip_model, MsSolver *solver, weight_t obj_offset)
+lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbool> scip_model, MsSolver *solver, int64_t obj_offset)
 {
     extern double opt_scip_cpu, opt_scip_cpu_add;
     lbool found_opt = l_Undef;
@@ -142,16 +142,17 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
         int64_t ubound = (!SCIPisInfinity(scip, primb) ? int64_t(round(primb)) + obj_offset : INT64_MAX);
         if (!solver->ipamir_used || opt_verbosity > 0)
             reportf("SCIP timeout with lower and upper bounds: [%lld, %lld]\n", lbound, ubound);
+        int64_t gcd = fromweight(solver->goal_gcd);
         if (!SCIPisInfinity(scip, dualb)) {
-            int64_t lb = (solver->goal_gcd == 1 ? lbound : (lbound > 0 ? lbound + solver->goal_gcd - 1 : lbound) / solver->goal_gcd);
+            int64_t lb = (gcd == 1 ? lbound : (lbound > 0 ? lbound + gcd - 1 : lbound) / gcd);
             if (Int(lb) > solver->scip_LB) solver->scip_LB = lb, solver->scip_foundLB = true;
         }
         if (!SCIPisInfinity(scip, primb)) {
-            int64_t ub = (solver->goal_gcd == 1 ? ubound : (ubound < 0 ? ubound - solver->goal_gcd + 1 : ubound) / solver->goal_gcd);
+            int64_t ub = (gcd == 1 ? ubound : (ubound < 0 ? ubound - gcd + 1 : ubound) / gcd);
             if (Int(ub) < solver->scip_UB) solver->scip_UB = ub, solver->scip_foundUB = true;
             SCIP_SOL *sol = SCIPgetBestSol(scip);
             if (sol != nullptr) {
-                Int scip_sol = (obj_offset + weight_t(round(SCIPgetSolOrigObj(scip, sol)))) / solver->goal_gcd;
+                Int scip_sol = (obj_offset + int64_t(round(SCIPgetSolOrigObj(scip, sol)))) / gcd;
                 if (scip_sol < solver->best_goalvalue) {
                     for (Var x = 0; x < (int)vars.size(); x++)
                         if (vars[x] != nullptr) {
@@ -200,7 +201,8 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
 		    reportf("SCIP optimum (rounded): %" PRId64 "\n", best_value);
 	    solver->best_goalvalue = best_value;
             vec<lbool> opt_model(scip_model.size()); 
-            for (int i = scip_model.size() - 1; i >= 0 ; i--) opt_model[i] = scip_model[i];
+            for (int i = scip_model.size() - 1; i >= 0 ; i--)
+                opt_model[i] = (scip_model[i] == l_Undef && !solver->sat_solver.isEliminated(i) ? l_False : scip_model[i]);
             solver->sat_solver.extendGivenModel(opt_model);
             solver->best_model.clear();
             for (int x = 0; x < solver->pb_n_vars; x++) solver->best_model.push(opt_model[x] != l_False);
@@ -315,12 +317,12 @@ lbool MsSolver::scip_solve(const Minisat::vec<Lit> *assump_ps,
         }
     }
 #endif
-    weight_t obj_offset = 0;
+    int64_t obj_offset = 0;
     int obj_vars = 0;
     auto set_var_coef = [&vars, &obj_offset, &obj_vars, scip, this](Lit relax, weight_t weight)
     {
         if (value(relax) != l_Undef) {
-            if (value(relax) == l_False) obj_offset += weight * this->goal_gcd;
+            if (value(relax) == l_False) obj_offset += fromweight(weight) * fromweight(this->goal_gcd);
         } else {
             obj_vars++;
             weight_t coef = sign(relax) ? weight : -weight;
@@ -329,7 +331,7 @@ lbool MsSolver::scip_solve(const Minisat::vec<Lit> *assump_ps,
             auto v = vars[var(relax)];
             MY_SCIP_CALL(SCIPaddVarObj(scip, v, double(coef)));
             if (coef < 0)
-                obj_offset -= coef;
+                obj_offset -= fromweight(coef);
         }
         return l_Undef;
     };
@@ -365,9 +367,9 @@ lbool MsSolver::scip_solve(const Minisat::vec<Lit> *assump_ps,
         if (set_var_coef(relax, weight) == l_False) return l_False;
     }
     if (opt_verbosity >= 2)
-        reportf("SCIPobj: obj_var=%d, obj_offset=%ld, ob_offset_to_add: %ld %ld\n", obj_vars, obj_offset,
+        reportf("SCIPobj: obj_var=%d, obj_offset=%" PRId64 ", ob_offset_to_add: %ld %ld\n", obj_vars, obj_offset,
                 goal_gcd * tolong(fixed_goalval), goal_gcd*tolong(harden_goalval));
-    obj_offset += goal_gcd * tolong(fixed_goalval + harden_goalval);
+    obj_offset += fromweight(goal_gcd) * tolong(fixed_goalval + harden_goalval);
 
     // 5. do solve
     // MY_SCIP_CALL((SCIPwriteOrigProblem(scip, "1.lp", nullptr, FALSE)));

ScipSolver.h

@@ -30,7 +30,7 @@ struct ScipSolver {
     SCIP *                   scip; 
     std::vector<SCIP_VAR *>  vars;
     std::vector<lbool>       model;
-    weight_t                 obj_offset;
+    int64_t                  obj_offset;
     bool                     must_be_started;
 
     ScipSolver() : scip(nullptr), obj_offset(0), must_be_started(false) {}
@@ -40,6 +40,6 @@ lbool scip_solve_async(SCIP *scip,
                        std::vector<SCIP_VAR *> vars,
                        std::vector<lbool> scip_model,
                        MsSolver *solver,
-                       weight_t obj_offset);
+                       int64_t obj_offset);
 
 #endif