Refactor to use native interfaces in OptimalBranching.jl

.gitignore

@@ -1,10 +1,24 @@
+# Julia
 *.jl.*.cov
 *.jl.cov
 *.jl.mem
 /Manifest.toml
-/docs/Manifest.toml
-/docs/build/
+
+# Benchmark data
+benchmarks/data/
+benchmarks/Manifest.toml
+
+# IDE
 .vscode/
-backup/
-datas/
-.DS_Store
+.idea/
+
+# OS
+.DS_Store
+Thumbs.db
+
+# Temporary files
+*.tmp
+*.temp
+
+statprof/
+OptimalBranching.jl/

Project.toml

@@ -1,29 +1,24 @@
 name = "BooleanInference"
 uuid = "d12a6243-8379-43cb-9459-098119da1519"
-authors = ["nzy1997"]
 version = "1.0.0-DEV"
+authors = ["nzy1997"]
 
 [deps]
+DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
 GenericTensorNetworks = "3521c873-ad32-4bb4-b63d-f4f178f42b49"
-HiGHS = "87dc4568-4c63-4d18-b0c0-bb2238e4078b"
-JuMP = "4076af6c-e467-56ae-b986-b466b2749572"
-KaHyPar = "2a6221f6-aa48-11e9-3542-2d9e0ef01880"
 OptimalBranchingCore = "c76e7b22-e1d2-40e8-b0f1-f659837787b8"
-Primes = "27ebfcd6-29c5-5fa9-bf4b-fb8fc14df3ae"
 ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
 SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf"
 TropicalNumbers = "b3a74e9c-7526-4576-a4eb-79c0d4c32334"
 
 [compat]
-GenericTensorNetworks = "3"
-HiGHS = "1.12.2"
-JuMP = "1.23.5"
-KaHyPar = "0.3.1"
+DataStructures = "0.18.22"
+GenericTensorNetworks = "4"
 OptimalBranchingCore = "0.1"
-Primes = "0.5.6"
+ProblemReductions = "0.3.5"
 SparseArrays = "1.11.0"
 TropicalNumbers = "0.6.2"
-julia = "1.11"
+julia = "1"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

README.md

