From cc02f1631ea4928d1558294596ded0415a8244f9 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 24 May 2026 14:56:03 +0200 Subject: [PATCH 01/10] Update README --- README.md | 48 +++++++++++++++++------------------------------- 1 file changed, 17 insertions(+), 31 deletions(-) diff --git a/README.md b/README.md index dbff06ab..ec0e5faa 100644 --- a/README.md +++ b/README.md @@ -93,6 +93,20 @@ count, i.e. all variables are assumed to be in the projection set. Beware to ALWAYS give the weight of both the literal and its negation or different counters may give different results. +### Accepted header directives + +| Directive | Meaning | +|-----------|---------| +| `c t mc` | Unweighted, unprojected model counting (default) | +| `c t pmc` | Unweighted projected model counting | +| `c t wmc` | Weighted model counting | +| `c t wpmc` / `c t pwmc` | Weighted projected model counting (aliases) | +| `c p show v1 v2 ... 0` | Projection (sampling) set | +| `c p weight L W 0` | Weight `W` for literal `L` (positive or negative integer) | + +`c t wmc` and `c t pwmc` require a weighted field generator (i.e. not +`--mode 0`); otherwise the parser will reject the file. + ## Weights It is _highly_ encouraged to give both the positive and the negative literal's weight, e.g. `1` and `-1`: @@ -199,34 +213,6 @@ The `prec` constructor argument controls the MPFR precision in bits: c = WeightedCounter(prec=256) # 256-bit internal precision ``` -### Building from source - -Build and install into a venv (requires GMP and MPFR: -`apt-get install libgmp-dev libmpfr-dev` / `brew install gmp mpfr`): - -```bash -git clone --recurse-submodules https://github.com/meelgroup/ganak -cd ganak -python -m venv venv -venv/bin/pip install . -``` - -For iterative development (rebuilding only the extension after CMake changes): - -```bash -# Enable the Python extension (only needed once): -cmake -DBUILD_PYTHON_EXTENSION=ON build - -# Rebuild after editing python/src/pyganak.cpp: -cmake --build build --target pyganak -j$(nproc) - -# Run tests: -venv/bin/pip install pytest -PYTHONPATH=build/lib venv/bin/pytest python/tests/ -v -``` - -See `python/README.md` for the full API reference. - ## Using as a Library Ganak can be used as a library. The file `src/example.cpp` gives an example of how to use Ganak as a library. Let's go through it step by step: @@ -248,8 +234,8 @@ how to use Ganak as a library. Let's go through it step by step: Ganak counter(conf, fg); setup_ganak(cnf, counter); - auto cnt = cnf.multiplier_weight->dup(); - if (!cnf.multiplier_weight->is_zero()) *cnt *= *counter.count(); + auto cnt = cnf.get_multiplier_weight()->dup(); + if (!cnf.get_multiplier_weight()->is_zero()) *cnt *= *counter.count(); cout << "count is: " << std::fixed << *cnt << endl; ``` @@ -266,7 +252,7 @@ two systems' counts to get the final count. | Mode | Flag | Field | Weight format example | Notes | |------|------|-------|-----------------------|-------| -| 0 | `--mode 0` | Integer | `c p weight 1 5 0` | Default; supports `--appmct` | +| 0 | `--mode 0` | Integer | _unweighted_ | Default; weights not supported. Supports `--appmct` | | 1 | `--mode 1` | Rational (exact) | `c p weight 1 1/4 0` | No floating-point error | | 2 | `--mode 2` | Complex rational | `c p weight 9 1/2+4i 0` | Must give both parts: `a+bi` or `a-bi` | | 3 | `--mode 3` | Polynomial over rationals | `c p weight 9 1/2*x0+4*x1+2 0` | Requires `--npolyvars N` | From f311d70ad87ae562c4bb44244b0c8a6614580b86 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 24 May 2026 15:22:08 +0200 Subject: [PATCH 02/10] Clean up mode 8 --- src/main.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main.cpp b/src/main.cpp index 4da23b96..a4adb1b2 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -499,7 +499,7 @@ void run_weighted_counter(Ganak& counter, const ArjunNS::SimplifiedCNF& cnf, con if (!cnt->is_zero()) cout << "s SATISFIABLE" << endl; else cout << "s UNSATISFIABLE" << endl; - if (mode == 0 || mode == 1 || mode == 2 || mode == 6 || mode == 7 || mode == 8) { + if (mode == 0 || mode == 1 || mode == 2 || mode == 6 || mode == 7) { std::stringstream ss; ss << std::scientific << setprecision(40); const CMSat::Field* ptr = cnt.get(); From 5a1731c3789e0c270d5e9e80d8ac1d7e1fabe429 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 24 May 2026 22:33:37 +0200 Subject: [PATCH 03/10] Filter preproc chart aggregators by depth=0; carry depth through schema CMS now emits a per-step nesting depth on each [simp-stats] line. Steps emitted inside an outer wrapper (e.g. must-renumber dispatched from oracle-vivif-veryfast) get depth>=1 and would double-count if summed alongside their depth=0 parent. - get_data_ganak.py: extend _SIMP_STATS_RE to capture the optional "depth N" suffix; key pending BEFOREs on (name, depth) with LIFO popping so same-name nesting matches correctly; add depth to the record/CSV/sqlite preproc schema (defaulting to 0 for older logs). - create_graphs_ganak.py: add "AND depth = 0" to every preproc chart aggregator so totals reflect only top-level steps. Existence-check COUNT queries left alone since they don't aggregate. Co-Authored-By: Claude Opus 4.7 (1M context) --- scripts/data/create_graphs_ganak.py | 27 ++++++++++++++------------- scripts/data/get_data_ganak.py | 29 +++++++++++++++++++++-------- 2 files changed, 35 insertions(+), 21 deletions(-) diff --git a/scripts/data/create_graphs_ganak.py b/scripts/data/create_graphs_ganak.py index 9e5418d8..5bc37bce 100755 --- a/scripts/data/create_graphs_ganak.py +++ b/scripts/data/create_graphs_ganak.py @@ -741,7 +741,7 @@ def _preproc_step_stats(con, dirs_sql, where_extra="", per_cnf=False): cur.execute( f"SELECT name, dirname, fname, delta_irred_bins, delta_irred_long_cls," f" delta_irred_long_lits, delta_free_vars, step_num" - f" FROM preproc WHERE dirname IN ({dirs_sql}){where_extra}" + f" FROM preproc WHERE dirname IN ({dirs_sql}) AND depth = 0{where_extra}" ) if per_cnf: @@ -855,7 +855,7 @@ def print_preproc_delta_table(matched_dirs, verbose=False): ROUND(100.0 * SUM(CASE WHEN delta_free_vars < 0 THEN 1 ELSE 0 END) / COUNT(*), 0) as pct_invoc_red_vars, ROUND(SUM(step_time), 2) as total_step_s - FROM preproc WHERE dirname IN ({dirs_sql}) + FROM preproc WHERE dirname IN ({dirs_sql}) AND depth = 0 GROUP BY name ORDER BY sum_d_lits ASC """) @@ -912,7 +912,7 @@ def print_preproc_step_efficiency(matched_dirs): SUM(CASE WHEN delta_free_vars < 0 THEN 1 ELSE 0 END) AS calls_var, ROUND(SUM(step_time), 2) AS total_s FROM preproc - WHERE dirname IN ({dirs_sql}) + WHERE dirname IN ({dirs_sql}) AND depth = 0 GROUP BY name HAVING lits_rmvd > 0 OR fvars_rmvd > 0 ORDER BY lits_rmvd DESC @@ -980,7 +980,7 @@ def print_preproc_time_breakdown(matched_dirs): SUM(IFNULL(delta_elimed_vars, 0)) AS elim_vars, SUM(IFNULL(delta_units, 0)) AS units_found FROM preproc - WHERE dirname IN ({dirs_sql}) AND step_time IS NOT NULL + WHERE dirname IN ({dirs_sql}) AND depth = 0 AND step_time IS NOT NULL GROUP BY name ORDER BY total_s DESC """) @@ -1047,7 +1047,7 @@ def print_preproc_noop_waste(matched_dirs): THEN step_time ELSE 0 END), 2) AS wasted_s, ROUND(SUM(step_time), 2) AS total_s FROM preproc - WHERE dirname IN ({dirs_sql}) AND step_time IS NOT NULL + WHERE dirname IN ({dirs_sql}) AND depth = 0 AND step_time IS NOT NULL GROUP BY name HAVING n_noop > 0 ORDER BY wasted_s DESC @@ -1089,7 +1089,7 @@ def print_preproc_extended_vars(matched_dirs): SUM(IFNULL(delta_units, 0)) AS sum_units, ROUND(SUM(step_time), 2) AS total_s FROM preproc - WHERE dirname IN ({dirs_sql}) + WHERE dirname IN ({dirs_sql}) AND depth = 0 AND (IFNULL(delta_elimed_vars,0) != 0 OR IFNULL(delta_replaced_vars,0) != 0 OR IFNULL(delta_units,0) != 0) @@ -1148,7 +1148,7 @@ def print_step_predecessor_effectiveness(matched_dirs, step="must-scc-vrepl"): OR delta_free_vars < 0 THEN 1 ELSE 0 END) / COUNT(*), 1) AS pct_active FROM preproc - WHERE dirname IN ({dirs_sql}) AND name='{step}' + WHERE dirname IN ({dirs_sql}) AND depth = 0 AND name='{step}' GROUP BY prev_step ORDER BY sum_lits DESC """) @@ -1215,7 +1215,7 @@ def preproc_time_chart(matched_dirs): AND IFNULL(delta_units,0) = 0 THEN step_time ELSE 0 END), 2) AS wasted_s FROM preproc - WHERE dirname IN ({dirs_sql}) AND step_time IS NOT NULL + WHERE dirname IN ({dirs_sql}) AND depth = 0 AND step_time IS NOT NULL GROUP BY name ORDER BY total_s DESC """) @@ -1280,7 +1280,7 @@ def preproc_efficiency_chart(matched_dirs): -SUM(delta_irred_long_lits) AS sum_lits, ROUND(SUM(step_time), 2) AS total_s FROM preproc - WHERE dirname IN ({dirs_sql}) AND step_time IS NOT NULL AND step_time > 0 + WHERE dirname IN ({dirs_sql}) AND depth = 0 AND step_time IS NOT NULL AND step_time > 0 GROUP BY name HAVING sum_lits > 0 AND total_s > 0 ORDER BY (sum_lits / total_s) DESC @@ -1344,7 +1344,7 @@ def preproc_time_pie_chart(matched_dirs): cur.execute(f""" SELECT name, ROUND(SUM(step_time), 2) AS total_s FROM preproc - WHERE dirname IN ({dirs_sql}) AND step_time IS NOT NULL + WHERE dirname IN ({dirs_sql}) AND depth = 0 AND step_time IS NOT NULL GROUP BY name ORDER BY total_s DESC """) @@ -1485,7 +1485,7 @@ def preproc_share_chart(matched_dirs): -SUM(delta_irred_long_lits) as sum_lits, -SUM(delta_free_vars) as sum_vars FROM preproc - WHERE dirname IN ({dirs_sql}) + WHERE dirname IN ({dirs_sql}) AND depth = 0 GROUP BY name ORDER BY sum_lits DESC """) @@ -1575,7 +1575,7 @@ def preproc_cumulative_chart(matched_dirs): -SUM(delta_free_vars) as sum_vars, AVG(step_num) as avg_pos FROM preproc - WHERE dirname IN ({dirs_sql}) + WHERE dirname IN ({dirs_sql}) AND depth = 0 GROUP BY name ORDER BY avg_pos ASC """) @@ -1648,7 +1648,7 @@ def print_preproc_per_step_detail(matched_dirs, verbose=False): f"SELECT name," f" ROUND(100.0 * SUM(CASE WHEN delta_irred_long_lits != 0 OR delta_irred_bins != 0" f" OR delta_free_vars != 0 THEN 1 ELSE 0 END) / COUNT(*), 1)" - f" FROM preproc WHERE dirname IN ({dirs_sql}) GROUP BY name" + f" FROM preproc WHERE dirname IN ({dirs_sql}) AND depth = 0 GROUP BY name" ) pct_active = {row[0]: row[1] for row in cur.fetchall()} con.close() @@ -2021,6 +2021,7 @@ def create_notebook(dirs): "out-ganak-mccomp2324-1452294-1", # same as above, but with arjun changes back to "out-ganak-mccomp2324-1299016-0" (with option for 1 new idea) #"out-ganak-mccomp2324-1458467-", # let's try some new ideas from LLM for arjun improvement -- but cadiback was wrongly set up # "out-ganak-mccomp2324-1514564-", # let's try some new ideas from LLM for arjun improvement -- there's been another f*ck up + # "out-ganak-mccomp2324-1517017-0", # 4 full runs for all the 4 new arjun orders ] # only_dirs = [ # "mei-march-2026-1239767-1", # gpmc diff --git a/scripts/data/get_data_ganak.py b/scripts/data/get_data_ganak.py index 939d357e..e978e1bc 100755 --- a/scripts/data/get_data_ganak.py +++ b/scripts/data/get_data_ganak.py @@ -294,6 +294,7 @@ def parse_ganak_output(fname): r'c o \[simp-stats\] (BEFORE|AFTER) (\S+) ' r'irred_bins (\d+) irred_long_cls (\d+) irred_long_lits (\d+) free_vars (\d+)' r'(?:\s+elimed_vars (\d+) replaced_vars (\d+) units (\d+) mem_MB (\d+) T:\s*([\d.]+))?' + r'(?:\s+depth (\d+))?' ) @@ -301,10 +302,16 @@ def parse_simp_stats(fname): """Parse [simp-stats] BEFORE/AFTER pairs from a ganak output file. Returns a list of dicts, one per matched BEFORE/AFTER pair. - New fields (from extended log format): - elimed_vars, replaced_vars, units, mem_MB, step_time, prev_step + Each record carries `depth` (nesting level of the wrapper at emission + time). Top-level steps are depth=0; nested children are depth>=1 and + their work is already counted by the parent — sum only depth=0 for + total-time accounting. + + Older logs without the `depth N` suffix get depth=0 (treated as flat). """ - # pending[name] -> list of full parsed tuples waiting for matching AFTER + # pending[(name, depth)] -> stack of pending BEFOREs awaiting matching AFTER. + # LIFO matching is required when the same-name step nests (e.g. clean-cls + # called from inside another clean-cls dispatch). pending = {} step_counts = {} # name -> number of completed pairs so far records = [] @@ -325,12 +332,14 @@ def parse_simp_stats(fname): if m.group(7) is not None: ext = (int(m.group(7)), int(m.group(8)), int(m.group(9)), int(m.group(10)), float(m.group(11))) + depth = int(m.group(12)) if m.group(12) is not None else 0 + key = (name, depth) if kind == "BEFORE": - pending.setdefault(name, []).append((core, ext)) + pending.setdefault(key, []).append((core, ext)) elif kind == "AFTER": - if pending.get(name): - before_core, before_ext = pending[name].pop(0) + if pending.get(key): + before_core, before_ext = pending[key].pop() occurrence = step_counts.get(name, 0) step_counts[name] = occurrence + 1 step_num = len(records) @@ -338,6 +347,7 @@ def parse_simp_stats(fname): "step_num": step_num, "occurrence": occurrence, "name": name, + "depth": depth, "prev_step": last_completed_step, "before_irred_bins": before_core[0], "before_irred_long_cls": before_core[1], @@ -578,7 +588,7 @@ def g(d, key): ]) preproc_cols = [ - "dirname", "fname", "step_num", "occurrence", "name", "prev_step", + "dirname", "fname", "step_num", "occurrence", "name", "depth", "prev_step", "before_irred_bins", "before_irred_long_cls", "before_irred_long_lits", "before_free_vars", "after_irred_bins", "after_irred_long_cls", "after_irred_long_lits", "after_free_vars", "delta_irred_bins", "delta_irred_long_cls", "delta_irred_long_lits", "delta_free_vars", @@ -606,6 +616,7 @@ def g_rec(rec, key): rec["step_num"], rec["occurrence"], rec["name"], + rec.get("depth", 0), rec.get("prev_step", "none"), rec["before_irred_bins"], rec["before_irred_long_cls"], @@ -694,6 +705,7 @@ def n(v): step_num INT NOT NULL, occurrence INT NOT NULL, name STRING NOT NULL, + depth INT NOT NULL DEFAULT 0, prev_step STRING NOT NULL DEFAULT 'none', before_irred_bins INT, before_irred_long_cls INT, @@ -807,6 +819,7 @@ def n(v): rec["step_num"], rec["occurrence"], rec["name"], + rec.get("depth", 0), rec.get("prev_step", "none"), n(rec.get("before_irred_bins")), n(rec.get("before_irred_long_cls")), @@ -836,7 +849,7 @@ def n(v): )) conn.executemany( - "INSERT INTO preproc VALUES (" + ",".join(["?"] * 31) + ")", + "INSERT INTO preproc VALUES (" + ",".join(["?"] * 32) + ")", preproc_rows ) From 1e68f2bfce0b306e4c5fc434a807fa54e1558b03 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Sun, 24 May 2026 22:40:19 +0200 Subject: [PATCH 04/10] New run, graph update --- scripts/data/create_graphs_ganak.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/data/create_graphs_ganak.py b/scripts/data/create_graphs_ganak.py index 5bc37bce..84b6815a 100755 --- a/scripts/data/create_graphs_ganak.py +++ b/scripts/data/create_graphs_ganak.py @@ -2005,7 +2005,7 @@ def create_notebook(dirs): # "out-ganak-mccomp2324-1261017-0", # Different order in Arjun # "out-ganak-mccomp2324-1279568-0", # release # "out-ganak-mccomp2324-1281478-0", # more data - "out-ganak-mccomp2324-1282000-0", # new preproc VERY GOOD !!!!!!!!!!!!!!!!! + # "out-ganak-mccomp2324-1282000-0", # new preproc VERY GOOD !!!!!!!!!!!!!!!!! # "out-ganak-mccomp2324-1282412-0", # new preproc v2 # "out-ganak-mccomp2324-1286085-", # 4 new puura orders # "out-ganak-mccomp2324-1286556-", # 4 new puura orders, and wl-based cache compact @@ -2018,10 +2018,10 @@ def create_notebook(dirs): # "out-ganak-mccomp2324-1358071-1", # same as above, but with CMS changes reverted -- Current best (kinda...) # "out-ganak-mccomp2324-1373930-1", # no grow after # "out-ganak-mccomp2324-1358071-", # same as above, but with CMS changes reverted - "out-ganak-mccomp2324-1452294-1", # same as above, but with arjun changes back to "out-ganak-mccomp2324-1299016-0" (with option for 1 new idea) + # "out-ganak-mccomp2324-1452294-1", # same as above, but with arjun changes back to "out-ganak-mccomp2324-1299016-0" (with option for 1 new idea) #"out-ganak-mccomp2324-1458467-", # let's try some new ideas from LLM for arjun improvement -- but cadiback was wrongly set up # "out-ganak-mccomp2324-1514564-", # let's try some new ideas from LLM for arjun improvement -- there's been another f*ck up - # "out-ganak-mccomp2324-1517017-0", # 4 full runs for all the 4 new arjun orders + "out-ganak-mccomp2324-1517017-0", # 4 full runs for all the 4 new arjun orders ] # only_dirs = [ # "mei-march-2026-1239767-1", # gpmc From 568fd1dd63bd8548f3c22910c2c22b3e69037a21 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 25 May 2026 01:00:18 +0200 Subject: [PATCH 05/10] Add units-found line to preproc cumulative chart Backbone-simpl is invisible on the volume-based cumulative chart because its only contribution is via unit propagation (delta_free_vars from units) which is dwarfed by occ-bve's BVE elimination. Plotting cumulative delta_units separately makes backbone-simpl's ~44% share of unit-finding visible at its pipeline position. Also: accept .out_arjun files in get_data_ganak.py; switch only_dirs to the latest run (1635700-0). Co-Authored-By: Claude Opus 4.7 (1M context) --- scripts/data/create_graphs_ganak.py | 24 ++++++++++++++---------- scripts/data/get_data_ganak.py | 2 +- 2 files changed, 15 insertions(+), 11 deletions(-) diff --git a/scripts/data/create_graphs_ganak.py b/scripts/data/create_graphs_ganak.py index 84b6815a..470dc53e 100755 --- a/scripts/data/create_graphs_ganak.py +++ b/scripts/data/create_graphs_ganak.py @@ -1573,6 +1573,7 @@ def preproc_cumulative_chart(matched_dirs): -SUM(delta_irred_long_cls) as sum_cls, -SUM(delta_irred_bins) as sum_bins, -SUM(delta_free_vars) as sum_vars, + SUM(IFNULL(delta_units, 0)) as sum_units, AVG(step_num) as avg_pos FROM preproc WHERE dirname IN ({dirs_sql}) AND depth = 0 @@ -1592,15 +1593,16 @@ def preproc_cumulative_chart(matched_dirs): gp_file = f"{TMP_DIR}/preproc_cumul_{lbl}.gnuplot" # Normalise to millions for readability - cum_lits = cum_cls = cum_vars = 0.0 + cum_lits = cum_cls = cum_vars = cum_units = 0.0 with open(dat_file, "w") as f: - f.write("# i cum_lits_M cum_cls_M cum_vars_M step_name\n") - f.write("0\t0.0\t0.0\t0.0\tstart\n") - for i, (name, s_lits, s_long_cls, s_bins, s_vars, _pos) in enumerate(rows): - cum_lits += max(s_lits, 0) / 1e6 - cum_cls += max((s_long_cls or 0) + (s_bins or 0), 0) / 1e6 - cum_vars += max(s_vars, 0) / 1e6 - f.write(f"{i+1}\t{cum_lits:.3f}\t{cum_cls:.3f}\t{cum_vars:.3f}\t{name}\n") + f.write("# i cum_lits_M cum_cls_M cum_vars_M cum_units_M step_name\n") + f.write("0\t0.0\t0.0\t0.0\t0.0\tstart\n") + for i, (name, s_lits, s_long_cls, s_bins, s_vars, s_units, _pos) in enumerate(rows): + cum_lits += max(s_lits, 0) / 1e6 + cum_cls += max((s_long_cls or 0) + (s_bins or 0), 0) / 1e6 + cum_vars += max(s_vars, 0) / 1e6 + cum_units += max(s_units or 0, 0) / 1e6 + f.write(f"{i+1}\t{cum_lits:.3f}\t{cum_cls:.3f}\t{cum_vars:.3f}\t{cum_units:.3f}\t{name}\n") n = len(rows) height_cm = max(16, n * 1.1) @@ -1625,7 +1627,8 @@ def preproc_cumulative_chart(matched_dirs): f.write(f'set ytics ({ytics_str})\n') f.write(f'plot "{dat_file}" using 2:1 with linespoints lc rgb "steelblue" lw 2 pt 7 ps 1 title "lits removed",\\\n') f.write(f' "{dat_file}" using 3:1 with linespoints lc rgb "dark-orange" lw 2 pt 5 ps 1 title "cls removed (bin+long)",\\\n') - f.write(f' "{dat_file}" using 4:1 with linespoints lc rgb "dark-green" lw 2 pt 9 ps 1 title "vars removed"\n\n') + f.write(f' "{dat_file}" using 4:1 with linespoints lc rgb "dark-green" lw 2 pt 9 ps 1 title "vars removed",\\\n') + f.write(f' "{dat_file}" using 5:1 with linespoints lc rgb "dark-violet" lw 2 pt 11 ps 1 title "units found"\n\n') title = f"Preproc cumulative chart (all steps, n={n}, ordered by pipeline position)" print(f"\n{BLUE}{title}{RESET}") @@ -2021,7 +2024,8 @@ def create_notebook(dirs): # "out-ganak-mccomp2324-1452294-1", # same as above, but with arjun changes back to "out-ganak-mccomp2324-1299016-0" (with option for 1 new idea) #"out-ganak-mccomp2324-1458467-", # let's try some new ideas from LLM for arjun improvement -- but cadiback was wrongly set up # "out-ganak-mccomp2324-1514564-", # let's try some new ideas from LLM for arjun improvement -- there's been another f*ck up - "out-ganak-mccomp2324-1517017-0", # 4 full runs for all the 4 new arjun orders + # "out-ganak-mccomp2324-1517017-0", # 4 full runs for all the 4 new arjun orders + "out-ganak-mccomp2324-1635700-0", # fix the printing of the preproc data ] # only_dirs = [ # "mei-march-2026-1239767-1", # gpmc diff --git a/scripts/data/get_data_ganak.py b/scripts/data/get_data_ganak.py index e978e1bc..a48e5b05 100755 --- a/scripts/data/get_data_ganak.py +++ b/scripts/data/get_data_ganak.py @@ -454,7 +454,7 @@ def main(): files[base]["solver"] = tp["solver"] continue - if f.endswith(".out_ganak") or f.endswith(".out"): + if f.endswith(".out_ganak") or f.endswith(".out_arjun") or f.endswith(".out"): files[base]["solver"] = "ganak" files[base].update(parse_ganak_output(f)) simp = parse_simp_stats(f) From 4e36ad335df716ba57b92e933be33ed0be28345e Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 25 May 2026 01:14:05 +0200 Subject: [PATCH 06/10] Shrink preproc charts and enlarge pie-chart text for slide use Cumulative chart was unusably tall (52cm x ~40cm) and the pie chart's labels were too small to read once scaled down inside a beamer slide. Reduce both figure sizes and bump pie-chart font sizes; move the cumulative-chart legend to bottom right where it doesn't sit on top of the curves. --- scripts/data/create_graphs_ganak.py | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/scripts/data/create_graphs_ganak.py b/scripts/data/create_graphs_ganak.py index 470dc53e..107f6390 100755 --- a/scripts/data/create_graphs_ganak.py +++ b/scripts/data/create_graphs_ganak.py @@ -1392,12 +1392,12 @@ def preproc_time_pie_chart(matched_dirs): with open(gp_file, "w") as f: for term, out, sz in [ - (f'pdfcairo size 52cm,40cm background "#d0d0d0"', pdf_file, ""), - (f'pngcairo size 800,640 background "#d0d0d0"', png_file, ""), + (f'pdfcairo size 20cm,16cm font ",18" background "#d0d0d0"', pdf_file, ""), + (f'pngcairo size 800,640 font ",12" background "#d0d0d0"', png_file, ""), ]: f.write(f'set terminal {term}\n') f.write(f'set output "{out}"\n') - f.write(f'set title "Preprocessing time breakdown (total {grand_total:.0f}s)\\n{lbl}"\n') + f.write(f'set title "Preprocessing time breakdown (total {grand_total:.0f}s)\\n{lbl}" font ",20"\n') f.write('set size ratio -1\n') f.write('unset border\n') f.write('unset tics\n') @@ -1426,13 +1426,13 @@ def preproc_time_pie_chart(matched_dirs): lx = r_label * math.cos(mid) ly = r_label * math.sin(mid) pct_str = f"{pct*100:.1f}%" - label_lines.append(f'set label "{name}\\n{pct_str}" at {lx:.3f},{ly:.3f} center font ",8"\n') + label_lines.append(f'set label "{name}\\n{pct_str}" at {lx:.3f},{ly:.3f} center font ",16"\n') # Legend entry at right lx2 = 1.25 ly2 = 0.95 - i * 0.13 f.write(f'set object {n_slices+i+1} rect from {lx2-0.05},{ly2-0.04} to {lx2+0.05},{ly2+0.04} ' f'fc rgb "{color}" fs solid 0.85 border lc rgb "grey"\n') - label_lines.append(f'set label "{name} ({pct*100:.1f}%)" at {lx2+0.08},{ly2} left font ",9"\n') + label_lines.append(f'set label "{name} ({pct*100:.1f}%)" at {lx2+0.08},{ly2} left font ",16"\n') angle = end_angle for ll in label_lines: f.write(ll) @@ -1605,15 +1605,16 @@ def preproc_cumulative_chart(matched_dirs): f.write(f"{i+1}\t{cum_lits:.3f}\t{cum_cls:.3f}\t{cum_vars:.3f}\t{cum_units:.3f}\t{name}\n") n = len(rows) - height_cm = max(16, n * 1.1) + height_cm = max(8, n * 0.40) + width_cm = 24 ytics_parts = ['"start" 0'] + [f'"{name}" {i+1}' for i, (name, *_) in enumerate(rows)] ytics_str = ", ".join(ytics_parts) with open(gp_file, "w") as f: for term, out in [ - (f'pdfcairo size 52cm,{height_cm:.0f}cm background "#d0d0d0"', pdf_file), - (f'pngcairo size 1200,{int(height_cm * 50)} background "#d0d0d0"', png_file), + (f'pdfcairo size {width_cm}cm,{height_cm:.0f}cm background "#d0d0d0"', pdf_file), + (f'pngcairo size {width_cm * 50},{int(height_cm * 50)} background "#d0d0d0"', png_file), ]: f.write(f'set terminal {term}\n') f.write(f'set output "{out}"\n') @@ -1623,7 +1624,7 @@ def preproc_cumulative_chart(matched_dirs): f.write(f'set yrange [-0.5:{n + 0.5}]\n') f.write('set xrange [0:*]\n') f.write('set grid xtics\n') - f.write('set key top left\n') + f.write('set key bottom right\n') f.write(f'set ytics ({ytics_str})\n') f.write(f'plot "{dat_file}" using 2:1 with linespoints lc rgb "steelblue" lw 2 pt 7 ps 1 title "lits removed",\\\n') f.write(f' "{dat_file}" using 3:1 with linespoints lc rgb "dark-orange" lw 2 pt 5 ps 1 title "cls removed (bin+long)",\\\n') From 1d3f30445480f363a7ec244914b93b30dbede548 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 25 May 2026 10:22:10 +0200 Subject: [PATCH 07/10] Fix font sizes --- scripts/data/create_graphs_ganak.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/data/create_graphs_ganak.py b/scripts/data/create_graphs_ganak.py index 107f6390..6fab3bf0 100755 --- a/scripts/data/create_graphs_ganak.py +++ b/scripts/data/create_graphs_ganak.py @@ -1426,13 +1426,13 @@ def preproc_time_pie_chart(matched_dirs): lx = r_label * math.cos(mid) ly = r_label * math.sin(mid) pct_str = f"{pct*100:.1f}%" - label_lines.append(f'set label "{name}\\n{pct_str}" at {lx:.3f},{ly:.3f} center font ",16"\n') + label_lines.append(f'set label "{name}\\n{pct_str}" at {lx:.3f},{ly:.3f} center font ",13"\n') # Legend entry at right lx2 = 1.25 ly2 = 0.95 - i * 0.13 f.write(f'set object {n_slices+i+1} rect from {lx2-0.05},{ly2-0.04} to {lx2+0.05},{ly2+0.04} ' f'fc rgb "{color}" fs solid 0.85 border lc rgb "grey"\n') - label_lines.append(f'set label "{name} ({pct*100:.1f}%)" at {lx2+0.08},{ly2} left font ",16"\n') + label_lines.append(f'set label "{name} ({pct*100:.1f}%)" at {lx2+0.08},{ly2} left font ",13"\n') angle = end_angle for ll in label_lines: f.write(ll) From 322ed86b1ba2f5c4e37bbd2510d2dece419b4648 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 27 May 2026 21:05:49 +0200 Subject: [PATCH 08/10] No more bce --- src/main.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main.cpp b/src/main.cpp index a4adb1b2..01d2555c 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -209,7 +209,6 @@ void add_ganak_options() add_arg("--arjunbackwmaxc", arjun_backw_maxc, fc_int, "Arjun backw max confl"); add_arg("--arjunoraclefindbins", arjun_oracle_find_bins, fc_int, "Arjun's oracle should find bins or not"); add_arg("--arjunoraclemult", simp_conf.oracle_mult, fc_double, "Multiplier for Arjun's oracle timeout when it is called from Puura"); - add_arg("--bce", etof_conf.do_bce, fc_int, "Do static BCE"); add_arg("--bveresolvmaxsz", simp_conf.bve_too_large_resolvent, fc_int, "Puura BVE max resolvent size in literals. -1 == no limit"); add_arg("--bvegrowiter1", simp_conf.bve_grow_iter1, fc_int, "Puura BVE growth allowance iter1"); add_arg("--bvegrowiter2", simp_conf.bve_grow_iter2, fc_int, "Puura BVE growth allowance iter2"); From b061e3e6c8a662fe9c37cec4d5db2aa10f23b5ac Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 28 May 2026 16:19:43 +0200 Subject: [PATCH 09/10] Expose LaurentPolyGen as mode 13 Add Laurent polynomial counting (multivariate Laurent polynomials over the rationals, allowing negative exponents) as --mode 13, wiring up the FieldGen construction and result output. Document usage with a worked example in the README and add a lit test. Co-Authored-By: Claude Opus 4.7 (1M context) --- README.md | 43 ++++++++++++++++++++++++++++++++++++++ src/main.cpp | 12 ++++++++++- tests/cnf-files/mode13.cnf | 10 +++++++++ 3 files changed, 64 insertions(+), 1 deletion(-) create mode 100644 tests/cnf-files/mode13.cnf diff --git a/README.md b/README.md index ec0e5faa..9f1a04ac 100644 --- a/README.md +++ b/README.md @@ -260,6 +260,49 @@ two systems' counts to get the final count. | 5 | `--mode 5` | Integer mod prime | `c p weight 1 3 0` | Requires `--prime X` | | 6 | `--mode 6` | Complex float (MPFR) | `c p weight 9 1/2+4i 0` | Must give both parts: `a+bi` or `a-bi`; see `--mpfrprec` | | 7 | `--mode 7` | Real float (MPFR) | `c p weight 1 0.3 0` | See `--mpfrprec` | +| 13 | `--mode 13` | Laurent polynomial over rationals | `c p weight 9 1/2*z0^2-3*z1^-1 0` | Requires `--npolyvars N`; exponents may be negative | + +### Laurent polynomial counting (`--mode 13`) + +Mode 13 is like the polynomial mode (`--mode 3`) but the weights are +*multivariate Laurent polynomials* over the rationals, i.e. polynomials whose +variable exponents may be **negative** as well as non-negative. Pass the number +of polynomial variables with `--npolyvars N`, and refer to them as `z0`, `z1`, +..., `z(N-1)` in the weight lines. Terms are written `coeff*zI^e` (the +exponent `e` may be negative, and parentheses around it are optional, e.g. +`z0^-2` or `z0^(-2)`); separate terms with `+`/`-`. A single weight line such as +`c p weight 9 1/2*z0^2 - 3*z1^-1 + z0^(-2) 0` is a valid Laurent polynomial. + +#### Worked example + +The following CNF has one clause `z0 ∨ z1` and assigns a Laurent-polynomial +weight to each literal: + +``` +p cnf 2 1 +c t wmc +1 2 0 +c p weight 1 z0+1 0 +c p weight -1 z0^-1 0 +c p weight 2 z1+1 0 +c p weight -2 z1^-1 0 +``` + +Running it: + +``` +./ganak --mode 13 --npolyvars 2 example.cnf +``` + +produces (summing the weight products over the three satisfying assignments): + +``` +s SATISFIABLE +c s exact laurent z0*z1 + z0 + z1 + z0*z1^-1 + 1 + z0^-1*z1 + z1^-1 + z0^-1 +``` + +The count is printed on the `c s exact laurent` line as the resulting Laurent +polynomial. You can also write your own field by implementing the `Field` and `FieldGen` interfaces. Absolutely _any_ field will work, and it's as easy as implementing diff --git a/src/main.cpp b/src/main.cpp index 01d2555c..456fd324 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -181,7 +181,8 @@ void add_ganak_options() 4=parity counting, 5=counting over a prime field (see --prime), 6=mpfr floating point complex numbers (see --mpfrprec), -7=mpfr floating point real numbers (see --mpfrprec) +7=mpfr floating point real numbers (see --mpfrprec), +13=multivariate Laurent polynomials over the rational field (see --npolyvars) )delimiter"); add_arg("--prime", prime_field, fc_int, "Prime for prime field counting"); add_arg("--npolyvars", poly_nvars, fc_int, "Number of variables in the polynomial field"); @@ -562,6 +563,8 @@ void run_weighted_counter(Ganak& counter, const ArjunNS::SimplifiedCNF& cnf, con } } else if (mode == 3) { cout << "c s exact poly " << *cnt << endl; + } else if (mode == 13) { + cout << "c s exact laurent " << *cnt << endl; } else if (mode == 4) { cout << "c s exact parity " << *cnt << endl; } else if (mode == 5) { @@ -631,6 +634,13 @@ int main(int argc, char *argv[]) { } fg = std::make_unique(poly_nvars); break; + case 13: + if (poly_nvars == -1) { + cout << "c o [arjun] ERROR: Must provide number of polynomial vars for mode 13 via --npolyvars" << endl; + exit(EXIT_FAILURE); + } + fg = std::make_unique(poly_nvars); + break; case 4: fg = std::make_unique(); break; diff --git a/tests/cnf-files/mode13.cnf b/tests/cnf-files/mode13.cnf new file mode 100644 index 00000000..00c7ada4 --- /dev/null +++ b/tests/cnf-files/mode13.cnf @@ -0,0 +1,10 @@ +c c RUN: %solver --mode 13 --npolyvars 2 %s | %OutputCheck %s +p cnf 2 1 +c t wmc +1 2 0 +c p weight 1 z0+1 0 +c p weight -1 z0^-1 0 +c p weight 2 z1+1 0 +c p weight -2 z1^-1 0 +c c CHECK: ^s SATISFIABLE$ +c c CHECK: ^c s exact laurent z0\*z1 \+ z0 \+ z1 \+ z0\*z1\^-1 \+ 1 \+ z0\^-1\*z1 \+ z1\^-1 \+ z0\^-1$ From 789fb1521c487e8dee29667758ad4b680de63257 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 28 May 2026 16:55:00 +0200 Subject: [PATCH 10/10] Fix zlib download: use GitHub release instead of zlib.net zlib.net DNS resolution fails in CI; download the identical zlib-1.3.1 tarball from the madler/zlib GitHub release instead. Co-Authored-By: Claude Opus 4.7 (1M context) --- .github/workflows/build.yml | 4 ++-- .github/workflows/release.yml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 51b92dad..a7554752 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -67,7 +67,7 @@ jobs: - name: Install zlib for Mac dynamic if: contains(matrix.os, 'macos') && matrix.shared_libs == 'ON' run: | - wget https://zlib.net/fossils/zlib-1.3.1.tar.gz + wget https://github.com/madler/zlib/releases/download/v1.3.1/zlib-1.3.1.tar.gz tar xzvf zlib-1.3.1.tar.gz cd zlib-1.3.1 ./configure @@ -78,7 +78,7 @@ jobs: - name: Install zlib for Mac static if: contains(matrix.os, 'macos') && matrix.shared_libs == 'OFF' run: | - wget https://zlib.net/fossils/zlib-1.3.1.tar.gz + wget https://github.com/madler/zlib/releases/download/v1.3.1/zlib-1.3.1.tar.gz tar xzvf zlib-1.3.1.tar.gz cd zlib-1.3.1 ./configure --static diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index b0f96215..ef77840f 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -65,7 +65,7 @@ jobs: - name: Install zlib for Mac static if: contains(matrix.os, 'macos') run: | - wget https://zlib.net/fossils/zlib-1.3.1.tar.gz + wget https://github.com/madler/zlib/releases/download/v1.3.1/zlib-1.3.1.tar.gz tar xzvf zlib-1.3.1.tar.gz cd zlib-1.3.1 ./configure --static