Refactor

.gitignore

@@ -4,9 +4,9 @@
 *.jl.mem
 /Manifest.toml
 
-# Benchmark data
-benchmarks/data/
+# Benchmark
 benchmarks/Manifest.toml
+benchmarks/data/
 
 # IDE
 .vscode/
@@ -40,4 +40,5 @@ OptimalBranching.jl/
 *.log
 *.out
 *.history
-/discs/
+/discs/
+/notes/

Project.toml

@@ -13,6 +13,7 @@ GenericTensorNetworks = "3521c873-ad32-4bb4-b63d-f4f178f42b49"
 GraphMakie = "1ecd5474-83a3-4783-bb4f-06765db800d2"
 GraphPlot = "a2cc645c-3eea-5389-862e-a155d0052231"
 Graphs = "86223c79-3864-5bf0-83f7-82e725a168b6"
+Gurobi = "2e9cd046-0924-5485-92f1-d5272153d98b"
 NetworkLayout = "46757867-2c16-5918-afeb-47bfcb05e46a"
 OptimalBranchingCore = "c76e7b22-e1d2-40e8-b0f1-f659837787b8"
 ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
@@ -30,6 +31,7 @@ GenericTensorNetworks = "4"
 GraphMakie = "0.6.3"
 GraphPlot = "0.6.2"
 Graphs = "1.13.1"
+Gurobi = "1.8.0"
 NetworkLayout = "0.4.10"
 OptimalBranchingCore = "0.1"
 ProblemReductions = "0.3.5"

benchmarks/Project.toml

@@ -13,6 +13,7 @@ JSON3 = "0f8b85d8-7281-11e9-16c2-39a750bddbf1"
 JuMP = "4076af6c-e467-56ae-b986-b466b2749572"
 OptimalBranchingCore = "c76e7b22-e1d2-40e8-b0f1-f659837787b8"
 Primes = "27ebfcd6-29c5-5fa9-bf4b-fb8fc14df3ae"
+Printf = "de0858da-6303-5e67-8744-51eddeeeb8d7"
 ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
 Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
 SHA = "ea8e919c-243c-51af-8825-aaa63cd721ce"
@@ -26,6 +27,8 @@ HiGHS = "1.19.3"
 JSON3 = "1.14.3"
 JuMP = "1.29.1"
 OptimalBranchingCore = "0.1.5"
+Printf = "1.11.0"
 ProblemReductions = "0.3.5"
 Random = "1.11.0"
+SHA = "0.7.0"
 Statistics = "1.11.1"

benchmarks/examples/analyze_results.jl

@@ -0,0 +1,83 @@
+using Pkg
+Pkg.activate(joinpath(@__DIR__, ".."))
+
+using BooleanInferenceBenchmarks
+using Statistics
+
+result_dir = resolve_results_dir("factoring")
+
+# 示例 1: 读取某个数据集的所有结果
+println("="^80)
+println("示例 1: 读取 numbers_8x8 数据集的所有结果")
+println("="^80)
+
+results_8x8 = load_dataset_results(result_dir, "numbers_8x8")
+println("找到 $(length(results_8x8)) 个结果")
+
+for (i, result) in enumerate(results_8x8)
+    println("\n结果 $i:")
+    print_result_summary(result)
+end
+
+# 示例 2: 读取所有结果并比较
+println("\n")
+println("="^80)
+println("示例 2: 读取所有结果并比较")
+println("="^80)
+
+all_results = load_all_results(result_dir)
+println("总共找到 $(length(all_results)) 个结果")
+
+compare_results(all_results)
+
+# 示例 3: 筛选特定求解器的结果
+println("\n")
+println("="^80)
+println("示例 3: 只看 BooleanInference 求解器的结果")
+println("="^80)
+
+bi_results = filter_results(all_results, solver_name="BI")
+println("找到 $(length(bi_results)) 个 BI 求解器的结果")
+
+compare_results(bi_results)
+
+# 示例 3.5: 详细比较 BI 求解器的不同配置
+println("\n")
+println("="^80)
+println("示例 3.5: 详细查看 BI 求解器在 numbers_10x10 上的不同配置")
+println("="^80)
+
+bi_10x10 = filter_results(bi_results, dataset="numbers_10x10")
+print_detailed_comparison(bi_10x10)
+
+# 示例 4: 筛选特定数据集和求解器
+println("\n")
+println("="^80)
+println("示例 4: 查看 numbers_10x10 数据集上的所有结果")
+println("="^80)
+
+results_10x10 = filter_results(all_results, dataset="numbers_10x10")
+compare_results(results_10x10)
+
+# 示例 5: 找到最快的配置
+println("\n")
+println("="^80)
+println("示例 5: 找到每个数据集上最快的配置")
+println("="^80)
+
+datasets = unique([splitext(basename(r.dataset_path))[1] for r in all_results])
+for dataset in sort(datasets)
+    dataset_results = filter_results(all_results, dataset=dataset)
+    if !isempty(dataset_results)
+        best = argmin([mean(r.times) for r in dataset_results])
+        best_result = dataset_results[best]
+        println("\n$dataset: $(best_result.solver_name) - Mean time: $(round(mean(best_result.times), digits=4))s")
+
+        # 打印配置
+        println("  Configuration:")
+        for k in sort(collect(keys(best_result.solver_config)))
+            println("    $k: $(best_result.solver_config[k])")
+        end
+    end
+end
+

