/*!
* \author Ruben Martins - rubenm@andrew.cmu.edu
*
* @section LICENSE
*
* MiniSat, Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
* Copyright (c) 2007-2010, Niklas Sorensson
* 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 "utils/Options.h"
#include "utils/ParseUtils.h"
#include "utils/System.h"
#include <errno.h>
#include <signal.h>
#include <zlib.h>
#include <fstream>
#include <iostream>
#include <map>
#include <stdlib.h>
#include <string>
#include <vector>
#include "core/Solver.h"
#include "MaxSAT.h"
#include "MaxTypes.h"
#include "ParserMaxSAT.h"
#include "ParserPB.h"
#include "ParserPartitions.h"
#include "MaxSAT_Partition.h"
// Algorithms
#include "algorithms/Alg_MSU3.h"
#include "algorithms/Alg_OLL.h"
#include "algorithms/Alg_WBO.h"
#include "algorithms/Alg_UpOLL.h"
#include "algorithms/Alg_UpMSU3.h"
#include "algorithms/Alg_UpWBO.h"
#include "algorithms/Alg_WMSU3.h"
#include "algorithms/Alg_UpWMSU3.h"
#define VER1_(x) #x
#define VER_(x) VER1_(x)
#define SATVER VER_(SOLVERNAME)
#define VER VER_(VERSION)
using NSPACE::cpuTime;
using NSPACE::OutOfMemoryException;
using NSPACE::IntOption;
using NSPACE::BoolOption;
using NSPACE::StringOption;
using NSPACE::IntRange;
using NSPACE::parseOptions;
using namespace upmax;
//=================================================================================================
static MaxSAT *mxsolver;
static void SIGINT_exit(int signum) {
mxsolver->printAnswer(_UNKNOWN_);
exit(_UNKNOWN_);
}
//=================================================================================================
#if !defined(_MSC_VER) && !defined(__MINGW32__)
void limitMemory(uint64_t max_mem_mb)
{
// FIXME: OpenBSD does not support RLIMIT_AS. Not sure how well RLIMIT_DATA works instead.
#if defined(__OpenBSD__)
#define RLIMIT_AS RLIMIT_DATA
#endif
// Set limit on virtual memory:
if (max_mem_mb != 0){
rlim_t new_mem_lim = (rlim_t)max_mem_mb * 1024*1024;
rlimit rl;
getrlimit(RLIMIT_AS, &rl);
if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
rl.rlim_cur = new_mem_lim;
if (setrlimit(RLIMIT_AS, &rl) == -1)
printf("c WARNING! Could not set resource limit: Virtual memory.\n");
}
}
#if defined(__OpenBSD__)
#undef RLIMIT_AS
#endif
}
#else
void limitMemory(uint64_t /*max_mem_mb*/)
{
printf("c WARNING! Memory limit not supported on this architecture.\n");
}
#endif
#if !defined(_MSC_VER) && !defined(__MINGW32__)
void limitTime(uint32_t max_cpu_time)
{
if (max_cpu_time != 0){
rlimit rl;
getrlimit(RLIMIT_CPU, &rl);
if (rl.rlim_max == RLIM_INFINITY || (rlim_t)max_cpu_time < rl.rlim_max){
rl.rlim_cur = max_cpu_time;
if (setrlimit(RLIMIT_CPU, &rl) == -1)
printf("c WARNING! Could not set resource limit: CPU-time.\n");
}
}
}
#else
void limitTime(uint32_t /*max_cpu_time*/)
{
printf("c WARNING! CPU-time limit not supported on this architecture.\n");
}
#endif
//=================================================================================================
// Main:
int main(int argc, char **argv) {
printf(
"c\nc UpMax:\t User partitioning for MaxSAT -- based on %s (%s version)\n",
SATVER, VER);
printf("c Version:\t October 2022\n");
printf("c Authors:\t Pedro Orvalho, Vasco Manquinho, Ruben Martins\n");
printf("c Contact:\t rubenm@andrew.cmu.edu\n");
try {
NSPACE::setUsageHelp("c USAGE: %s [options] <input-file>\n\n");
#if defined(__linux__)
fpu_control_t oldcw, newcw;
_FPU_GETCW(oldcw);
newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
_FPU_SETCW(newcw);
printf(
"c WARNING: for repeatability, setting FPU to use double precision\n");
#endif
BoolOption allopts("UpMax", "all-opt", "Finds all optimal solutions.\n", false);
BoolOption allvars("UpMax", "all-vars", "Uses all variables to find optimal solutions.\n", false);
BoolOption printmodel("UpMax", "print-model", "Print model.\n", true);
StringOption printsoft("UpMax", "print-unsat-soft", "Print unsatisfied soft claues in the optimal assignment.\n", NULL);
IntOption verbosity("UpMax", "verbosity",
"Verbosity level (0=minimal, 1=more).\n", 0,
IntRange(0, 1));
StringOption json ("UpMax", "json", "JSON search statistics output destination\n", NULL);
IntOption pwcnf_limit("UpMax","limit","Conflict limit for each partition.\n",-1,IntRange(-1,INT32_MAX));
IntOption pwcnf_mode("UpMax","merge","Merge heuristic (0=partition size,1=core size,2=saturation only).\n",0,IntRange(0,2));
IntOption cpu_lim("UpMax", "cpu-lim",
"Limit on CPU time allowed in seconds.\n", 0,
IntRange(0, INT32_MAX));
IntOption mem_lim("UpMax", "mem-lim",
"Limit on memory usage in megabytes.\n", 0,
IntRange(0, INT32_MAX));
BoolOption upmax("UpMax", "upmax", "User partitioning.\n", true);
StringOption upfile("UpMax", "upfile", "PWCNF file with automatic partition.\n", NULL);
BoolOption wcnf("UpMax", "wcnf", "Transform PWCNF in WCNF file.\n", false);
IntOption algorithm("UpMax", "algorithm",
"Search algorithm "
"(0=wbo,1=msu3,2=oll)\n",
1, IntRange(0, 2));
IntOption graph_type("UpMax", "graph-type",
"Graph type (0=vig, 1=cvig, 2=res, 3=random).",
2, IntRange(0, 3));
BoolOption bmo("UpMax", "bmo", "BMO search.\n", true);
IntOption cardinality("Encodings", "cardinality",
"Cardinality encoding (0=cardinality networks, "
"1=totalizer, 2=modulo totalizer).\n",
1, IntRange(0, 2));
IntOption amo("Encodings", "amo", "AMO encoding (0=Ladder).\n", 0,
IntRange(0, 0));
IntOption pb("Encodings", "pb", "PB encoding (0=SWC,1=GTE,2=Adder).\n", 1,
IntRange(0, 2));
IntOption formula("UpMax", "formula",
"Type of formula (0=WCNF, 1=OPB, 2=PWCNF).\n", 0, IntRange(0, 2));
IntOption weight(
"WBO", "weight-strategy",
"Weight strategy (0=none, 1=weight-based, 2=diversity-based).\n", 2,
IntRange(0, 2));
BoolOption symmetry("WBO", "symmetry", "Symmetry breaking.\n", true);
IntOption symmetry_lim(
"WBO", "symmetry-limit",
"Limit on the number of symmetry breaking clauses.\n", 500000,
IntRange(0, INT32_MAX));
parseOptions(argc, argv, true);
// Try to set resource limits:
if (cpu_lim != 0) limitTime(cpu_lim);
if (mem_lim != 0) limitMemory(mem_lim);
double initial_time = cpuTime();
MaxSAT *S = NULL;
signal(SIGXCPU, SIGINT_exit);
signal(SIGTERM, SIGINT_exit);
if (argc == 1) {
printf("c Warning: no filename.\n");
}
gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
if (in == NULL)
printf("c ERROR! Could not open file: %s\n",
argc == 1 ? "<stdin>" : argv[1]),
printf("s UNKNOWN\n"), exit(_ERROR_);
MaxSATFormula *maxsat_formula = new MaxSATFormula();
if ((int)formula == _FORMAT_MAXSAT_) {
parseMaxSATFormula(in, maxsat_formula);
maxsat_formula->setFormat(_FORMAT_MAXSAT_);
} else if ((int)formula == _FORMAT_PB_){
ParserPB *parser_pb = new ParserPB();
parser_pb->parsePBFormula(argv[1], maxsat_formula);
maxsat_formula->setFormat(_FORMAT_PB_);
} else {
parsePwcnfFormula(in, maxsat_formula);
maxsat_formula->setFormat(_FORMAT_PWCNF_);
}
gzclose(in);
printf("c | "
" |\n");
printf("c ========================================[ Problem Statistics "
"]===========================================\n");
printf("c | "
" |\n");
if (maxsat_formula->getFormat() == _FORMAT_MAXSAT_)
printf(
"c | Problem Format: %17s "
" |\n",
"MaxSAT");
else
printf(
"c | Problem Format: %17s "
" |\n",
"PB");
if (maxsat_formula->getProblemType() == _UNWEIGHTED_)
printf("c | Problem Type: %19s "
" |\n",
"Unweighted");
else
printf("c | Problem Type: %19s "
" |\n",
"Weighted");
printf("c | Number of variables: %12d "
" |\n",
maxsat_formula->nVars());
printf("c | Number of hard clauses: %7d "
" |\n",
maxsat_formula->nHard());
printf("c | Number of soft clauses: %7d "
" |\n",
maxsat_formula->nSoft());
printf("c | Number of cardinality: %7d "
" |\n",
maxsat_formula->nCard());
printf("c | Number of PB : %7d "
" |\n",
maxsat_formula->nPB());
double parsed_time = cpuTime();
printf("c | Parse time: %12.2f s "
" |\n",
parsed_time - initial_time);
printf("c | "
" |\n");
if (upfile != NULL){
MaxSAT_Partition * mp = new MaxSAT_Partition();
mp->loadFormula(maxsat_formula);
mp->init();
if (wcnf){
mp->split(PWCNF_MODE);
mp->printPWCNFtoFile((const char *) upfile, wcnf);
} else {
int graphType = graph_type;
if (graphType == 3) {
// random
mp->split(RAND_MODE);
} else mp->split(UNFOLDING_MODE, graphType);
mp->printPWCNFtoFile((const char *) upfile);
}
exit(_UNKNOWN_);
}
switch ((int)algorithm) {
case _ALGORITHM_WBO_:
if (upmax){
S = new UpWBO(verbosity, pwcnf_mode, pwcnf_limit);
} else {
S = new WBO(verbosity, weight, symmetry, symmetry_lim);
}
break;
case _ALGORITHM_MSU3_:
if (upmax){
if(maxsat_formula->getProblemType() == _UNWEIGHTED_)
S = new UpMSU3(verbosity, pwcnf_mode, pwcnf_limit);
else
S = new UpWMSU3(verbosity);
} else {
if(maxsat_formula->getProblemType() == _UNWEIGHTED_)
S = new MSU3(verbosity);
else
S = new WMSU3(verbosity);
}
break;
case _ALGORITHM_OLL_:
if (upmax){
S = new UpOLL(verbosity, pwcnf_mode, pwcnf_limit);
} else {
S = new OLL(verbosity, cardinality);
}
break;
default:
printf("c Error: Invalid MaxSAT algorithm.\n");
printf("s UNKNOWN\n");
exit(_ERROR_);
}
if (S->getMaxSATFormula() == NULL)
S->loadFormula(maxsat_formula);
S->setPrintModel(printmodel);
S->setPrintSoft((const char *)printsoft);
S->setJson((const char *) json);
S->setInitialTime(initial_time);
S->_all_opt_sols = allopts;
S->_all_var_sols = allvars;
mxsolver = S;
mxsolver->setPrint(true);
int ret = (int)mxsolver->search();
delete S;
return ret;
} catch (OutOfMemoryException &) {
sleep(1);
printf("c Error: Out of memory.\n");
printf("s UNKNOWN\n");
exit(_ERROR_);
} catch(MaxSATException &e) {
sleep(1);
printf("c Error: MaxSAT Exception: %s\n", e.getMsg());
printf("s UNKNOWN\n");
exit(_ERROR_);
}
}