@@ -1,6 +1,114 @@
-# BooleanInference
+# BooleanInference.jl
 
 [![Stable](https://img.shields.io/badge/docs-stable-blue.svg)](https://nzy1997.github.io/BooleanInference.jl/stable/)
 [![Dev](https://img.shields.io/badge/docs-dev-blue.svg)](https://nzy1997.github.io/BooleanInference.jl/dev/)
 [![Build Status](https://github.com/nzy1997/BooleanInference.jl/actions/workflows/CI.yml/badge.svg?branch=main)](https://github.com/nzy1997/BooleanInference.jl/actions/workflows/CI.yml?query=branch%3Amain)
 [![Coverage](https://codecov.io/gh/nzy1997/BooleanInference.jl/branch/main/graph/badge.svg)](https://codecov.io/gh/nzy1997/BooleanInference.jl)
+
+A high-performance Julia package for solving Boolean satisfiability problems using tensor network contraction and optimal branching strategies.
+
+## Features
+
+- **Tensor Network Representation**: Efficiently represents Boolean satisfiability problems as tensor networks
+- **Optimal Branching**: Uses advanced branching strategies to minimize search space
+- **Multiple Problem Types**: Supports CNF, circuit, and factoring problems
+- **High Performance**: Optimized for speed with efficient propagation and contraction algorithms
+- **Flexible Interface**: Easy-to-use API for various constraint satisfaction problems
+
+## Installation
+
+```julia
+using Pkg
+Pkg.add("BooleanInference")
+```
+
+## Quick Start
+
+### Solving SAT Problems
+
+```julia
+using BooleanInference
+using GenericTensorNetworks: ∧, ∨, ¬
+
+# Define a CNF formula
+@bools a b c d e f g
+cnf = ∧(∨(a, b, ¬d, ¬e), ∨(¬a, d, e, ¬f), ∨(f, g), ∨(¬b, c), ∨(¬a))
+
+# Solve and get assignments
+sat = Satisfiability(cnf; use_constraints=true)
+satisfiable, assignments, depth = solve_sat_with_assignments(sat)
+
+println("Satisfiable: ", satisfiable)
+println("Assignments: ", assignments)
+```
+
+### Solving Factoring Problems
+
+```julia
+# Factor a semiprime number
+a, b = solve_factoring(5, 5, 31*29)
+println("Factors: $a × $b = $(a*b)")
+```
+
+### Circuit Problems
+
+```julia
+# Solve circuit satisfiability
+circuit = @circuit begin
+    c = x ∧ y
+end
+push!(circuit.exprs, Assignment([:c], BooleanExpr(true)))
+
+tnproblem = setup_from_circuit(circuit)
+result, depth = solve(tnproblem, BranchingStrategy(), NoReducer())
+```
+
+## Core Components
+
+### Problem Types
+- `TNProblem`: Main problem representation
+- `TNStatic`: Static problem structure
+- `DomainMask`: Variable domain representation
+
+### Solvers
+- `TNContractionSolver`: Tensor network contraction-based solver
+- `LeastOccurrenceSelector`: Variable selection strategy
+- `NumUnfixedVars`: Measurement strategy
+
+### Key Functions
+- `solve()`: Main solving function
+- `setup_from_cnf()`: Setup from CNF formulas
+- `setup_from_circuit()`: Setup from circuit descriptions
+- `solve_factoring()`: Solve integer factoring problems
+
+## Advanced Usage
+
+### Custom Branching Strategy
+
+```julia
+using OptimalBranchingCore: BranchingStrategy
+
+# Configure custom solver
+bsconfig = BranchingStrategy(
+    table_solver=TNContractionSolver(),
+    selector=LeastOccurrenceSelector(2, 10),
+    measure=NumUnfixedVars()
+)
+
+# Solve with custom configuration
+result, depth = solve(problem, bsconfig, NoReducer())
+```
+
+### Benchmarking
+
+The package includes comprehensive benchmarking tools:
+
+```julia
+using BooleanInferenceBenchmarks
+
+# Compare different solvers
+configs = [(10,10), (12,12), (14,14)]
+results = run_solver_comparison(FactoringProblem, configs)
+print_solver_comparison_summary(results)
+```
+

benchmarks/Project.toml

@@ -0,0 +1,27 @@
+name = "BooleanInferenceBenchmarks"
+uuid = "3611a03f-6421-4259-a011-a603192356a0"
+version = "0.1.0"
+authors = ["Xiwei Pan <xiwei.pan@connect.hkust-gz.edu.cn>"]
+
+[deps]
+BenchmarkTools = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf"
+BooleanInference = "d12a6243-8379-43cb-9459-098119da1519"
+Dates = "ade2ca70-3891-5945-98fb-dc099432e06a"
+Gurobi = "2e9cd046-0924-5485-92f1-d5272153d98b"
+JSON3 = "0f8b85d8-7281-11e9-16c2-39a750bddbf1"
+JuMP = "4076af6c-e467-56ae-b986-b466b2749572"
+Primes = "27ebfcd6-29c5-5fa9-bf4b-fb8fc14df3ae"
+ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
+Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
+SHA = "ea8e919c-243c-51af-8825-aaa63cd721ce"
+Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
+
+[compat]
+BenchmarkTools = "1.6.0"
+Dates = "1.11.0"
+Gurobi = "1.7.6"
+JSON3 = "1.14.3"
+JuMP = "1.29.1"
+ProblemReductions = "0.3.5"
+Random = "1.11.0"
+Statistics = "1.11.1"

benchmarks/README.md

@@ -0,0 +1,106 @@
+# BooleanInference Benchmarks
+
+This directory contains benchmarking code for BooleanInference.jl, organized as a separate Julia package with a modern **multiple dispatch architecture** to keep benchmark dependencies isolated from the main package.
+
+## Architecture
+
+The benchmark system uses Julia's **multiple dispatch** with abstract types to provide a clean, extensible interface for different problem types.
+
+## Structure
+
+```text
+benchmark/
+├── Project.toml              # Benchmark package dependencies
+├── src/
+│   ├── BooleanInferenceBenchmarks.jl  # Main benchmark module
+│   ├── abstract_types.jl     # Abstract type definitions and interfaces
+│   ├── generic_benchmark.jl  # Generic benchmark framework
+│   ├── factoring_problem.jl  # Factoring problem implementation
+│   └── utils.jl              # Generic utilities
+├── scripts/
+│   ├── run_benchmarks.jl     # Standalone benchmark runner
+│   └── example_usage.jl      # Usage examples
+├── data/                     # Generated datasets (gitignored)
+└── README.md                 # This file
+```
+
+## Usage
+
+### Quick Start
+
+```bash
+# Run example usage
+julia --project=benchmark benchmark/scripts/example_usage.jl
+```
+
+### Programmatic Usage
+
+```julia
+using Pkg; Pkg.activate("benchmark")
+using BooleanInferenceBenchmarks
+
+# Create problem configurations
+configs = [FactoringConfig(10, 10), FactoringConfig(12, 12)]
+
+# Generate datasets using multiple dispatch
+generate_datasets(FactoringProblem; configs=configs, per_config=100)
+
+# Run benchmarks using multiple dispatch
+results = benchmark_problem(FactoringProblem; configs=configs, samples_per_config=5)
+
+# Run complete benchmark suite
+full_results = run_full_benchmark(FactoringProblem)
+```
+
+## Adding New Problem Types
+
+The multiple dispatch architecture makes adding new problem types extremely simple:
+
+```julia
+# 1. Define problem and config types
+struct YourProblem <: AbstractBenchmarkProblem end
+struct YourConfig <: AbstractProblemConfig
+    param1::Int
+    param2::String
+end
+
+# 2. Implement the 5 required interface methods
+function generate_instance(::Type{YourProblem}, config::YourConfig; rng, include_solution=false)
+    # Generate problem instance
+end
+
+function solve_instance(::Type{YourProblem}, instance)
+    # Solve the instance
+end
+
+function problem_id(::Type{YourProblem}, config::YourConfig, data)
+    # Generate unique ID
+end
+
+function default_configs(::Type{YourProblem})
+    # Return default configurations
+end
+
+function filename_pattern(::Type{YourProblem}, config::YourConfig)
+    # Generate filename pattern
+end
+
+# 3. That's it! Use the same generic functions:
+generate_datasets(YourProblem)
+benchmark_problem(YourProblem)
+run_full_benchmark(YourProblem)
+```
+
+## Key Advantages
+
+- **DRY Principle**: Write benchmark logic once, use for all problem types
+- **Type Safety**: Julia's type system catches errors at compile time
+- **Extensibility**: Adding new problems requires minimal code
+- **Consistency**: All problem types use the same interface
+- **Performance**: Multiple dispatch enables efficient, optimized code
+
+## Data Management
+
+- Datasets are generated in `benchmark/data/`
+- Add `benchmark/data/` to `.gitignore` to avoid committing large files
+- Use JSONL format for datasets (one JSON object per line)

benchmarks/examples/run_benchmarks.jl

@@ -0,0 +1,70 @@
+# Comprehensive solver comparison benchmark script
+# Demonstrates both automatic and manual solver comparison approaches
+# Usage: julia --project=benchmark benchmark/examples/run_benchmarks.jl
+
+using Pkg
+Pkg.activate(joinpath(@__DIR__, ".."))
+
+using BooleanInferenceBenchmarks
+
+using Gurobi
+const GUROBI_ENV = Gurobi.Env()
+
+function main()
+	println("Running BooleanInference Solver Comparison Benchmarks...")
+
+	# Show available solvers
+	println("\nAvailable solvers:")
+	list_available_solvers(FactoringProblem)
+
+	# Configure benchmark parameters
+	configs = [(10,10), (12,12), (14,14)] 
+	dataset_per_config = 10
+
+	println("\nComparing BooleanInference vs IP Solver...")
+	println("Configurations: $configs")
+	println("Instances per config: $dataset_per_config")
+
+	# Option 1: Automatic comparison of all available solvers
+	# println("\n=== Automatic Solver Comparison (All Available Solvers) ===")
+	all_results = run_solver_comparison(FactoringProblem, configs; 
+	                                  dataset_per_config=dataset_per_config)
+
+	# Print beautiful comparison table
+	print_solver_comparison_summary(all_results)
+	# Persist comparison results
+	save_solver_comparison(FactoringProblem, all_results; note="demo run")
+
+	# # Option 2: Manual head-to-head comparison for detailed analysis
+	# println("\n=== Head-to-Head Comparison (Detailed Analysis) ===")
+
+	# # Test BooleanInference solver
+	# println("Benchmarking BooleanInference solver...")
+	# bi_results = run_full_benchmark(FactoringProblem, configs;
+	#                                dataset_per_config=dataset_per_config, 
+	#                                solver=BooleanInferenceSolver())
+
+	# # Test IP solver
+	# println("Benchmarking IP solver...")
+	# ip_results = run_full_benchmark(FactoringProblem, configs;
+	#                                dataset_per_config=dataset_per_config,
+	#                                solver=IPSolver(Gurobi.Optimizer, GUROBI_ENV))
+
+	# # Side-by-side comparison
+	# println("\nHead-to-Head Results:")
+	# compare_solver_results("BooleanInference", bi_results, "IP-Gurobi", ip_results)
+
+	# println("\nAll benchmarks completed!")
+	# println("Datasets cached in: benchmarks/data/factoring/")
+	# println("Results saved in: benchmarks/data/factoring_benchmark_results.json")
+
+	# println("\nFor quick one-liner comparisons, you can also use:")
+	# println("   # Compare all solvers automatically:")
+	# println("   run_solver_comparison(FactoringProblem, [(10,10)])")
+	# println("   # Or test a specific solver:")
+	# println("   run_full_benchmark(FactoringProblem, [(10,10)]; solver=BooleanInferenceSolver())")
+end
+
+if abspath(PROGRAM_FILE) == @__FILE__
+	main()
+end