benchmarks/examples/benchmark.jl

@@ -0,0 +1,67 @@
+using CairoMakie
+using Statistics
+
+bit_lengths = [16]  # 现在只有一个 scale，以后可以变成 [16, 20, 24, ...]
+
+mingamma = [62, 8, 50, 34, 23, 49, 41, 21, 23, 44,
+            40, 18, 30, 30, 16, 49, 58, 58, 29, 20]
+
+mostoccurrence = [47, 44, 25, 21, 46, 46, 54, 36, 6, 17,
+                  34, 38, 36, 16, 12, 18, 41, 41, 7, 18]
+
+kissat = [49, 36, 18, 80, 14, 85, 10, 24, 47, 0,
+          0, 3, 3, 36, 0, 44, 7, 7, 25, 14]
+
+minisat = [62, 61, 40, 70, 52, 96, 89, 36, 76, 6,
+           10, 61, 43, 155, 74, 11, 73, 73, 15, 77]
+
+# Helper function: mean and std for a group of instances
+function mean_and_err(values)
+    m = mean(values)
+    err = std(values)  # or std(values) / sqrt(length(values)) for std error
+    return m, err
+end
+
+m_mingamma, err_mingamma = mean_and_err(mingamma)
+m_most, err_most         = mean_and_err(mostoccurrence)
+m_kissat, err_kissat     = mean_and_err(kissat)
+m_minisat, err_minisat   = mean_and_err(minisat)
+
+f = Figure()
+ax = Axis(f[1, 1],
+    xlabel = "bit length",
+    ylabel = "runtime (or your metric)",
+    title = "Performance vs bit length with error bars",
+)
+
+# For now we only have one bit length, so each algo has just one mean value.
+bit_lengths = [16]
+
+mingamma_means = [m_mingamma]
+mingamma_errs  = [err_mingamma]
+
+most_means = [m_most]
+most_errs  = [err_most]
+
+kissat_means = [m_kissat]
+kissat_errs  = [err_kissat]
+
+minisat_means = [m_minisat]
+minisat_errs  = [err_minisat]
+
+# Plot lines + error bars for each algorithm
+lines!(ax, bit_lengths, mingamma_means, label = "MinGamma")
+errorbars!(ax, bit_lengths, mingamma_means, mingamma_errs, mingamma_errs)
+
+lines!(ax, bit_lengths, most_means, label = "MostOccurrence")
+errorbars!(ax, bit_lengths, most_means, most_errs, most_errs)
+
+lines!(ax, bit_lengths, kissat_means, label = "Kissat")
+errorbars!(ax, bit_lengths, kissat_means, kissat_errs, kissat_errs)
+
+lines!(ax, bit_lengths, minisat_means, label = "MiniSat")
+errorbars!(ax, bit_lengths, minisat_means, minisat_errs, minisat_errs)
+
+axislegend(ax)
+f
+# save("performance_vs_bitlength.png", f)

benchmarks/examples/cnfsat_example.jl

@@ -3,23 +3,44 @@ Pkg.activate(joinpath(@__DIR__, ".."))
 
 using BooleanInferenceBenchmarks
 using ProblemReductions
+using BooleanInference
+using BooleanInference.OptimalBranchingCore
 
-dataset_path = joinpath(@__DIR__, "..", "data", "CNF", "random")
-cnf_files = discover_cnf_files(dataset_path)
-println("Found $(length(cnf_files)) CNF files in $dataset_path:")
-for file in cnf_files
-    instance = parse_cnf_file(file)
-    cnf = cnf_instantiation(instance)
-end
+result_dir = resolve_results_dir("CNFSAT")
+
+for n in [100]
+    for r in [350, 380, 400, 420, 430, 450]
+    dataset_path = joinpath(@__DIR__, "..", "data", "3CNF", "random", "n=$(n)", "$(n)-$(r)")
+
+    for i in 1:5
+        bsconfig = BranchingStrategy(
+            table_solver=TNContractionSolver(),
+            # selector=MinGammaSelector(1,2,TNContractionSolver(), GreedyMerge()),
+            selector=MostOccurrenceSelector(3,i),
+            measure=NumHardTensors(),
+            set_cover_solver=GreedyMerge()
+        )
 
