Development happens here

CLAUDE.md

@@ -18,10 +18,10 @@ Always disable ccache and build the `ganak` target:
 CCACHE_DISABLE=1 cmake --build build --target ganak -j8 2>&1 | tail -20
 ```
 
-The build directory is `build/`. If it doesn't exist or CMake needs to be re-run:
+The build directory is `build/`. Go to that directory, and run:
 
 ```
-mkdir -p build && cd build && cmake ..
+./build_norm.sh
 ```
 
 Common build options:

CMakeLists.txt

@@ -355,6 +355,21 @@ if(POLICY CMP0169)
 endif()
 
 
+# ---- cadical / cadiback (transitive deps of arjun/cryptominisat) ----
+# These are not used directly by ganak, but arjun's exported target lists
+# them in its INTERFACE_LINK_LIBRARIES.  Import them here so CMake resolves
+# them to actual library paths rather than bare -l flags.
+set(cadical_DIR "" CACHE PATH "cadical build dir containing cadicalConfig.cmake")
+if(cadical_DIR AND NOT TARGET cadical)
+    find_package(cadical CONFIG REQUIRED HINTS "${cadical_DIR}")
+    message(STATUS "cadical: using pre-built at ${cadical_DIR}")
+endif()
+set(cadiback_DIR "" CACHE PATH "cadiback build dir containing cadibackConfig.cmake")
+if(cadiback_DIR AND NOT TARGET cadiback)
+    find_package(cadiback CONFIG REQUIRED HINTS "${cadiback_DIR}")
+    message(STATUS "cadiback: using pre-built at ${cadiback_DIR}")
+endif()
+
 # ---- CryptoMiniSat5 ----
 set(cryptominisat5_DIR "" CACHE PATH "cryptominisat5 install/build prefix (contains lib/cmake/cryptominisat5/). Auto-resolved if empty.")
 if(NOT TARGET cryptominisat5)

EMSCRIPTEN.md

@@ -15,6 +15,13 @@ emmake make -j16
 emmake make install
 ```
 
