Skip to content

Commit

Permalink
Add -c to preserve model count
Browse files Browse the repository at this point in the history
This is experimental and untested. (see #3)
  • Loading branch information
ndrewh committed Feb 29, 2024
1 parent 06ead46 commit 22668af
Show file tree
Hide file tree
Showing 2 changed files with 40 additions and 4 deletions.
36 changes: 33 additions & 3 deletions sbva.cc
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ using namespace std;

static bool enable_trace = 0;
static bool generate_proof = 0;
static bool preserve_model_count = 0;

static time_t end_time = 0;
static unsigned int max_replacements = 0;
Expand Down Expand Up @@ -682,7 +683,7 @@ class Formula {
int new_var = num_vars;

// Prepare to add new clauses.
clauses->resize(num_clauses + matched_lit_count + matched_clause_count);
clauses->resize(num_clauses + matched_lit_count + matched_clause_count + (preserve_model_count ? 1 : 0));
lit_to_clauses->resize(num_vars * 2);
lit_count_adjust->resize(num_vars * 2);
if (sparsevec_lit_idx(new_var) >= adjacency_matrix_width) {
Expand Down Expand Up @@ -739,6 +740,32 @@ class Formula {
}
}

// Preserving model count:
//
// The only case where we add a model is if both assignments for the auxiiliary variable satisfy the formula
// for the same assignment of the original variables. This only happens if all(matched_lits) *AND*
// all(matches_clauses) are satisfied.
//
// The easiest way to fix this is to add one clause that constrains all(matched_lits) => -f
if (preserve_model_count) {
int new_clause = num_clauses + matched_lit_count + matched_clause_count;
auto cls = Clause();
cls.lits.push_back(-new_var);
for (int i = 0; i < matched_lit_count; ++i) {
int lit = (*matched_lits)[i];
cls.lits.push_back(-lit);
(*lit_to_clauses)[lit_index(-lit)].push_back(new_clause);
}

(*clauses)[new_clause] = cls;
(*lit_to_clauses)[(lit_index(-new_var))].push_back(new_clause);

if (generate_proof) {
proof->push_back(ProofClause(true, cls.lits));
}
}


set<int> valid_clause_ids;
for (int i = 0; i < matched_clause_count; ++i) {
valid_clause_ids.insert((*matched_clauses_id)[i]);
Expand Down Expand Up @@ -770,7 +797,7 @@ class Formula {
}

adj_deleted += removed_clause_count;
num_clauses += matched_lit_count + matched_clause_count;
num_clauses += matched_lit_count + matched_clause_count + (preserve_model_count ? 1 : 0);

// Update priorities.
for (auto lit : lits_to_update) {
Expand Down Expand Up @@ -844,7 +871,7 @@ int main(int argc, char **argv) {
Tiebreak tiebreak = Tiebreak::ThreeHop;

int opt;
while ((opt = getopt(argc, argv, "p:i:o:t:s:vn")) != -1) {
while ((opt = getopt(argc, argv, "p:i:o:t:s:vnc")) != -1) {
switch (opt) {
case 'i':
fin = fopen(optarg, "r");
Expand Down Expand Up @@ -880,6 +907,9 @@ int main(int argc, char **argv) {
case 'n':
tiebreak = Tiebreak::None;
break;
case 'c':
preserve_model_count = true;
break;
default:
fprintf(stderr, "Usage: %s [-i input] [-o output]\n", argv[0]);
return 1;
Expand Down
8 changes: 7 additions & 1 deletion wrapper.py
Original file line number Diff line number Diff line change
Expand Up @@ -67,17 +67,22 @@ def run_solver_reduced(args, reduced_cnf, reduced_drat):

def run(args):
with NamedTemporaryFile() as bva_cnf, NamedTemporaryFile() as bva_drat:
extra_args = []
if args.preserve_model_count:
extra_args += ["-c"]

# Run BVA
p = subprocess.run([
'timeout', str(args.t2), args.bva,
'-i', args.input,
'-o', bva_cnf.name,
'-p', bva_drat.name,
'-t', str(args.t1),
])
] + extra_args)

if p.returncode == 0:
# BVA ran successfully
nv, nc = find_stats(bva_cnf.name)
run_solver_reduced(args, bva_cnf.name, bva_drat.name)
else:
# Run original solver on input
Expand All @@ -89,6 +94,7 @@ def run(args):
parser.add_argument('-i', '--input', type=str, required=True)
parser.add_argument('-o', '--output', type=str, required=True)
parser.add_argument('--bva', type=str, required=True)
parser.add_argument('--preserve-model-count', action="store_true", default=False)
parser.add_argument('--t1', type=int, help='Inner timeout', required=True)
parser.add_argument('--t2', type=int, help='Outer timeout', required=True)
parser.add_argument('--solver', type=str, required=True)
Expand Down

0 comments on commit 22668af

Please sign in to comment.