-result = benchmark_dataset(
-    CNFSATProblem,
-    dataset_path;
-    solver=BooleanInferenceSolver(),
-    verify=true
-)
+        result = benchmark_dataset(
+            CNFSATProblem,
+            dataset_path;
+            solver=BooleanInferenceSolver(;bsconfig),
+            verify=false,
+            save_result=result_dir
+        )
+    end
+
+        result = benchmark_dataset(
+            CNFSATProblem,
+            dataset_path;
+            solver=MinisatSolver(minisat_path="/opt/homebrew/bin/minisat", timeout=300.0, quiet=false),
+            verify=false,
+            save_result=result_dir
+        )
+end
+end
 
-test_file = joinpath(dataset_path, "3sat1.cnf")
-test_instance = parse_cnf_file(test_file)
-result = solve_instance(CNFSATProblem, test_instance, BooleanInferenceSolver())
-@show result
+# test_file = joinpath(dataset_path, "3sat10.cnf")
+# test_instance = parse_cnf_file(test_file)
+# result = solve_instance(CNFSATProblem, test_instance, BooleanInferenceSolver(;bsconfig, show_stats=true))
+# result = solve_instance(CNFSATProblem, test_instance, KissatSolver(kissat_path="/opt/homebrew/bin/kissat", timeout=300.0, quiet=false))

benchmarks/examples/compare_region.jl

