diff --git a/src/main.cpp b/src/main.cpp index 1b1163a..f1a0fca 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -83,6 +83,12 @@ int main(int argc, char **argv) { .action([&](const auto&) {tiebreak = Tiebreak::None;}) .flag() .help("Use original BVA tie-break. Runs BVA instead of SBVA"); + program.add_argument("--clscutoff") + .action([&](const auto& a) {config.matched_cls_cutoff = std::atoi(a.c_str());}) + .help("Matched clauses cutoff. The larger, the larger the gain must be to perform BVA"); + program.add_argument("--litscutoff") + .action([&](const auto& a) {config.matched_lits_cutoff = std::atoi(a.c_str());}) + .help("Matched literals cutoff. The larger, the larger the gain must be to perform BVA"); program.add_argument("-c", "--countpreserve") .action([&](const auto&) {config.preserve_model_cnt = true;}) .flag() diff --git a/src/sbva.cpp b/src/sbva.cpp index 45d67cd..fbeaa75 100644 --- a/src/sbva.cpp +++ b/src/sbva.cpp @@ -730,7 +730,8 @@ class Formula { continue; } - if (matched_lits.size() <= 2 && matched_clauses.size() <= 2) { + if (matched_lits.size() <= config.matched_lits_cutoff && + matched_clauses.size() <= config.matched_cls_cutoff) { continue; } diff --git a/src/sbva.h b/src/sbva.h index b3fcd11..4c8fc91 100644 --- a/src/sbva.h +++ b/src/sbva.h @@ -39,6 +39,8 @@ struct Config { int64_t steps = std::numeric_limits::max(); unsigned int max_replacements = 0; bool preserve_model_cnt = 0; + uint32_t matched_lits_cutoff = 2; // the larger, the more strict + uint32_t matched_cls_cutoff = 2; // the larger, the more strict }; enum Tiebreak {