From b0d16316c2182caf19c64dc9e7addb5224d6d568 Mon Sep 17 00:00:00 2001
From: Andrew Haberlandt <andrew.haberlandt@gmail.com>
Date: Sun, 25 Feb 2024 16:08:36 -0500
Subject: [PATCH] Add -c to preserve model count

This is experimental and untested. (see #3)
---
 sbva.cc    | 36 +++++++++++++++++++++++++++++++++---
 wrapper.py |  8 +++++++-
 2 files changed, 40 insertions(+), 4 deletions(-)

diff --git a/sbva.cc b/sbva.cc
index dd3f3c7..7cc7e13 100644
--- a/sbva.cc
+++ b/sbva.cc
@@ -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;
@@ -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) {
@@ -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]);
@@ -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) {
@@ -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");
@@ -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;
diff --git a/wrapper.py b/wrapper.py
index dfad6a4..2b80a13 100644
--- a/wrapper.py
+++ b/wrapper.py
@@ -67,6 +67,10 @@ 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,
@@ -74,10 +78,11 @@ def run(args):
             '-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
@@ -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)