@@ -0,0 +1,120 @@
+using CairoMakie
+using Statistics
+
+# ========== 1. Prepare data in "long" format ==========
+# Each row (scale, n, perf) is one sample.
+
+scales = Int[]
+ns     = Int[]
+perfs  = Float64[]
+
+# Helper function to add data for one (scale, n)
+function add_data!(scales, ns, perfs, scale::Int, n::Int, values::Vector{<:Real})
+    for v in values
+        push!(scales, scale)
+        push!(ns, n)
+        push!(perfs, float(v))
+    end
+end
+
+# --------- Fill your data here ---------
+# scale = 16
+data1 = [100, 76, 56, 24, 88, 82, 99, 47, 28, 45, 54, 64, 53, 62, 29, 31, 69, 69, 16, 37]
+data2 = [62, 8, 50, 34, 23, 49, 41, 21, 23, 44, 40, 18, 30, 30, 16, 49, 58, 58, 29, 20]
+data3 = [50, 11, 29, 28, 31, 67, 42, 38, 31, 43, 46, 11, 41, 23, 17, 30, 37, 37, 30, 22]
+data4 = [55, 9, 15, 22, 16, 49, 58, 34, 25, 38, 45, 12, 35, 24, 28, 15, 44, 44, 31, 17]
+data5 = [40, 31, 41, 24, 11, 40, 35, 17, 18, 32, 19, 12, 15, 24, 21, 16, 33, 33, 39, 20]
+add_data!(scales, ns, perfs, 16, 1, data1)          # n = 1: 100, 76, ...
+add_data!(scales, ns, perfs, 16, 2, data2)            # n = 2: 62, 8, ...
+add_data!(scales, ns, perfs, 16, 3, data3)           # n = 3: 50, 11, ...
+add_data!(scales, ns, perfs, 16, 4, data4)            # n = 4: 55, 9, ...
+add_data!(scales, ns, perfs, 16, 5, data5)           # n = 5: 40, 31, ...
+
+#kissat
+kissat16 = [49, 36, 18, 80, 14, 85, 10, 24, 47, 0, 0, 3, 3, 36, 0, 44, 7, 7, 25, 14]
+minisat16 = [62, 61, 40, 70, 52, 96, 89, 36, 76, 6, 10, 61, 43, 155, 74, 11, 73, 73, 15, 77]
+
+# scale = 20
+data1 = [130, 158, 230, 79, 83, 189, 103, 352, 31, 106, 143, 199, 64, 63, 133, 150, 36, 176, 29, 43]
+data2 = [124, 136, 238, 69, 53, 94, 98, 158, 35, 287, 76, 130, 257, 48, 68, 82, 31, 113, 29, 36]
+data3 = [113, 130, 134, 160, 52, 46, 55, 158, 53, 54, 107, 153, 255, 69, 85, 40, 34, 146, 69, 39]
+data4 = [138, 172, 69, 119, 30, 89, 45, 154, 37, 269, 157, 137, 181, 44, 25, 37, 30, 76, 52, 45]
+data5 = [243, 125, 172, 48, 25, 30, 86, 105, 38, 142, 126, 115, 48, 39, 58, 46, 27, 55, 24, 25]
+add_data!(scales, ns, perfs, 20, 1, data1)         # n = 1: 130, 158, ...
+add_data!(scales, ns, perfs, 20, 2, data2)         # n = 2: 124, 136, ...
+add_data!(scales, ns, perfs, 20, 3, data3)         # n = 3: 113, 130, ...
+add_data!(scales, ns, perfs, 20, 4, data4)         # n = 4: 138, 172, ...
+add_data!(scales, ns, perfs, 20, 5, data5)         # n = 5: 243, 125, ...
+
+# kissat
+kissat20 = [37, 20, 0, 557, 67, 27, 352, 35, 239, 239, 62, 593, 291, 195, 38, 0, 492, 39, 309, 485]
+minisat20 = [111, 157, 343, 273, 165, 217, 312, 239, 31, 510, 79, 731, 323, 106, 73, 30, 429, 30, 362, 109]
+
+# scale = 24
+data1 = [1243, 3932, 1068, 1054, 94, 383, 852, 363, 1382, 700, 1798, 125, 138, 47, 1860, 982, 194, 2083, 1878, 615]
+data2 = [612, 1030, 1520, 709, 480, 361, 602, 341, 1012, 865, 1373, 93, 79, 50, 355, 790, 158, 1352, 925, 404]
+data3 = [313, 1861, 1229, 234, 54, 165, 604, 66, 381, 949, 994, 99, 56, 49, 348, 734, 548, 1108, 459, 498]
+data4 = [348, 2002, 253, 723, 94, 303, 434, 56, 249, 858, 1015, 51, 55, 61, 355, 39, 66, 1022, 490, 334]
+data5 = [216, 962, 577, 411, 84, 378, 249, 45, 64, 403, 545, 33, 297, 55, 330, 256, 119, 1816, 1177, 522]
+add_data!(scales, ns, perfs, 24, 1, data1)         # n = 1: 1243, 3932, ...
+add_data!(scales, ns, perfs, 24, 2, data2)         # n = 2: 612, 1030, ...
+add_data!(scales, ns, perfs, 24, 3, data3)         # n = 3: 313, 1861, ...
+add_data!(scales, ns, perfs, 24, 4, data4)
+add_data!(scales, ns, perfs, 24, 5, data5)
+
+#kissat
+kissat24 = [538, 2414, 62, 335, 395, 1226, 22, 0, 546, 1788, 2724, 343, 1733, 2227, 2381, 1982, 2136, 2784, 1913, 1006]
+minisat24 = [716, 1758, 843, 1175, 627, 712, 282, 280, 89, 320, 1983, 88, 1605, 1843, 1097, 1123, 470, 362, 1109, 1342]
+
+# ========== 2. Make a faceted boxplot by scale ==========
+
+baseline_dict = Dict(
+    16 => [mean(kissat16), mean(minisat16)],      # baseline 1 & baseline 2 for scale 16
+    20 => [mean(kissat20), mean(minisat20)],    # baseline 1 & baseline 2 for scale 20
+    24 => [mean(kissat24), mean(minisat24)],    # baseline 1 & baseline 2 for scale 24
+)
+
+unique_scales = sort(unique(scales))
+n_scales = length(unique_scales)
+
+colors = [:red, :blue, :green, :orange, :purple]
+linestyles = [:dash, :dot, :dashdot, :dash, :dot]
+
+# Adjust resolution depending on how many scales you have
+fig = Figure(resolution = (350 * n_scales, 400))
+
+for (i, sc) in enumerate(unique_scales)
+    ax = Axis(fig[1, i];
+        title  = "Bit length = $sc",
+        xlabel = "Region size n",
+        ylabel = "Branch number"
+    )
+
+    # Select data for this scale
+    idx = findall(j -> scales[j] == sc, eachindex(scales))
+    xs  = ns[idx]      # n values (group variable)
+    ys  = perfs[idx]   # performance values
+
+    # Boxplot: group by xs, values = ys
+    boxplot!(ax, xs, ys)
+
+    xleft, xright = 0.5, maximum(xs) + 0.5
+
+    for (bi, b) in enumerate(baseline_dict[sc])
+        lines!(
+            ax,
+            [xleft, xright], [b, b]; 
+            color     = colors[(bi - 1) % length(colors) + 1],
+            linestyle = linestyles[(bi - 1) % length(linestyles) + 1],
+            linewidth = 2
+        )
+    end
+
+    # Nice x ticks: only show n that appear in this scale
+    unique_ns = sort(unique(xs))
+    ax.xticks = (unique_ns, string.(unique_ns))
+end
+
+save("boxplot_region.png", fig)
+fig
+