+NOTE: after the above, you need to "make distclean" and also to configure GMP, run:
+```
+./configure --enable-cxx --enable-static --enable-shared CC="gcc -std=gnu17"
+```
+because newest GCC complains
+
+
 Useful commands for building stuff like MPFR and MPIR for Emscripten:
 ```
 EMCONFIGURE_JS=1 emconfigure ./configure ABI=64 --disable-assembly CFLAGS=-m64 CXXFLAGS=-m64 LDFLAGS=-m64 --enable-cxx

README.md

@@ -263,30 +263,17 @@ simplification, and then through Ganak's counting, finally, we combine these
 two systems' counts to get the final count.
 
 ## Supported Weights
-Ganak supports many different weights:
-- For counting over integers, the default mode `--mode 0` works. Here, you can
-  even run approximate counting after some timeout, with e.g `--appmct 1000`
-  which will automatically switch over to approximate counting after 1000s of
-  preprocessing and Ganak.
-- For counting over rationals (i.e. infinite precision weighted counting), you
-  can use `--mode 1` which will give you a precise count, without _any_
-  floating point errors.
-- For counting over the complex rationals field, you need to specify the weight of the
-  literal as a complex number and pass the `--mode 2` flag. For example, if you
-  want to give the weight 1/2 + 4i for literal 9, you can specify the weight as
-  `c p weight 9 1/2 4 0`.
-- For counting over polynomials over a finite field, you can use `--mode 3`
-  which will give you a polynomial count. The weight of the literal is given as
-  `c p weight 9 1/2*x0+4x1+2 0` which means the weight of literal 9 is
-  `1/2*x_0 + 4*x_1+2`. In this mode you MUST specify the number of polynomial
-  variables via `--npolyvars N`
-- For parity counting, you can use the `--mode 4` flag. This will
-  count the number of solutions modulo 2
-- For counting over integers modulo a prime, you can use `--mode 5 --prime X`,
-  where X is the prime.
-- For counting over the complex numbers, but using floats instead of infinite
-  precision rationals, you can use `--mode 6`, and specify the weights as
-  per `--mode 2`.
+
+| Mode | Flag | Field | Weight format example | Notes |
+|------|------|-------|-----------------------|-------|
+| 0 | `--mode 0` | Integer | `c p weight 1 5 0` | Default; 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` |
+| 4 | `--mode 4` | Parity (mod 2) | `c p weight 1 1 0` | |
+| 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` |
 
 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

scripts/build_clang.sh

@@ -6,7 +6,7 @@ rm -rf sharp*
 rm -rf Make*
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 cmake -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_C_COMPILER=clang \
     -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \
     -Dsbva_DIR="${SAT_DIR}/sbva/build" \

scripts/build_clang_analyze.sh

@@ -6,7 +6,7 @@ rm -rf sharp*
 rm -rf Make*
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 cmake -DANALYZE=ON -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_C_COMPILER=clang \
     -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \
     -Dsbva_DIR="${SAT_DIR}/sbva/build" \

scripts/build_debug.sh

@@ -9,7 +9,7 @@ rm -rf sharp*
 rm -rf Make*
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 cmake -DCMAKE_BUILD_TYPE=Debug \
     -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \
     -Dsbva_DIR="${SAT_DIR}/sbva/build" \

scripts/build_emscripten.sh

@@ -13,7 +13,7 @@ rm -rf Makefile
 rm -rf rjun-src
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 emcmake cmake -DCMAKE_INSTALL_PREFIX=$EMINSTALL -DENABLE_TESTING=OFF \
     -Dcadical_DIR="${SAT_DIR}/cadical/build" \
     -Dcadiback_DIR="${SAT_DIR}/cadiback" \

scripts/build_norm.sh

@@ -14,16 +14,16 @@ rm -rf CM*
 rm -rf cmake*
 rm -rf deps
 rm -rf _deps
-SOLVERS_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
-echo "solvers dir: $SOLVERS_DIR"
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
+echo "solvers dir: $SAT_DIR"
 cmake -DENABLE_TESTING=ON \
-    -Dcadical_DIR="${SOLVERS_DIR}/cadical/build" \
-    -Dcadiback_DIR="${SOLVERS_DIR}/cadiback/build" \
-    -Dcryptominisat5_DIR="${SOLVERS_DIR}/cryptominisat/build" \
-    -Dsbva_DIR="${SOLVERS_DIR}/sbva/build" \
-    -Dtreedecomp_DIR="${SOLVERS_DIR}/treedecomp/build" \
-    -Darjun_DIR="${SOLVERS_DIR}/arjun/build" \
-    -Dapproxmc_DIR="${SOLVERS_DIR}/approxmc/build" \
+    -Dcadical_DIR="${SAT_DIR}/cadical/build" \
+    -Dcadiback_DIR="${SAT_DIR}/cadiback/build" \
+    -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \
+    -Dsbva_DIR="${SAT_DIR}/sbva/build" \
+    -Dtreedecomp_DIR="${SAT_DIR}/treedecomp/build" \
+    -Darjun_DIR="${SAT_DIR}/arjun/build" \
+    -Dapproxmc_DIR="${SAT_DIR}/approxmc/build" \
     ..
 make -j$(nproc)
 make test

scripts/build_release.sh

@@ -6,7 +6,7 @@ rm -rf sharp*
 rm -rf Make*
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 cmake -DCMAKE_BUILD_TYPE=Release \
     -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \
     -Dsbva_DIR="${SAT_DIR}/sbva/build" \

scripts/build_sanitize.sh

@@ -8,7 +8,7 @@ rm -rf sharp*
 rm -rf Make*
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 CC=clang CXX=clang++ cmake -DSANITIZE=ON \
     -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \
     -Dsbva_DIR="${SAT_DIR}/sbva/build" \

scripts/build_static.sh

@@ -15,7 +15,7 @@ rm -rf .cmake
 rm -rf lib*
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 cmake -DBUILD_SHARED_LIBS=OFF \
     -DGMPXX_LIBRARY=/usr/local/lib/libgmpxx.a \
     -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \

scripts/build_static_release.sh

@@ -15,7 +15,7 @@ rm -rf .cmake
 rm -rf lib*
 rm -rf deps
 rm -rf _deps
-SAT_DIR=$(cd ../.. && pwd)
+SAT_DIR="$(cd "$(dirname "$0")/../.." && pwd)"
 cmake -DCMAKE_BUILD_TYPE=Release -DBUILD_SHARED_LIBS=OFF \
     -DGMPXX_LIBRARY=/usr/local/lib/libgmpxx.a \
     -Dcryptominisat5_DIR="${SAT_DIR}/cryptominisat/build" \

scripts/cache_miss_bucket_summary.py

@@ -105,7 +105,7 @@ def main():
     total_rows, total_solved = cur.fetchone()
     con.close()
 
-    headers = ["metric"] + [b[0] for b in buckets]
+    headers = ["cache miss rate"] + [b[0] for b in buckets]
     title = f"Cache Miss Rate Bucket Summary  —  {args.dirname}"
     print(f"\n{BLUE}{title}{RESET}")
     for call in calls:

scripts/data/analyze_preproc.py

@@ -0,0 +1,88 @@
+import sqlite3
+import os
+os.chdir("/home/soos/development/sat_solvers/ganak/build/data")
+con = sqlite3.connect("data.sqlite3")
+cur = con.cursor()
+
+cur.execute("""
+SELECT name,
+       COUNT(DISTINCT fname) as n_cnfs,
+       SUM(CASE WHEN delta_irred_long_lits < 0 THEN 1 ELSE 0 END) as invoc_lits,
+       SUM(CASE WHEN delta_free_vars < 0 THEN 1 ELSE 0 END) as invoc_vars,
+       -SUM(delta_irred_long_lits) as sum_lits,
+       -SUM(delta_free_vars) as sum_vars,
+       COUNT(*) as n_invoc
+FROM preproc
+GROUP BY name
+ORDER BY sum_lits DESC
+""")
+rows = cur.fetchall()
+print(f"{'step':<30} {'n_cnfs':>7} {'%inv_lits':>9} {'%inv_vars':>9} {'sum_lits':>12} {'sum_vars':>12} {'n_invoc':>8}")
+print("-"*104)
+for r in rows:
+    name, n_cnfs, invoc_lits, invoc_vars, sum_lits, sum_vars, n_invoc = r
+    pct_lits = 100*invoc_lits/n_invoc if n_invoc else 0
+    pct_vars = 100*invoc_vars/n_invoc if n_invoc else 0
+    print(f"{name:<30} {n_cnfs:>7} {pct_lits:>8.0f}% {pct_vars:>8.0f}% {sum_lits:>12,} {sum_vars:>12,} {n_invoc:>8,}")
+
+cur.execute("SELECT -SUM(delta_irred_long_lits), -SUM(delta_free_vars) FROM preproc")
+t = cur.fetchone()
+print(f"\nTOTAL: lits={t[0]:,}  vars={t[1]:,}")
+
+print("\n\n--- Per-CNF distribution of lits removed (steps that remove lits) ---")
+cur.execute("""
+SELECT p.fname,
+       -SUM(p.delta_irred_long_lits) as total_lits_removed,
+       -SUM(p.delta_free_vars) as total_vars_removed,
+       d.ganak_time
+FROM preproc p
+JOIN data d ON d.fname = p.fname AND d.dirname = p.dirname
+WHERE d.ganak_time IS NOT NULL
+GROUP BY p.dirname, p.fname
+ORDER BY total_lits_removed DESC
+LIMIT 20
+""")
+rows2 = cur.fetchall()
+print(f"{'fname':<50} {'lits_removed':>13} {'vars_removed':>13} {'time':>8}")
+for r in rows2:
+    print(f"{r[0][-48:]:<50} {r[1]:>13,} {r[2]:>13,} {r[3]:>8.2f}")
+
+print("\n\n--- Steps that are ALWAYS active (invoc_pct_lits > 80%) vs rarely active ---")
+cur.execute("""
+SELECT name,
+       COUNT(*) as n_invoc,
+       -SUM(delta_irred_long_lits) as sum_lits,
+       ROUND(100.0 * SUM(CASE WHEN delta_irred_long_lits < 0 THEN 1 ELSE 0 END) / COUNT(*), 1) as pct_lits
+FROM preproc
+GROUP BY name
+HAVING sum_lits > 0
+ORDER BY pct_lits DESC
+""")
+rows3 = cur.fetchall()
+print(f"{'step':<30} {'n_invoc':>8} {'sum_lits':>12} {'%active':>8}")
+for r in rows3:
+    print(f"{r[0]:<30} {r[1]:>8,} {r[2]:>12,} {r[3]:>7.1f}%")
+
+print("\n\n--- occ-bve deep dive: bins added ---")
+cur.execute("""
+SELECT -SUM(delta_irred_bins), SUM(delta_irred_bins), COUNT(*)
+FROM preproc WHERE name = 'occ-bve'
+""")
+r = cur.fetchone()
+print(f"delta_bins total={r[0]:,} sum={r[1]:,} n={r[2]:,}")
+
+print("\n\n--- What's removing the most lits ON AVERAGE per invocation? ---")
+cur.execute("""
+SELECT name,
+       COUNT(*) as n_invoc,
+       -SUM(delta_irred_long_lits) as sum_lits,
+       ROUND(-1.0*SUM(delta_irred_long_lits)/COUNT(*), 1) as avg_lits_per_invoc,
+       ROUND(-1.0*SUM(delta_free_vars)/COUNT(*), 1) as avg_vars_per_invoc
+FROM preproc
+GROUP BY name
+ORDER BY avg_lits_per_invoc DESC
+""")
+rows4 = cur.fetchall()
+print(f"{'step':<30} {'n_invoc':>8} {'sum_lits':>12} {'avg_lits/inv':>13} {'avg_vars/inv':>13}")
+for r in rows4:
+    print(f"{r[0]:<30} {r[1]:>8,} {r[2]:>12,} {r[3]:>13,.1f} {r[4]:>13,.1f}")