Skip to content

Commit

Permalink
2020 evaluation version
Browse files Browse the repository at this point in the history
  • Loading branch information
@fbacchus
fbacchus committed Jan 12, 2022
1 parent 415a6e2 commit de5f7c2
Show file tree
Hide file tree
Showing 62 changed files with 11,171 additions and 7,790 deletions.
8 changes: 4 additions & 4 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ LINUX_CPLEXLIBDIR ?= /w/63/fbacchus/CPLEX_Studio1210/cplex/lib/x86-64_linux/st
LINUX_CPLEXINCDIR ?= /w/63/fbacchus/CPLEX_Studio1210/cplex/include
#
#If you want to build on macos
DARWIN_CPLEXLIBDIR ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio128/cplex/lib/x86-64_osx/static_pic/
DARWIN_CPLEXINCDIR ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio128/cplex/include
DARWIN_CPLEXLIBDIR ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio1210/cplex/lib/x86-64_osx/static_pic/
DARWIN_CPLEXINCDIR ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio1210/cplex/include

ifeq "$(shell uname)" "Linux"
CPLEXLIBDIR =$(LINUX_CPLEXLIBDIR)
Expand All @@ -30,7 +30,7 @@ endif
BUILD_DIR ?= build

# Include debug-symbols in release builds?
MAXHS_RELSYM ?= -g
#MAXHS_RELSYM ?= -g

# Sat solver you can use minisat of glucose. minisat is faster.for maxhs
SATSOLVER = minisat
Expand Down Expand Up @@ -100,7 +100,7 @@ $(BUILD_DIR)/profile/%.o: MAXHS_CXXFLAGS +=$(MAXHS_PRF) -pg
## Build-type Link-flags:
$(BUILD_DIR)/profile/bin/$(MAXHS): MAXHS_LDFLAGS += -pg
ifeq "$(shell uname)" "Linux"
$(BUILD_DIR)/release/bin/$(MAXHS): MAXHS_LDFLAGS += -z muldefs
$(BUILD_DIR)/release/bin/$(MAXHS): MAXHS_LDFLAGS += --static -z muldefs
endif
$(BUILD_DIR)/release/bin/$(MAXHS): MAXHS_LDFLAGS += $(MAXHS_RELSYM)

Expand Down
185 changes: 127 additions & 58 deletions maxhs/core/Assumptions.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,96 +21,165 @@ 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 "maxhs/core/Assumptions.h"
#include "maxhs/core/Bvars.h"
#include "maxhs/core/TotalizerManager.h"
#include "maxhs/utils/Params.h"

#ifdef GLUCOSE
namespace Minisat = Glucose;
#endif

using Minisat::l_True;
using Minisat::l_False;
using Minisat::l_True;
using Minisat::l_Undef;
using Minisat::lbool;
using Minisat::Lit;
using Minisat::lit_Undef;
using Minisat::var;

Assumps::Assumps(MaxHS_Iface::SatSolver* s, Bvars& b, TotalizerManager* t)
: satsolver{s}, bvars(b), totalizers{t}, map(bvars.maxvar() + 1, -1) {}

