Skip to content

Commit

Permalink
WIP: Short Prepro
Browse files Browse the repository at this point in the history
  • Loading branch information
@BenKaufmann
BenKaufmann committed Dec 17, 2024
1 parent c9fa8b7 commit b0b87c4
Show file tree
Hide file tree
Showing 5 changed files with 126 additions and 6 deletions.
4 changes: 2 additions & 2 deletions clasp/cli/clasp_cli_options.inl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,9 +104,9 @@ OPTION(share, "!,@1", ARG_EXT(defaultsTo("auto")->state(Value::value_defaulted),
" %A: {auto|problem|learnt|all}", FUN(arg) {ContextParams::ShareMode x; return arg>>x && SET(SELF.shareMode, (uint32)x);}, GET((ContextParams::ShareMode)SELF.shareMode))
OPTION(learn_explicit, ",@2" , ARG(flag()), "Do not use Short Implication Graph for learning", STORE_FLAG(SELF.shortMode), GET(SELF.shortMode))
OPTION(short_simp_mode, ",@2" , ARG_EXT(arg("<mode>")->defaultsTo("no")->state(Value::value_defaulted), DEFINE_ENUM_MAPPING(ContextParams::ShortSimpMode, \
MAP("no" , ContextParams::simp_no) , MAP("learnt", ContextParams::simp_learnt))),\
MAP("no" , ContextParams::simp_no), MAP("learnt", ContextParams::simp_learnt), MAP("all", ContextParams::simp_all))),\
"Remove duplicate short constraints [%D]\n"\
" %A: {no|learnt}", FUN(arg) {ContextParams::ShortSimpMode x; return arg>>x && SET(SELF.shortSimp, (uint32)x);}\
" %A: {no|learnt|all}", FUN(arg) {ContextParams::ShortSimpMode x; return arg>>x && SET(SELF.shortSimp, (uint32)x);}\
, GET((ContextParams::ShortSimpMode)SELF.shortSimp))\
OPTION(sat_prepro , "!,@1", ARG(arg("<arg>")->implicit("2")), \
"Run SatELite-like preprocessing (Implicit: %I)\n" \
Expand Down
6 changes: 6 additions & 0 deletions clasp/shared_context.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,11 @@ class ShortImplicationsGraph {
* \return true iff a new implication was added.
*/
bool add(LitView lits, bool learnt);
//! Removes the given constraint from the implication graph.
/*!
* \pre The object is currently not shared.
*/
void remove(LitView lits, bool learnt);

//! Removes p and its implications.
/*!
Expand Down Expand Up @@ -975,6 +980,7 @@ class SharedContext {
[[nodiscard]] MinPtr minimizeNoCreate() const;
//@}
private:
bool preprocessShort();
bool unfreezeStep();
Literal addStepLit();
using VarVec = PodVector_t<VarInfo>;
Expand Down
1 change: 1 addition & 0 deletions clasp/solver_strategies.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -585,6 +585,7 @@ struct ContextParams {
enum ShortSimpMode {
simp_no = 0, /*!< No additional simplifications. */
simp_learnt = 1, /*!< Drop duplicate learnt short clauses. */
simp_all = 2, /*!< Drop all duplicate short clauses. */
};
//! How to handle physical sharing of (explicit) constraints.
enum ShareMode {
Expand Down
118 changes: 115 additions & 3 deletions src/shared_context.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ bool ShortImplicationsGraph::add(LitView lits, bool learnt) {
Literal p = lits[0], q = lits[1], r = (tern ? lits[2] : lit_false);
p.unflag(), q.unflag(), r.unflag();
if (not shared_) {
bool simp = learnt && simp_ == ContextParams::simp_learnt;
bool simp = simp_ == ContextParams::simp_all || (learnt && simp_ == ContextParams::simp_learnt);
if (simp && contains(getList(~p).left_view(), q)) {
return true;
}
Expand Down Expand Up @@ -241,6 +241,31 @@ bool ShortImplicationsGraph::add(LitView lits, bool learnt) {
#endif
return false;
}
void ShortImplicationsGraph::remove(LitView lits, bool learnt) {
assert(not shared_);
bool tern = lits.size() == 3u;
uint32& stats = (tern ? tern_ : bin_)[learnt];
unsigned i = 0, rem = 0;
for (auto x : lits) {
auto& w = getList(~x);
auto sz = w.left_size() + w.right_size();
if (not tern) {
w.erase_left_unordered(std::find(w.left_begin(), w.left_end(), lits[1 - i]));
}
else {
Tern t = {lits[(i + 1) % 3], lits[(i + 2) % 3]};
w.erase_right_unordered(std::find_if(w.right_begin(), w.right_end(), [&t](const Tern& e) {
return contains(t, e[0]) && contains(t, e[1]);
}));
}
rem += sz != (w.left_size() + w.right_size());
w.try_shrink();
++i;
}
if (rem) {
--stats;
}
}

void ShortImplicationsGraph::removeBin(Literal other, Literal sat) {
--bin_[other.flagged()];
Expand Down Expand Up @@ -1023,8 +1048,11 @@ bool SharedContext::endInit(bool attachAll) {
initStats(*master());
heuristic.simplify();
SatPrePtr temp = std::move(satPrepro);
bool ok = not master()->hasConflict() && master()->preparePost() && (not temp || temp->preprocess(*this)) &&
master()->endInit();
bool ok = not master()->hasConflict() && master()->preparePost() && (not temp || temp->preprocess(*this));
if (ok && not temp && btig_.simpMode() == ContextParams::simp_all) {
ok = preprocessShort();
}
ok = ok && master()->endInit();
satPrepro = std::move(temp);
master()->dbIdx_ = sizeVec(master()->constraints_);
lastTopLevel_ = master()->assign_.front;
Expand Down Expand Up @@ -1207,6 +1235,90 @@ uint32 SharedContext::problemComplexity() const {
}
return numConstraints();
}
bool SharedContext::preprocessShort() {
auto& s = *master();
auto& assign = s.assign_;
LitVec lits;
LitVec tern;
for (Var v = 1; v < assign.numVars() && not s.hasConflict(); ++v) {
if (assign.value(v) != value_free) {
continue;
}
for (Literal lit : {posLit(v), negLit(v)}) {
if (marked(lit)) {
continue;
}
tern.clear();
bool ok = true;
auto qFront = assign.assigned();
assign.assign(lit, 0, lit_true);
do {
ok = btig_.forEach(assign.trail[qFront++], [&](Literal p, Literal q, Literal r = lit_false) {
if (r == lit_false) {
return assign.assign(q, 0, p);
}
auto vq = assign.value(q.var());
auto vr = assign.value(r.var());
auto ante = Antecedent(p);
if (vr == trueValue(r) || vq == trueValue(q)) {
if (assign.reason(r.var()).asUint() == ante.asUint() ||
assign.reason(q.var()).asUint() == ante.asUint()) {
tern.push_back(~p);
tern.push_back(q);
tern.push_back(r);
}
return true;
}
if (vr == vq) {
return vr == value_free;
}
if (vq) {
if (assign.reason(q.var()).asUint() == ante.asUint()) {
tern.push_back(q.flag());
tern.push_back(~p);
tern.push_back(r);
}
return assign.assign(r, 0, Antecedent(p, ~q));
}
if (assign.reason(r.var()).asUint() == ante.asUint()) {
tern.push_back(r.flag());
tern.push_back(~p);
tern.push_back(q);
}
return assign.assign(q, 0, Antecedent(p, ~r));
});
} while (ok && qFront < assign.assigned());
if (ok) {
for (auto i = 0u; i < sizeVec(tern); i += 3) {
bool sat = not tern[i].flagged();
bool learnt = tern[i + 1].flagged() || tern[i + 2].flagged();
tern[i].unflag();
btig_.remove(std::span(tern.data() + i, 3), learnt);
if (not sat) {
btig_.add(std::span(tern.data() + i + 1, 2), learnt);
}
}
}
while (assign.trail.back() != lit) {
if (not marked(assign.trail.back())) {
mark(assign.trail.back());
lits.push_back(assign.trail.back());
}
assign.undoLast();
}
assign.undoLast();
if (not ok) {
master()->force(~lit) && master()->propagate();
break;
}
}
}
while (not lits.empty()) {
unmark(lits.back().var());
lits.pop_back();
}
return master()->simplify();
}
/////////////////////////////////////////////////////////////////////////////////////////
// Distributor
/////////////////////////////////////////////////////////////////////////////////////////
Expand Down
3 changes: 2 additions & 1 deletion tests/cli_test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -458,7 +458,8 @@ TEST_CASE("Cli options", "[cli]") {
REQUIRE(config.getValue(key, val) == 2);
REQUIRE(val == "no");

for (auto [x, y] : {std::pair{ContextParams::simp_learnt, "learnt"}, std::pair{ContextParams::simp_no, "no"}}) {
for (auto [x, y] : {std::pair{ContextParams::simp_learnt, "learnt"}, std::pair{ContextParams::simp_all, "all"},
std::pair{ContextParams::simp_no, "no"}}) {
CAPTURE(y);
REQUIRE(1 == config.setValue(key, y));
REQUIRE(config.shortSimp == x);
Expand Down

0 comments on commit b0b87c4

Please sign in to comment.