Correcting s-line for SATISFIABLE decision instance of pseudo-Boolean problems

Author: marekpiotrow

MsSolver.cc

@@ -490,7 +490,12 @@ void MsSolver::maxsat_solve(solve_Command cmd)
         if (status == l_Undef && termCallback != nullptr && 0 != termCallback(termCallbackState))
             asynch_interrupt = true;
         if (soft_cls.size() == 0) {
-            if (!ipamir_used) opt_satisfiable_out = false;
+            if (!ipamir_used) {
+                if (!opt_maxsat && goal == NULL && satisfied)      // force a correct output for
+                    opt_satisfiable_out = asynch_interrupt = true; // pseudo-Boolean decision problems
+                else opt_satisfiable_out = false;
+                if (opt_verbosity > 0) printStats(true);
+            }
             return;
         } else if (status == l_True) {
             for (int i = 0; i < soft_cls.size(); i++)

PbSolver.cc

@@ -719,9 +719,10 @@ void PbSolver::solve(solve_Command cmd)
     if (opt_verbosity >= 1){
         if      (!sat)
             reportf(asynch_interrupt ? "\bUNKNOWN\b\n" : "\bUNSATISFIABLE\b\n");
-        else if (goal == NULL)
+        else if (goal == NULL && !opt_maxsat) {
             reportf("\bSATISFIABLE: No goal function specified.\b\n");
-        else if (cmd == sc_FirstSolution){
+            asynch_interrupt = true; // to get SATISFIABLE result
+        } else if (cmd == sc_FirstSolution){
             char* tmp = toString(best_goalvalue * goal_gcd);
             reportf("\bFirst solution found: %s\b\n", tmp);
             xfree(tmp);
@@ -734,6 +735,7 @@ void PbSolver::solve(solve_Command cmd)
             reportf("\bOptimal solution: %s\b\n", tmp);
             xfree(tmp);
         }
+        printStats(true);
     }
 }
 

README.md

@@ -25,7 +25,7 @@ Since version 1.7.0 the default SAT solver is changed to CaDiCaL by Armin Biere.
     git clone https://github.com/arminbiere/cadical  
     cd cadical  
     patch -p1 <../uwrmaxsat/cadical.patch  
-    ./configure  
+    ./configure --no-contracts --no-tracing  
     make cadical  
     cd ../uwrmaxsat  
     cp config.cadical config.mk  

SatSolver.cc

@@ -175,7 +175,7 @@ bool ExtSimpSolver::impliedObservedLits(Lit lit, Minisat::vec<Lit>& props, const
     if (!okay()) return false;
     if (value(lit) != l_Undef) return value(lit) == l_True;
     for (int i = 0; i < assumps.size(); i++)
-        if (value(assumps[i]) == l_False) return false;
+        if (value(assumps[i]) == l_False) return true;
 
     for (int i = 0; i < assumps.size(); i++)
         if (value(assumps[i]) != l_True && toInt(assumps[i]) >= 0) solver->assume(lit2val(assumps[i]));
@@ -184,15 +184,15 @@ bool ExtSimpSolver::impliedObservedLits(Lit lit, Minisat::vec<Lit>& props, const
     solver->limit ("decisions", 1); // set decision limit to one
     lbool ret = solveLimited();
 
-    if (ret == l_Undef && extPropagator->dec_level > 1) {
+    if (ret != l_False && extPropagator->dec_level > 1) {
         for (const int clit : extPropagator->last_trails[1 - extPropagator->dec_level % 2]) {
             if (clit != 0) {
                 Lit l = mkLit(abs(clit) - 1, clit < 0);
                 if (l != lit) props.push(l);
             }
         }
     }
-    return ret == l_Undef;
+    return ret != l_False;
 }
 #elif defined(MERGESAT)
 bool ExtSimpSolver::impliedObservedLits(Lit lit, Minisat::vec<Lit>& props, const vec<Lit>& assumptions, int )