void Assumps::init(const vector<Lit>& ivals, CoreType coreType) {
//initialize assumptions with set of b-lits. coreType determines
//what kind of conflicts we are looking for. If looking for cores,
//add only noncore vars (conflict will be negation == core), etc.

assumps.clear();
for(auto l : ivals) {
assert(bvars.isBvar(l));
if(satsolver->curVal(l) != l_True)
//Don't need true lits in assumption.
switch(coreType) {
case CoreType::cores:
if(bvars.isNonCore(l))
assumps.push_back(l);
break;
case CoreType::nonCores:
if(bvars.isCore(l))
assumps.push_back(l);
break;
case CoreType::mixed:
assumps.push_back(l);
}
if (satsolver->curVal(l) == l_False)
cout << "c WARNING assumptions being initialized with false lit\n";
}
setMap();
void Assumps::init(vector<Lit> lits) {
// initialize assumptions with set of b-lits. coreType determines
// what kind of conflicts we are looking for. If looking for cores,
// add only noncore vars (conflict will be negation == core), etc.
assumps = std::move(lits);
if (params.verbosity > 1)
cout << "c Init assumptions with " << assumps.size() << "lits\n";
// cout << "size of assumps: " << assumps.size() << "\n";
// printAssumps();
setMap();
// printMap();
}

void Assumps::all_softs_true() {
//harden all softs not yet forced.
// harden all softs not yet forced.
assumps.clear();
for(size_t i = 0; i < bvars.n_bvars(); i++)
if(satsolver->curVal(bvars.varOfCls(i)) == l_Undef)
for (size_t i = 0; i < bvars.n_bvars(); i++)
if (satsolver->curVal(bvars.varOfCls(i)) == l_Undef)
assumps.push_back(~bvars.litOfCls(i));
setMap();
}


void Assumps::permute() {
std::random_shuffle(assumps.begin(), assumps.end());
setMap();
}

void Assumps::exclude(const vector<Lit>& ex) {
//Unlike update exclude removes the lits without regard for its polarity.
for(auto l : ex)
if(getIndex(l) >= 0)
assumps[getIndex(l)] = lit_Undef;
auto isUndef = [](Lit l) { return l == lit_Undef; };
auto p = std::remove_if(assumps.begin(), assumps.end(), isUndef);
assumps.erase(p, assumps.end());
// Unlike update exclude removes the lits without regard for its polarity.
for (auto l : ex)
if (getIndex(l) >= 0) assumps[getIndex(l)] = lit_Undef;
removeUndefs();
setMap();
}

void Assumps::update(const vector<Lit>& conflict, bool rm) {
//Update assumptions with set of literals in conflict. Flip
//flip the assumptions--if using Fb or remove the assumptions if
//using Fbeq
if(rm)
// Update assumptions with set of literals in conflict. Flip
// flip the assumptions--if using Fb or remove the assumptions if
// using Fbeq
if (rm)
remove(conflict);
else
flip(conflict);
}

void Assumps::flip(const vector<Lit>& conflict) {
//conflict variables must be in assumps. Update assumptions to agree
//with conflict.
for(auto l : conflict) {
checkUpdate(l);
if(assumps[getIndex(l)] == l)
cout << "c WARNING conflict agrees with assumption---no real update in flip assumptions\n";
assumps[getIndex(l)] = l;
// conflict variables must be in assumps. Update assumptions to agree
// with conflict.
for (auto l : conflict) {
if (checkUpdate(l)) {
if (assumps[getIndex(l)] == l)
cout << "c WARNING conflict agrees with assumption---no real update in "
"flip assumptions\n";
assumps[getIndex(l)] = l;
}
}
}

void Assumps::remove(const vector<Lit>& conflict) {
//conflict variables must be in assumps.
//perserve order of assumps.
for(auto l : conflict)
if(checkUpdate(l))
assumps[getIndex(l)] = lit_Undef;
// conflict variables must be in assumps.
// perserve order of assumps.
if(params.abstract_assumps == 0) {
for (auto l : conflict)
if (checkUpdate(l))
assumps[getIndex(l)] = lit_Undef;
}
else if(params.abstract_assumps == 1) {
for (auto l : conflict)
if (checkUpdate(l)) {
assumps[getIndex(l)] = lit_Undef;
if (totalizers->isToutput(l)) {
Lit ln = totalizers->getNextOLit(l);
if (ln != lit_Undef)
assumps.push_back(~ln); // lit_Undef cannot be negated!
}
}
}
else if(params.abstract_assumps == 2) {
bool tot_relaxed {false};
for (auto l : conflict)
if (checkUpdate(l)) {
if(bvars.isBvar(l))
assumps[getIndex(l)] = lit_Undef;
else if (totalizers->isToutput(l) && !tot_relaxed) {
assumps[getIndex(l)] = lit_Undef;
Lit ln = totalizers->getNextOLit(l);
if (ln != lit_Undef)
assumps.push_back(~ln);
tot_relaxed = true;
}
}
}
removeUndefs();
setMap();
}

void Assumps::clearIndex(Lit l) {
assert(var(l) < static_cast<int>(map.size()));
map[var(l)] = -1;
}

int Assumps::getIndex(Lit l) {
assert(var(l) < static_cast<int>(map.size()));
return map[var(l)];
}

bool Assumps::removeUndefs() {
auto isUndef = [](Lit l) { return l == lit_Undef; };
auto p = std::remove_if(assumps.begin(), assumps.end(), isUndef);
assumps.erase(p, assumps.end());
setMap();
if(p != assumps.end()) {
assumps.erase(p, assumps.end());
return true;
}
return false;
}

void Assumps::setMap() {
std::fill(map.begin(), map.end(), -1);
for (size_t i = 0; i < assumps.size(); i++) {
if (static_cast<size_t>(var(assumps[i])) > map.size())
map.resize(var(assumps[i]) + 1, -1);
map[var(assumps[i])] = i;
}
}

void Assumps::printMap() {
for (size_t i = 0; i < map.size(); i++)
std::cout << "a map[" << i << "] = " << map[i] << "\n";
}

bool Assumps::checkUpdate(Lit l) {
if (getIndex(l) < 0) {
cout << "c ERROR tried to update literal not in assumptions: " << l
<< " to int: " << toInt(l) << "\n";
if (totalizers->isToutput(l))
cout << "c ERROR " << l << " is totalizer output\n";
return false;
}
return true;
}

void Assumps::printAssumps() { cout << "c assumps:\n" << assumps << "\n"; }
102 changes: 45 additions & 57 deletions maxhs/core/Assumptions.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,80 +25,68 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
#ifndef ASSUMPTIONS_h
#define ASSUMPTIONS_h

#include <vector>
#include <algorithm>
#include "maxhs/ifaces/SatSolver.h"
#include "maxhs/core/Wcnf.h"
#include "maxhs/core/Bvars.h"
#include "maxhs/utils/io.h"
#include <vector>

#include "maxhs/core/MaxSolverTypes.h"
#include "maxhs/ifaces/SatSolver.h"

#ifdef GLUCOSE
namespace Minisat = Glucose;
#endif
class Bvars;
class TotalizerManager;

using Minisat::Lit;
using Minisat::var;
using Minisat::lbool;
namespace MaxHS_Iface {
class Cplex;
class SatSolver;
} // namespace MaxHS_Iface

using std::vector;

class Assumps {
//MaxSolver helper class
public:
Assumps(MaxHS_Iface::SatSolver* s, Bvars& b) : satsolver{s}, bvars (b) {
map.resize(bvars.n_bvars(), -1); }
~Assumps() {}
//initialize assumptions to make all softs true, or set of passed softs
void init(const vector<Lit>& ivals, CoreType ctype);
// MaxSolver helper class
public:
Assumps(MaxHS_Iface::SatSolver* s, Bvars& b, TotalizerManager* t);
// initialize assumptions to make all softs true, or set of passed softs
void init(vector<Minisat::Lit> lits);
void all_softs_true();
void permute();

//update requires that lits in conflict currently appear negated in
//assumptions Warns this is not the case.
//exclude ensures these variables corresponding to these lits are
//not part of assumption
void update(const vector<Lit>& conflict, bool remove);
void exclude(const vector<Lit>& ex);

const vector<Lit>& vec() const { return assumps; }
// update requires that lits in conflict currently appear negated in
// assumptions Warns this is not the case.
// exclude ensures these variables corresponding to these lits are
// not part of assumption
void exclude(const vector<Minisat::Lit>& ex);
void update(const vector<Minisat::Lit>& conflict, bool remove);
const vector<Minisat::Lit>& vec() const { return assumps; }
template <class Compare>
void sort(Compare comp) {
void sort(Compare comp) {
std::sort(assumps.begin(), assumps.end(), comp);
setMap();
}
friend ostream& operator<<(ostream& os, const Assumps& a);
friend std::ostream& operator<<(std::ostream& os, const Assumps& a);

private:
vector<Lit> assumps;
vector<int> map;
private:
MaxHS_Iface::SatSolver* satsolver;
Bvars& bvars;
// const uint8_t inMxdvar = 2;
// const uint8_t inMxbvar = 1;
// vector<uint8_t>& inMx;
//
void remove(const vector<Lit>& conflict);
void flip(const vector<Lit>& conflict);
void clearIndex(Lit l) {
map[bvars.toIndex(var(l))] = -1;
}
int getIndex(Lit l) {
return map[bvars.toIndex(var(l))];
}
void setMap() {
std::fill(map.begin(), map.end(), -1);
for(size_t i = 0; i < assumps.size(); i++)
map[bvars.toIndex(var(assumps[i]))] = i;
}
bool checkUpdate(Lit l) {
if(getIndex(l) < 0) {
cout << "c ERROR tried to update literal not in assumptions\n";
return false;
}
return true;
}
TotalizerManager* totalizers;
vector<Minisat::Lit> assumps;
vector<int> map;
vector<int> tot_index;
vector<int> counts;
vector<int> coeff;
void flip(const vector<Minisat::Lit>& conflict);
void remove(const vector<Minisat::Lit>& conflict);

void clearIndex(Minisat::Lit l);
int getIndex(Minisat::Lit l);
bool removeUndefs();
void setMap();
void printMap();
bool checkUpdate(Minisat::Lit l);
void printAssumps();
};

inline ostream& operator<<(ostream& os, const Assumps& a) {
os << a.assumps;
inline std::ostream& operator<<(std::ostream& os, const Assumps& a) {
os << "Assumps" << a.assumps;
return os;
}

Expand Down
Loading

0 comments on commit de5f7c2

Please sign in to comment.