Refactor

.gitignore

@@ -33,9 +33,11 @@ OptimalBranching.jl/
 /benchmarks/third-party/**/build/
 /benchmarks/third-party/**/bin/
 /benchmarks/third-party/**/CMakeFiles/
-/benchmarks/third-party/**/Makefile
 /benchmarks/third-party/**/cmake_install.cmake
+/benchmarks/third-party/**/build/**
 
 # === Logs ===
 *.log
-*.out
+*.out
+*.history
+/discs/

.gitmodules

@@ -13,4 +13,8 @@
 [submodule "benchmarks/third-party/CnC"]
 	path = benchmarks/third-party/CnC
 	url = https://github.com/marijnheule/CnC.git
-	ignore = all
+	ignore = all
+[submodule "benchmarks/third-party/cir_bench"]
+	path = benchmarks/third-party/cir_bench
+	url = https://github.com/santoshsmalagi/Benchmarks.git
+	ignore = all

Project.toml

@@ -4,17 +4,33 @@ version = "1.0.0-DEV"
 authors = ["nzy1997"]
 
 [deps]
+BitBasis = "50ba71b6-fa0f-514d-ae9a-0916efc90dcf"
+CairoMakie = "13f3f980-e62b-5c42-98c6-ff1f3baf88f0"
+Colors = "5ae59095-9a9b-59fe-a467-6f913c188581"
+Compose = "a81c6b42-2e10-5240-aca2-a61377ecd94b"
 DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
 GenericTensorNetworks = "3521c873-ad32-4bb4-b63d-f4f178f42b49"
+GraphMakie = "1ecd5474-83a3-4783-bb4f-06765db800d2"
+GraphPlot = "a2cc645c-3eea-5389-862e-a155d0052231"
+Graphs = "86223c79-3864-5bf0-83f7-82e725a168b6"
+NetworkLayout = "46757867-2c16-5918-afeb-47bfcb05e46a"
 OptimalBranchingCore = "c76e7b22-e1d2-40e8-b0f1-f659837787b8"
 ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
 SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"
 Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
 TropicalNumbers = "b3a74e9c-7526-4576-a4eb-79c0d4c32334"
 
 [compat]
+BitBasis = "0.9.10"
+CairoMakie = "0.15.6"
+Colors = "0.13.1"
+Compose = "0.9.6"
 DataStructures = "0.18.22"
 GenericTensorNetworks = "4"
+GraphMakie = "0.6.3"
+GraphPlot = "0.6.2"
+Graphs = "1.13.1"
+NetworkLayout = "0.4.10"
 OptimalBranchingCore = "0.1"
 ProblemReductions = "0.3.5"
 SparseArrays = "1.11.0"

README.md

@@ -67,7 +67,7 @@ result, depth = solve(tnproblem, BranchingStrategy(), NoReducer())
 
 ### Problem Types
 - `TNProblem`: Main problem representation
-- `TNStatic`: Static problem structure
+- `BipartiteGraph`: Static problem structure
 - `DomainMask`: Variable domain representation
 
 ### Solvers

benchmarks/Project.toml

@@ -11,6 +11,7 @@ Gurobi = "2e9cd046-0924-5485-92f1-d5272153d98b"
 HiGHS = "87dc4568-4c63-4d18-b0c0-bb2238e4078b"
 JSON3 = "0f8b85d8-7281-11e9-16c2-39a750bddbf1"
 JuMP = "4076af6c-e467-56ae-b986-b466b2749572"
+OptimalBranchingCore = "c76e7b22-e1d2-40e8-b0f1-f659837787b8"
 Primes = "27ebfcd6-29c5-5fa9-bf4b-fb8fc14df3ae"
 ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
 Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
@@ -24,6 +25,7 @@ Gurobi = "1.7.6"
 HiGHS = "1.19.3"
 JSON3 = "1.14.3"
 JuMP = "1.29.1"
+OptimalBranchingCore = "0.1.5"
 ProblemReductions = "0.3.5"
 Random = "1.11.0"
 Statistics = "1.11.1"

benchmarks/examples/circuitsat_example.jl

@@ -0,0 +1,96 @@
+# Example: CircuitSAT Benchmarking with Verilog and AAG files
+
+using Pkg
+Pkg.activate(joinpath(@__DIR__, ".."))
+
+using BooleanInferenceBenchmarks
+using BooleanInference
+
+# # Example 1: Benchmark a single Verilog file
+# println("="^60)
+# println("Example 1: Benchmark Single Verilog File (c17)")
+# println("="^60)
+
+# c17_path = joinpath(@__DIR__, "..", "data", "iscas85", "c17.v")
+# result = benchmark_dataset(CircuitSATProblem, c17_path)
+
+# if result !== nothing
+#     println("\nResults:")
+#     println("  Instances tested: ", result["instances_tested"])
+#     println("  Successful runs: ", result["successful_runs"])
+#     println("  Accuracy rate: ", round(result["accuracy_rate"] * 100, digits=2), "%")
+#     println("  Median time: ", round(result["median_time"], digits=6), " seconds")
+# end
+# println()
+
+c3540_path = joinpath(@__DIR__, "..", "data", "aig", "non-arithmetic", "c3540.aag")
+result = benchmark_dataset(CircuitSATProblem, c3540_path)
+
+if result !== nothing
+    println("\nResults:")
+    println("  Instances tested: ", result["instances_tested"])
+    println("  Successful runs: ", result["successful_runs"])
+    println("  Accuracy rate: ", round(result["accuracy_rate"] * 100, digits=2), "%")
+    println("  Median time: ", round(result["median_time"], digits=6), " seconds")
+end
+println()
+
+# Example 2: Benchmark ISCAS85 directory (all Verilog files)
+println("="^60)
+println("Example 2: Benchmark ISCAS85 Dataset")
+println("="^60)
+
+iscas85_dir = joinpath(@__DIR__, "..", "data", "iscas85")
+result = benchmark_dataset(CircuitSATProblem, iscas85_dir)
+
+if result !== nothing
+    println("\nResults:")
+    println("  Instances tested: ", result["instances_tested"])
+    println("  Successful runs: ", result["successful_runs"])
+    println("  Accuracy rate: ", round(result["accuracy_rate"] * 100, digits=2), "%")
+    println("  Median time: ", round(result["median_time"], digits=6), " seconds")
+end
+println()
+
+# Example 3: Benchmark AAG files (if available)
+println("="^60)
+println("Example 3: Benchmark AAG Dataset")
+println("="^60)
+
+aag_dir = joinpath(@__DIR__, "..", "data", "aig", "non-arithmetic")
+if isdir(aag_dir)
+    result = benchmark_dataset(CircuitSATProblem, aag_dir)
+
+    if result !== nothing
+        println("\nResults:")
+        println("  Instances tested: ", result["instances_tested"])
+        println("  Successful runs: ", result["successful_runs"])
+        println("  Accuracy rate: ", round(result["accuracy_rate"] * 100, digits=2), "%")
+        println("  Median time: ", round(result["median_time"], digits=6), " seconds")
+    end
+else
+    println("AAG directory not found: $aag_dir")
+end
+println()
+
+# # Example 4: Discover available circuits
+# println("="^60)
+# println("Example 4: Discover Available Circuits")
+# println("="^60)
+
+# verilog_files = discover_circuit_files(iscas85_dir; format=:verilog)
+# println("Found $(length(verilog_files)) Verilog circuits:")
+# for (i, file) in enumerate(verilog_files)
+#     println("  $i. ", basename(file))
+# end
+
+# if isdir(aag_dir)
+#     aag_files = discover_circuit_files(aag_dir; format=:aag)
+#     println("\nFound $(length(aag_files)) AAG circuits")
+# end
+# println()
+
+println("="^60)
+println("Examples completed!")
+println("="^60)
+

benchmarks/examples/cnfsat_example.jl

@@ -0,0 +1,25 @@
+using Pkg
+Pkg.activate(joinpath(@__DIR__, ".."))
+
+using BooleanInferenceBenchmarks
+using ProblemReductions
+
+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 = benchmark_dataset(
+    CNFSATProblem,
+    dataset_path;
+    solver=BooleanInferenceSolver(),
+    verify=true
+)
+
+test_file = joinpath(dataset_path, "3sat1.cnf")
+test_instance = parse_cnf_file(test_file)
+result = solve_instance(CNFSATProblem, test_instance, BooleanInferenceSolver())
+@show result

benchmarks/examples/factoring_example.jl

@@ -3,8 +3,8 @@ Pkg.activate(joinpath(@__DIR__, ".."))
 
 using BooleanInferenceBenchmarks
 using Random
-using Gurobi
 
+using Gurobi
 const env = Gurobi.Env()
 
 # ----------------------------------------
@@ -18,11 +18,11 @@ println("=" ^80)
 configs = [
     # FactoringConfig(10, 10),
     # FactoringConfig(12, 12),
-    # FactoringConfig(14, 14),
+    FactoringConfig(14, 14),
     # FactoringConfig(16, 16),
     # FactoringConfig(18, 18),
     # FactoringConfig(20, 20),
-    FactoringConfig(22, 22),
+    # FactoringConfig(22, 22),
     # FactoringConfig(24, 24)
 ]
 
@@ -56,7 +56,8 @@ println("Comparing Solvers")
 println("=" ^80)
 
 # results = run_solver_comparison(FactoringProblem, paths, solvers=[XSATSolver(;yosys_path="/opt/homebrew/bin/yosys"), BooleanInferenceSolver()])
-# results = run_solver_comparison(FactoringProblem, paths, solvers=[XSATSolver(;yosys_path="/opt/homebrew/bin/yosys")])
-results = run_solver_comparison(FactoringProblem, paths, solvers=[BooleanInferenceSolver()])
+# results = run_solver_comparison(FactoringProblem, paths, solvers=[XSATSolver(;yosys_path="/opt/homebrew/bin/yosys", timeout=600.0)])
+# results = run_solver_comparison(FactoringProblem, paths, solvers=[KissatSolver(kissat_path="/opt/homebrew/bin/kissat", timeout=300.0), MinisatSolver(minisat_path="/opt/homebrew/bin/minisat", timeout=300.0)])
+results = run_solver_comparison(FactoringProblem, paths, solvers=[IPSolver(Gurobi.Optimizer, env)])
 print_solver_comparison_summary(results)
 

benchmarks/src/BooleanInferenceBenchmarks.jl

@@ -11,6 +11,8 @@ using Statistics: mean, median
 using SHA: bytes2hex, sha256, sha1
 using ProblemReductions
 using ProblemReductions: Factoring, CircuitSAT, reduceto, constraints, objectives, AbstractProblem, Symbol
+using ProblemReductions: BoolVar, CNFClause, CNF, Satisfiability
+using OptimalBranchingCore
 
 include("abstract_types.jl")
 include("utils.jl")
@@ -22,22 +24,46 @@ include("comparison.jl")
 include("circuitIO/circuitIO.jl")
 using .CircuitIO
 
+include("solver/solver_ip.jl")
+include("solver/solver_xsat.jl")
+include("solver/solver_cnfsat.jl")
+
 # Factoring problem
 include("factoring/types.jl")
 include("factoring/interface.jl")
 include("factoring/generators.jl")
-include("factoring/solver_ip.jl")
 include("factoring/solvers.jl")
 include("factoring/dataset.jl")
-include("factoring/solver_xsat.jl")
+
+# CircuitSAT problem
+include("circuitSAT/types.jl")
+include("circuitSAT/interface.jl")
+include("circuitSAT/dataset.jl")
+include("circuitSAT/solvers.jl")
+
+# CNFSAT problem
+include("CNFSAT/types.jl")
+include("CNFSAT/parser.jl")
+include("CNFSAT/dataset.jl")
+include("CNFSAT/interface.jl")
+include("CNFSAT/solvers.jl")
 
 export AbstractBenchmarkProblem, AbstractProblemConfig, AbstractInstance, AbstractSolver
-export solve_instance, verify_solution, read_instances
-export available_solvers, default_solver, solver_name
+export solve_instance, verify_solution, read_instances, generate_instance
+export available_solvers, default_solver, solver_name, problem_id
 export benchmark_dataset, run_solver_comparison
 export list_available_solvers, print_solver_comparison_summary, compare_solver_results
 export FactoringProblem, FactoringConfig, FactoringInstance, generate_factoring_datasets
 export CircuitSATProblem, CircuitSATConfig, CircuitSATInstance
+export load_circuit_instance, load_verilog_dataset, load_aag_dataset
+export load_circuit_datasets, discover_circuit_files, create_circuitsat_configs
+export is_satisfiable
 export BooleanInferenceSolver, IPSolver, XSATSolver
+export CNFSolver, KissatSolver, MinisatSolver
+export CNFSolverResult, run_cnf_solver
+export CNFSATProblem, CNFSATConfig, CNFSATInstance
+export parse_cnf_file, cnf_instantiation
+export load_cnf_dataset, load_cnf_datasets, discover_cnf_files, create_cnfsat_configs
+export load_cnf_instance, is_cnf_satisfiable
 
 end

benchmarks/src/CNFSAT/dataset.jl

@@ -0,0 +1,69 @@
+# Dataset management for CNF SAT benchmarks
+
+"""
+    discover_cnf_files(dir::String)
+
+Recursively discover CNF files (*.cnf) in a directory.
+"""
+function discover_cnf_files(dir::String)
+    files = String[]
+
+    for (root, dirs, filenames) in walkdir(dir)
+        for filename in filenames
+            if endswith(filename, ".cnf")
+                push!(files, joinpath(root, filename))
+            end
+        end
+    end
+
+    sort!(files)
+    return files
+end
+
+"""
+    create_cnfsat_configs(files::Vector{String})
+
+Create CNFSATConfig objects from a list of CNF files.
+"""
+function create_cnfsat_configs(files::Vector{String})
+    return [CNFSATConfig(path) for path in files]
+end
+
+"""
+    load_cnf_dataset(dir::String)
+
+Load all CNF files from a directory and create configs.
+"""
+function load_cnf_dataset(dir::String)
+    files = discover_cnf_files(dir)
+    @info "Found $(length(files)) CNF files in $dir"
+    return create_cnfsat_configs(files)
+end
+
+"""
+    load_cnf_datasets(dirs::Vector{String})
+
+Load CNF datasets from multiple directories.
+
+# Example
+```julia
+configs = load_cnf_datasets([
+    "benchmarks/third-party/CnC/tests",
+    "data/sat-competition"
+])
+```
+"""
+function load_cnf_datasets(dirs::Vector{String})
+    configs = CNFSATConfig[]
+
+    for dir in dirs
+        if isdir(dir)
+            append!(configs, load_cnf_dataset(dir))
+        else
+            @warn "Directory not found: $dir"
+        end
+    end
+
+    @info "Total $(length(configs)) CNF configs loaded"
+    return configs
+end