Merge pull request #26 from OptimalBranching/xw/hybrid

Update CDCL-hybrid solver

Author: isPANN

.github/workflows/CI.yml

@@ -31,11 +31,15 @@ jobs:
           - x64
     steps:
       - uses: actions/checkout@v6
+        with:
+          submodules: recursive
       - uses: julia-actions/setup-julia@v2
         with:
           version: ${{ matrix.version }}
           arch: ${{ matrix.arch }}
       - uses: julia-actions/cache@v2
+      - name: Build CaDiCaL dependency
+        run: make
       - uses: julia-actions/julia-buildpkg@v1
       - uses: julia-actions/julia-runtest@v1
       - uses: julia-actions/julia-processcoverage@v1
@@ -53,10 +57,14 @@ jobs:
       statuses: write
     steps:
       - uses: actions/checkout@v6
+        with:
+          submodules: recursive
       - uses: julia-actions/setup-julia@v2
         with:
           version: '1'
       - uses: julia-actions/cache@v2
+      - name: Build CaDiCaL dependency
+        run: make
       - name: Configure doc environment
         shell: julia --project=docs --color=yes {0}
         run: |

.gitignore

@@ -24,9 +24,9 @@ Thumbs.db
 *.swo
 
 statprof/
-OptimalBranching.jl/
 .julia/
 .claude/
+.history/
 
 # === Build outputs ===
 /benchmarks/artifacts/
@@ -43,4 +43,8 @@ OptimalBranching.jl/
 /discs/
 /notes/
 
-/benchmarks/results/
+/benchmarks/results/
+*.dylib
+*.o
+*.so
+*.dll

.gitmodules

@@ -18,3 +18,7 @@
 	path = benchmarks/third-party/cir_bench
 	url = https://github.com/santoshsmalagi/Benchmarks.git
 	ignore = all
+[submodule "deps/cadical"]
+	path = deps/cadical
+	url = https://github.com/arminbiere/cadical.git
+	ignore = all

Makefile

@@ -0,0 +1,45 @@
+# BooleanInference Makefile
+# This Makefile handles building the CaDiCaL dependency and the custom library
+
+.PHONY: all submodule cadical mylib clean clean-all help
+
+# Default target
+all: mylib
+
+# Help message
+help:
+	@echo "Available targets:"
+	@echo "  all        - Build everything (default)"
+	@echo "  submodule  - Initialize and update git submodules"
+	@echo "  cadical    - Build the CaDiCaL library"
+	@echo "  mylib      - Build the custom CaDiCaL wrapper library"
+	@echo "  clean      - Clean the custom library"
+	@echo "  clean-all  - Clean everything including CaDiCaL build"
+
+# Update git submodules
+submodule:
+	git submodule update --init --recursive
+
+# Build CaDiCaL
+cadical: submodule
+	@echo "Building CaDiCaL..."
+	cd deps/cadical && \
+	  make clean || true && \
+	  export CFLAGS="-fPIC" CXXFLAGS="-fPIC" && \
+	  ./configure && \
+	  $(MAKE) -j4 CFLAGS="-fPIC" CXXFLAGS="-fPIC"
+
+# Build the custom library (depends on CaDiCaL)
+mylib: cadical
+	@echo "Building custom CaDiCaL wrapper..."
+	$(MAKE) -C src/cdcl
+
+# Clean custom library only
+clean:
+	$(MAKE) -C src/cdcl clean
+
+# Clean everything
+clean-all: clean
+	@echo "Cleaning CaDiCaL build..."
+	cd deps/cadical && make clean 2>/dev/null || true
+	rm -rf deps/cadical/build

Project.toml

@@ -7,13 +7,15 @@ authors = ["nzy1997"]
 BitBasis = "50ba71b6-fa0f-514d-ae9a-0916efc90dcf"
 CairoMakie = "13f3f980-e62b-5c42-98c6-ff1f3baf88f0"
 Colors = "5ae59095-9a9b-59fe-a467-6f913c188581"
+Combinatorics = "861a8166-3701-5b0c-9a16-15d98fcdc6aa"
 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"
 Gurobi = "2e9cd046-0924-5485-92f1-d5272153d98b"
