Revision 613cbffb7e96f803f23141771593a583bb420279 authored by Pedro Orvalho on 28 April 2023, 12:39:23 UTC, committed by GitHub on 28 April 2023, 12:39:23 UTC
1 parent bab67fc
Alg_WMSU3.cc
/*!
* \author Ruben Martins - rubenm@andrew.cmu.edu
*
* @section LICENSE
*
* Open-WBO, Copyright (c) 2013-2022, Ruben Martins, Vasco Manquinho, Ines Lynce
* UpMax, Copyright (c) 2022, Pedro Orvalho, Vasco Manquinho, Ruben Martins
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in
* all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*
*/
#include "Alg_WMSU3.h"
using namespace upmax;
/*_________________________________________________________________________________________________
|
| WMSU3_none : [void] -> [void]
|
| Description:
|
| Non-incremental WMSU3 algorithm.
| Similar to the MSU3 algorithm but uses PB constraints instead of
| cardinality constraints.
|
| For further details see:
| * Joao Marques-Silva, Jordi Planes: On Using Unsatisfiability for
| Solving Maximum Satisfiability. CoRR abs/0712.1097 (2007)
|
| Post-conditions:
| * 'ubCost' is updated.
| * 'lbCost' is updated.
| * 'nbSatisfiable' is updated.
| * 'nbCores' is updated.
|
|________________________________________________________________________________________________@*/
StatusCode WMSU3::WMSU3_none()
{
//nbInitialVariables = maxsat_formula->nVars();
lbool res = l_True;
initRelaxation();
solver = rebuildSolver();
encoder.setIncremental(_INCREMENTAL_NONE_);
activeSoft.growTo(maxsat_formula->nSoft(), false);
for (int i = 0; i < maxsat_formula->nSoft(); i++)
coreMapping[maxsat_formula->getSoftClause(i).assumption_var] = i;
assumptions.clear();
for (;;)
{
res = searchSATSolver(solver, assumptions);
if (res == l_True)
{
nbSatisfiable++;
uint64_t newCost = computeCostModel(solver->model);
if (newCost < ubCost || nbSatisfiable == 1)
{
saveModel(solver->model);
printf("o %" PRIu64 "\n", newCost);
ubCost = newCost;
}
if (ubCost == 0 || lbCost == ubCost ||
(currentWeight == 1 && nbSatisfiable > 1))
{
assert(nbSatisfiable > 0);
printAnswer(_OPTIMUM_);
exit(_OPTIMUM_);
}
for (int i = 0; i < maxsat_formula->nSoft(); i++)
if (maxsat_formula->getSoftClause(i).weight >= currentWeight && !activeSoft[i])
assumptions.push(~maxsat_formula->getSoftClause(i).assumption_var);
}
if (res == l_False)
{
nbCores++;
// Assumes that the first SAT call is done with the soft clauses disabled.
if (nbSatisfiable == 0)
{
printAnswer(_UNSATISFIABLE_);
exit(_UNSATISFIABLE_);
}
if (lbCost == ubCost)
{
assert(nbSatisfiable > 0); // Otherwise, the problem is UNSAT.
if (verbosity > 0) printf("c LB = UB\n");
printAnswer(_OPTIMUM_);
exit(_OPTIMUM_);
}
sumSizeCores += solver->conflict.size();
if (solver->conflict.size() == 0) nbCores--;
for (int i = 0; i < solver->conflict.size(); i++)
{
int index_soft = coreMapping[solver->conflict[i]];
assert(!activeSoft[index_soft]);
activeSoft[index_soft] = true;
}
objFunction.clear();
coeffs.clear();
assumptions.clear();
for (int i = 0; i < maxsat_formula->nSoft(); i++)
{
// If a soft clause is active then is added to the 'currentObjFunction'
if (activeSoft[i])
{
objFunction.push(maxsat_formula->getSoftClause(i).relaxation_vars[0]);
coeffs.push(maxsat_formula->getSoftClause(i).weight);
}
// Otherwise, the soft clause is not relaxed and the assumption is used
// to get an unsat core.
else if (maxsat_formula->getSoftClause(i).weight >= currentWeight)
assumptions.push(~maxsat_formula->getSoftClause(i).assumption_var);
}
if (verbosity > 0)
printf("c Relaxed soft clauses %d / %d\n", objFunction.size(), maxsat_formula->nSoft());
delete solver;
solver = rebuildSolver();
lbCost++;
while (!subsetSum(coeffs, lbCost))
{
lbCost++;
}
if (verbosity > 0) printf("c LB : %-12" PRIu64 "\n", lbCost);
encoder.encodePB(solver, objFunction, coeffs, lbCost);
}
}
return _ERROR_;
}
// Public search method
StatusCode WMSU3::search()
{
if (maxsat_formula->getProblemType() == _UNWEIGHTED_)
{
printf("Error: Currently algorithm WMSU3 does not support unweighted MaxSAT"
" instances.\n");
printf("s UNKNOWN\n");
return _ERROR_;
}
if (bmo_strategy) is_bmo = isBMO();
printConfiguration();
if (!is_bmo) currentWeight = 1; // No weight strategy none.
return WMSU3_none();
}
/************************************************************************************************
//
// Rebuild MaxSAT solver
//
************************************************************************************************/
/*_________________________________________________________________________________________________
|
| rebuildSolver : [void] -> [Solver *]
|
| Description:
|
| Rebuilds a SAT solver with the current MaxSAT formula.
|
|________________________________________________________________________________________________@*/
Solver *WMSU3::rebuildSolver()
{
Solver *S = newSATSolver();
for (int i = 0; i < maxsat_formula->nVars(); i++)
newSATVariable(S);
for (int i = 0; i < maxsat_formula->nHard(); i++)
S->addClause(maxsat_formula->getHardClause(i).clause);
vec<Lit> clause;
for (int i = 0; i < maxsat_formula->nSoft(); i++)
{
clause.clear();
maxsat_formula->getSoftClause(i).clause.copyTo(clause);
for (int j = 0; j < maxsat_formula->getSoftClause(i).relaxation_vars.size(); j++)
clause.push(maxsat_formula->getSoftClause(i).relaxation_vars[j]);
S->addClause(clause);
}
return S;
}
/************************************************************************************************
//
// Other protected methods
//
************************************************************************************************/
/*_________________________________________________________________________________________________
|
| initRelaxation : [void] -> [void]
|
| Description:
|
| Initializes the relaxation variables by adding a fresh variable to the
| 'relaxationVars' of each soft clause.
|
| Post-conditions:
| * 'objFunction' contains all relaxation variables that were added to soft
| clauses.
|
|________________________________________________________________________________________________@*/
void WMSU3::initRelaxation()
{
for (int i = 0; i < maxsat_formula->nSoft(); i++)
{
Lit l = maxsat_formula->newLiteral();
maxsat_formula->getSoftClause(i).relaxation_vars.push(l);
maxsat_formula->getSoftClause(i).assumption_var = l;
}
}
// Returns true if there is a subset of set[] with sum equal to given sum
bool WMSU3::subsetSum(vec<uint64_t> &set, int64_t sum)
{
int n = set.size();
// Declaring the array dynamically to avoid stack frame limit
bool ** subset = new bool*[sum+1];
for (int i = 0; i <= sum; i++)
subset[i] = new bool[n+1];
// The value of subset[i][j] will be true if there is a subset of set[0..j-1]
// with sum equal to i
// If sum is 0, then answer is true
for (int i = 0; i <= n; i++)
{
//assert (i < n+1);
//printf("i %d\n",i);
subset[0][i] = true;
}
// If sum is not 0 and set is empty, then answer is false
for (int i = 1; i <= sum; i++)
subset[i][0] = false;
// Fill the subset table in bottom up manner
for (int i = 1; i <= sum; i++)
{
for (int j = 1; j <= n; j++)
{
subset[i][j] = subset[i][j - 1];
if (i >= set[j - 1])
subset[i][j] = subset[i][j] || subset[i - set[j - 1]][j - 1];
}
}
bool is_subset = subset[sum][n];
for (int i = 0; i <= sum; i++)
delete [] subset[i];
delete [] subset;
return is_subset;
}
// Print WSMU3 configuration.
void WMSU3::print_WMSU3_configuration()
{
if (is_bmo)
{
if (bmo_strategy)
printf("c | BMO strategy: %20s "
" |\n",
"On");
else
printf("c | BMO strategy: %20s "
" |\n",
"Off");
printf("c | BMO search: %22s "
" |\n",
"Yes");
print_Card_configuration(encoder.getCardEncoding());
}
else
{
if (bmo_strategy)
printf("c | BMO strategy: %20s "
" |\n",
"On");
else
printf("c | BMO strategy: %20s "
" |\n",
"Off");
printf("c | BMO search: %22s "
" |\n",
"No");
print_PB_configuration(encoder.getPBEncoding());
}
}
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...