+Libdl = "8f399da3-3557-5675-b5ff-fb832c97cbdb"
 NetworkLayout = "46757867-2c16-5918-afeb-47bfcb05e46a"
 OptimalBranchingCore = "c76e7b22-e1d2-40e8-b0f1-f659837787b8"
 ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
@@ -25,13 +27,15 @@ TropicalNumbers = "b3a74e9c-7526-4576-a4eb-79c0d4c32334"
 BitBasis = "0.9.10"
 CairoMakie = "0.15.6"
 Colors = "0.13.1"
+Combinatorics = "1.1.0"
 Compose = "0.9.6"
 DataStructures = "0.18.22"
 GenericTensorNetworks = "4"
 GraphMakie = "0.6.3"
 GraphPlot = "0.6.2"
 Graphs = "1.13.1"
 Gurobi = "1.8.0"
+Libdl = "1.11.0"
 NetworkLayout = "0.4.10"
 OptimalBranchingCore = "0.1"
 ProblemReductions = "0.3.5"

README.md

@@ -12,7 +12,11 @@ A high-performance Julia package for solving Boolean satisfiability problems usi
 - **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
+- **Circuit Simplification**: Automatic circuit simplification using constant propagation and gate optimization
+- **CDCL Integration**: Supports clause learning via CaDiCaL SAT solver integration
+- **2-SAT Solver**: Built-in efficient 2-SAT solver for special cases
 - **High Performance**: Optimized for speed with efficient propagation and contraction algorithms
+- **Visualization**: Problem structure visualization with graph-based representations
 - **Flexible Interface**: Easy-to-use API for various constraint satisfaction problems
 
 ## Installation
@@ -36,7 +40,7 @@ cnf = ∧(∨(a, b, ¬d, ¬e), ∨(¬a, d, e, ¬f), ∨(f, g), ∨(¬b, c), ∨(
 
 # Solve and get assignments
 sat = Satisfiability(cnf; use_constraints=true)
-satisfiable, assignments, depth = solve_sat_with_assignments(sat)
+satisfiable, assignments, stats = solve_sat_with_assignments(sat)
 
 println("Satisfiable: ", satisfiable)
 println("Assignments: ", assignments)
@@ -46,69 +50,144 @@ println("Assignments: ", assignments)
 
 ```julia
 # Factor a semiprime number
-a, b = solve_factoring(5, 5, 31*29)
+a, b, stats = solve_factoring(5, 5, 31*29)
 println("Factors: $a × $b = $(a*b)")
 ```
 
-### Circuit Problems
+### Circuit SAT Problems
 
 ```julia
+using ProblemReductions: Circuit, Assignment, BooleanExpr
+
 # 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())
+satisfiable, stats = solve_circuit_sat(circuit)
 ```
 
 ## Core Components
 
 ### Problem Types
-- `TNProblem`: Main problem representation
-- `BipartiteGraph`: Static problem structure
-- `DomainMask`: Variable domain representation
-
-### Solvers
-- `TNContractionSolver`: Tensor network contraction-based solver
-- `LeastOccurrenceSelector`: Variable selection strategy
-- `NumUnfixedVars`: Measurement strategy
+- `TNProblem`: Main tensor network problem representation
+- `BipartiteGraph`: Static problem structure (variables and tensors)
+- `DomainMask`: Variable domain representation using bitmasks
+- `ClauseTensor`: Clause representation as tensor factors
+
+### Solvers & Strategies
+- `TNContractionSolver`: Tensor network contraction-based branching table solver
+- `MostOccurrenceSelector`: Variable selection based on occurrence frequency
+- `NumUnfixedVars`: Measurement strategy counting unfixed variables
+- `NumUnfixedTensors`: Measurement based on unfixed tensor count
+- `HardSetSize`: Measurement based on hard clause set size
 
 ### 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
+
+| Function | Description |
+|----------|-------------|
+| `solve()` | Main solving function with configurable strategy |
+| `solve_sat_problem()` | Solve SAT and return satisfiability result |
+| `solve_sat_with_assignments()` | Solve SAT and return variable assignments |
+| `solve_circuit_sat()` | Solve circuit satisfiability problems |
+| `solve_factoring()` | Solve integer factoring problems |
+| `setup_from_cnf()` | Setup problem from CNF formulas |
+| `setup_from_circuit()` | Setup problem from circuit descriptions |
+| `setup_from_sat()` | Setup problem from CSP representation |
 
 ## Advanced Usage
 
 ### Custom Branching Strategy
 
 ```julia
-using OptimalBranchingCore: BranchingStrategy
+using OptimalBranchingCore: BranchingStrategy, GreedyMerge
 
 # Configure custom solver
 bsconfig = BranchingStrategy(
     table_solver=TNContractionSolver(),
-    selector=LeastOccurrenceSelector(2, 10),
-    measure=NumUnfixedVars()
+    selector=MostOccurrenceSelector(3, 4),
+    measure=NumUnfixedTensors(),
+    set_cover_solver=GreedyMerge()
 )
 
 # Solve with custom configuration
-result, depth = solve(problem, bsconfig, NoReducer())
+result = solve(problem, bsconfig, NoReducer())
 ```
 
-### Benchmarking
+### Circuit Simplification
+
+```julia
+using ProblemReductions: CircuitSAT
+
+# Simplify a circuit before solving
+simplified_circuit, var_mapping = simplify_circuit(circuit, fixed_vars)
+```
 
-The package includes comprehensive benchmarking tools:
+### 2-SAT Solving
 
 ```julia
-using BooleanInferenceBenchmarks
+# Check if problem is 2-SAT reducible and solve
+if is_2sat_reducible(problem)
+    result = solve_2sat(problem)
+end
+```
 
-# Compare different solvers
-configs = [(10,10), (12,12), (14,14)]
-results = run_solver_comparison(FactoringProblem, configs)
-print_solver_comparison_summary(results)
+### CDCL with Clause Learning
+
+```julia
+# Solve using CaDiCaL and mine learned clauses
+status, model, learned_clauses = solve_and_mine(cnf; conflict_limit=30000, max_len=5)
 ```
 
+### Visualization
+
+```julia
+# Visualize the problem structure
+visualize_problem(problem, "output.png")
+
+# Get and visualize highest degree variables
+high_degree_vars = get_highest_degree_variables(problem, k=10)
+visualize_highest_degree_vars(problem, k=10, "high_degree.png")
+```
+
+## Project Structure
+
+```
+src/
+├── BooleanInference.jl    # Main module
+├── interface.jl           # High-level API functions
+├── core/                  # Core data structures
+│   ├── static.jl          # BipartiteGraph structure
+│   ├── domain.jl          # DomainMask operations
+│   ├── problem.jl         # TNProblem definition
+│   └── stats.jl           # BranchingStats tracking
+├── branching/             # Branching algorithms
+│   ├── branch.jl          # Main branching logic (bbsat!)
+│   ├── propagate.jl       # Constraint propagation
+│   └── measure.jl         # Measure strategies
+├── branch_table/          # Branching table generation
+│   ├── contraction.jl     # Tensor contraction
+│   ├── selector.jl        # Variable selection
+│   └── branchtable.jl     # Table generation
+├── utils/                 # Utility functions
+│   ├── simplify_circuit.jl # Circuit simplification
+│   ├── circuit2cnf.jl     # Circuit to CNF conversion
+│   ├── twosat.jl          # 2-SAT solver
+│   └── visualization.jl   # Problem visualization
+└── cdcl/                  # CDCL integration
+    └── CaDiCaLMiner.jl    # CaDiCaL wrapper for clause learning
+```
+
+## Dependencies
+
+Key dependencies include:
+- [GenericTensorNetworks.jl](https://github.com/QuEraComputing/GenericTensorNetworks.jl) - Tensor network operations
+- [OptimalBranchingCore.jl](https://github.com/OptimalBranching/OptimalBranchingCore.jl) - Branching framework
+- [ProblemReductions.jl](https://github.com/GiggleLiu/ProblemReductions.jl) - Problem reduction utilities
+- [Graphs.jl](https://github.com/JuliaGraphs/Graphs.jl) - Graph data structures
+- [CairoMakie.jl](https://github.com/MakieOrg/Makie.jl) - Visualization
+
+## License
+
+This project is licensed under the MIT License - see the [LICENSE](LICENSE) file for details.