diff --git a/.gitignore b/.gitignore index 3dad150..becbd4f 100644 --- a/.gitignore +++ b/.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 \ No newline at end of file +*.out +*.history +/discs/ \ No newline at end of file diff --git a/.gitmodules b/.gitmodules index e61a015..7c0cbc2 100644 --- a/.gitmodules +++ b/.gitmodules @@ -13,4 +13,8 @@ [submodule "benchmarks/third-party/CnC"] path = benchmarks/third-party/CnC url = https://github.com/marijnheule/CnC.git - ignore = all \ No newline at end of file + ignore = all +[submodule "benchmarks/third-party/cir_bench"] + path = benchmarks/third-party/cir_bench + url = https://github.com/santoshsmalagi/Benchmarks.git + ignore = all diff --git a/Project.toml b/Project.toml index a1ef5bb..3fc0932 100644 --- a/Project.toml +++ b/Project.toml @@ -4,8 +4,16 @@ 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" @@ -13,8 +21,16 @@ 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" diff --git a/README.md b/README.md index a0498a5..314c4f7 100644 --- a/README.md +++ b/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 diff --git a/benchmarks/Project.toml b/benchmarks/Project.toml index 15665c7..f7287c5 100644 --- a/benchmarks/Project.toml +++ b/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" diff --git a/benchmarks/examples/circuitsat_example.jl b/benchmarks/examples/circuitsat_example.jl new file mode 100644 index 0000000..b12d11e --- /dev/null +++ b/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) + diff --git a/benchmarks/examples/cnfsat_example.jl b/benchmarks/examples/cnfsat_example.jl new file mode 100644 index 0000000..53474ab --- /dev/null +++ b/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 \ No newline at end of file diff --git a/benchmarks/examples/factoring_example.jl b/benchmarks/examples/factoring_example.jl index 400ecfa..0a3597e 100644 --- a/benchmarks/examples/factoring_example.jl +++ b/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) diff --git a/benchmarks/src/BooleanInferenceBenchmarks.jl b/benchmarks/src/BooleanInferenceBenchmarks.jl index 18ce260..a90c2ad 100644 --- a/benchmarks/src/BooleanInferenceBenchmarks.jl +++ b/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 \ No newline at end of file diff --git a/benchmarks/src/CNFSAT/dataset.jl b/benchmarks/src/CNFSAT/dataset.jl new file mode 100644 index 0000000..80a3b59 --- /dev/null +++ b/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 diff --git a/benchmarks/src/CNFSAT/interface.jl b/benchmarks/src/CNFSAT/interface.jl new file mode 100644 index 0000000..24c1440 --- /dev/null +++ b/benchmarks/src/CNFSAT/interface.jl @@ -0,0 +1,88 @@ +# Interface functions for CNF SAT benchmarking + +# Solvers available for CNF SAT +function available_solvers(::Type{CNFSATProblem}) + return [BooleanInferenceSolver(), KissatSolver(), MinisatSolver()] +end + +function default_solver(::Type{CNFSATProblem}) + return BooleanInferenceSolver() +end + +# Problem identification +function problem_id(config::CNFSATConfig) + return basename(config.path) +end + +function problem_id(instance::CNFSATInstance) + return instance.name +end + +# Load a single CNF instance from file +function load_cnf_instance(config::CNFSATConfig) + return parse_cnf_file(config.path) +end + +# Read instances from a config (for compatibility with benchmark API) +function read_instances(::Type{CNFSATProblem}, config::CNFSATConfig) + return [load_cnf_instance(config)] +end + +# Read instances from a directory path (for benchmark_dataset) +function read_instances(::Type{CNFSATProblem}, path::AbstractString) + if isfile(path) + # Single file + if !endswith(path, ".cnf") + error("Expected .cnf file, got: $path") + end + config = CNFSATConfig(path) + return [load_cnf_instance(config)] + elseif isdir(path) + # Directory: load all .cnf files + cnf_files = discover_cnf_files(path) + + instances = CNFSATInstance[] + + for cnf_file in cnf_files + try + config = CNFSATConfig(cnf_file) + push!(instances, load_cnf_instance(config)) + catch e + @warn "Failed to load $cnf_file" exception=e + end + end + + return instances + else + error("Path not found: $path") + end +end + +# Generate a single instance (for compatibility, just loads the file) +function generate_instance(::Type{CNFSATProblem}, config::CNFSATConfig; kwargs...) + return load_cnf_instance(config) +end + +# Verify solution +function verify_solution(::Type{CNFSATProblem}, instance::CNFSATInstance, result) + # Check if we got a valid result + if result === nothing + return false + end + + # The result should be a tuple (is_sat, stats) or similar + # We consider it successful if the solver ran without errors + return true +end + +# Helper function to check if the CNF is satisfiable +function is_cnf_satisfiable(result) + if result === nothing + return nothing # Solver failed + end + # Assuming result is (satisfiable::Bool, stats) + if result isa Tuple && length(result) >= 1 + return result[1] + end + return nothing +end diff --git a/benchmarks/src/CNFSAT/parser.jl b/benchmarks/src/CNFSAT/parser.jl new file mode 100644 index 0000000..f3cf859 --- /dev/null +++ b/benchmarks/src/CNFSAT/parser.jl @@ -0,0 +1,109 @@ +# DIMACS CNF file parser + +""" + parse_cnf_file(filepath::String) -> CNFSATInstance + +Parse a CNF file in DIMACS format and return a CNFSATInstance. + +DIMACS CNF format: +- Comment lines start with 'c' +- Problem line: "p cnf " +- Clause lines: space-separated integers, terminated by 0 + - Positive integers represent positive literals + - Negative integers represent negative literals + - Example: "1 -2 3 0" means (x1 ∨ ¬x2 ∨ x3) +""" +function parse_cnf_file(filepath::String) + isfile(filepath) || error("File not found: $filepath") + + name = basename(filepath) + # Remove extension if present + if endswith(name, ".cnf") + name = name[1:end-4] + end + + num_vars = 0 + num_clauses = 0 + clauses = Vector{Vector{Int}}() + header_found = false + + open(filepath, "r") do io + for line in eachline(io) + line = strip(line) + + # Skip empty lines + isempty(line) && continue + + # Skip comment lines + startswith(line, 'c') && continue + + # Parse problem line + if startswith(line, 'p') + header_found = true + parts = split(line) + length(parts) >= 4 || error("Invalid problem line: $line") + parts[2] == "cnf" || error("Expected 'cnf' format, got: $(parts[2])") + + num_vars = parse(Int, parts[3]) + num_clauses = parse(Int, parts[4]) + continue + end + + # Parse clause line + if header_found + literals = Int[] + for token in split(line) + token = strip(token) + isempty(token) && continue + + lit = parse(Int, token) + if lit == 0 + # End of clause + if !isempty(literals) + push!(clauses, literals) + literals = Int[] + end + else + push!(literals, lit) + end + end + + # Handle clause that doesn't end with explicit 0 on same line + if !isempty(literals) + push!(clauses, literals) + end + end + end + end + + header_found || error("No problem header found in file: $filepath") + + # Verify that the number of clauses matches the header + if length(clauses) != num_clauses + @warn "Number of clauses ($(length(clauses))) doesn't match header ($num_clauses) in $filepath" + end + + return CNFSATInstance(name, num_vars, num_clauses, clauses, filepath) +end + +""" + cnf_instantiation(instance::CNFSATInstance) + +Convert a CNFSATInstance to a ProblemReductions.CNF problem. +""" +function cnf_instantiation(instance::CNFSATInstance) + # Create boolean variables for each variable in the CNF + # Variables are numbered 1 to num_vars + var_symbols = [Symbol("x$i") for i in 1:instance.num_vars] + + # Convert clauses to CNFClause objects + cnf_clauses = map(instance.clauses) do clause_literals + bool_vars = map(clause_literals) do lit + var_idx = abs(lit) + is_negated = lit < 0 + BoolVar(var_symbols[var_idx], is_negated) + end + CNFClause(bool_vars) + end + return CNF(cnf_clauses) +end diff --git a/benchmarks/src/CNFSAT/solvers.jl b/benchmarks/src/CNFSAT/solvers.jl new file mode 100644 index 0000000..432f2d8 --- /dev/null +++ b/benchmarks/src/CNFSAT/solvers.jl @@ -0,0 +1,22 @@ +# Solver implementations for CNF SAT + +# BooleanInference solver +function solve_instance(::Type{CNFSATProblem}, instance::CNFSATInstance, solver::BooleanInferenceSolver) + cnf = cnf_instantiation(instance) + tn_problem = BooleanInference.setup_from_cnf(cnf) + result = BooleanInference.solve(tn_problem, solver.bsconfig, solver.reducer; show_stats=solver.show_stats) + return result +end + +# Kissat solver - works directly with CNF files +function solve_instance(::Type{CNFSATProblem}, instance::CNFSATInstance, solver::KissatSolver) + # Kissat can work directly with the CNF file + result = run_cnf_solver(solver, instance.source_path) + return result +end + +# MiniSat solver - works directly with CNF files +function solve_instance(::Type{CNFSATProblem}, instance::CNFSATInstance, solver::MinisatSolver) + result = run_cnf_solver(solver, instance.source_path) + return result +end diff --git a/benchmarks/src/CNFSAT/types.jl b/benchmarks/src/CNFSAT/types.jl new file mode 100644 index 0000000..ee3524c --- /dev/null +++ b/benchmarks/src/CNFSAT/types.jl @@ -0,0 +1,33 @@ +# Types for CNF SAT problem instances + +struct CNFSATProblem <: AbstractBenchmarkProblem end + +""" +Configuration for CNF SAT problems. +- path: path to the CNF file in DIMACS format +""" +struct CNFSATConfig <: AbstractProblemConfig + path::String + + function CNFSATConfig(path::String) + isfile(path) || error("CNF file not found: $path") + new(path) + end +end + +""" +Represents a CNF SAT instance loaded from a DIMACS file. +Fields: +- name: instance name (typically filename without extension) +- num_vars: number of variables +- num_clauses: number of clauses +- clauses: vector of clauses, where each clause is a vector of literals (integers) +- source_path: path to the original CNF file +""" +struct CNFSATInstance <: AbstractInstance + name::String + num_vars::Int + num_clauses::Int + clauses::Vector{Vector{Int}} + source_path::String +end diff --git a/benchmarks/src/abstract_types.jl b/benchmarks/src/abstract_types.jl index 31b90d7..6bbe458 100644 --- a/benchmarks/src/abstract_types.jl +++ b/benchmarks/src/abstract_types.jl @@ -3,16 +3,30 @@ abstract type AbstractProblemConfig end abstract type AbstractInstance end abstract type AbstractSolver end -@kwdef struct BooleanInferenceSolver <: AbstractSolver - warmup::Bool = true +# CNF-based SAT solvers share common characteristics +abstract type CNFSolver <: AbstractSolver end + +struct BooleanInferenceSolver <: AbstractSolver + warmup::Bool + bsconfig::BranchingStrategy + reducer::AbstractReducer + show_stats::Bool + function BooleanInferenceSolver(;warmup=true, bsconfig=BranchingStrategy( + table_solver=TNContractionSolver(), + selector=MinGammaSelector(1,2, TNContractionSolver(), OptimalBranchingCore.GreedyMerge()), + measure=NumUnfixedVars() + ), reducer=NoReducer(), show_stats=false) + new(warmup, bsconfig, reducer, show_stats) + end end struct IPSolver <: AbstractSolver warmup::Bool optimizer::Any env::Any + verify::Bool function IPSolver(optimizer=Gurobi.Optimizer, env=nothing) - new(true, optimizer, env) + new(true, optimizer, env, true) end end @@ -20,8 +34,9 @@ struct XSATSolver <: AbstractSolver warmup::Bool csat_path::String yosys_path::String - satisfiable_when_high::Bool - function XSATSolver(;csat_path=joinpath(dirname(@__DIR__), "artifacts", "bin", "csat"), yosys_path=nothing) + verify::Bool + timeout::Real + function XSATSolver(;csat_path=joinpath(dirname(@__DIR__), "artifacts", "bin", "csat"), yosys_path=nothing, timeout=600.0) !isfile(csat_path) && error("File $csat_path for X-SAT solver does not exist") # check if yosys is installed by homebrew or apt @@ -34,30 +49,43 @@ struct XSATSolver <: AbstractSolver else !isfile(yosys_path) && error("File $yosys_path for Yosys does not exist") end - new(false, csat_path, yosys_path, true) + new(false, csat_path, yosys_path, true, timeout) end end -struct KissatSolver <: AbstractSolver + +struct KissatSolver <: CNFSolver warmup::Bool kissat_path::String - yosys_path::String - abc_path::String - satisfiable_when_high::Bool - function KissatSolver(;kissat_path=nothing, yosys_path=nothing, abc_path=nothing) - if isnothing(kissat_path) - kissat_path = try - kissat_path = strip(read(`which kissat`, String)) - catch - error("Kissat not found in PATH, and kissat_path is not provided") - end - else - !isfile(kissat_path) && error("File $kissat_path for Kissat does not exist") - end - new(true, kissat_path, yosys_path, abc_path, false) + abc_path::Union{String, Nothing} + verify::Bool + timeout::Real + function KissatSolver(;kissat_path=nothing, abc_path=joinpath(dirname(@__DIR__), "artifacts", "bin", "abc"), timeout=600.0) + kissat_path = isnothing(kissat_path) ? + find_executable_in_path("kissat", "Kissat") : + validate_executable_path(kissat_path, "Kissat") + abc_path = validate_executable_path(abc_path, "ABC") + new(false, kissat_path, abc_path, false, timeout) # CNF solvers typically don't need warmup end end +struct MinisatSolver <: CNFSolver + warmup::Bool + minisat_path::String + abc_path::Union{String, Nothing} + verify::Bool + timeout::Real + function MinisatSolver(;minisat_path=nothing, abc_path=joinpath(dirname(@__DIR__), "artifacts", "bin", "abc"), timeout=600.0) + minisat_path = isnothing(minisat_path) ? + find_executable_in_path("minisat", "MiniSAT") : + validate_executable_path(minisat_path, "MiniSAT") + abc_path = validate_executable_path(abc_path, "ABC") + new(false, minisat_path, abc_path, false, timeout) + end +end + + + # ---------------------------------------- # Core Interface (must be implemented) # ---------------------------------------- @@ -82,4 +110,12 @@ end function solver_name(::XSATSolver) return "X-SAT" +end + +function solver_name(::KissatSolver) + return "Kissat" +end + +function solver_name(::MinisatSolver) + return "MiniSAT" end \ No newline at end of file diff --git a/benchmarks/src/benchmark.jl b/benchmarks/src/benchmark.jl index 995dfec..e378d29 100644 --- a/benchmarks/src/benchmark.jl +++ b/benchmarks/src/benchmark.jl @@ -1,16 +1,19 @@ """ - benchmark_dataset(problem_type, dataset_path; solver=nothing, warmup=true) + benchmark_dataset(problem_type, dataset_path; solver=nothing, verify=true) Run benchmark on a single dataset file/directory. # Arguments - `problem_type::Type{<:AbstractBenchmarkProblem}`: The type of problem to benchmark -- `dataset_path::String`: Path to the dataset file or directory +- `dataset_path::AbstractString`: Path to the dataset file or directory - `solver`: The solver to use (defaults to the problem type's default solver) -- `warmup::Bool`: Whether to perform warmup/tuning (default: true). Set to false for solvers - implemented in non-Julia languages (e.g., C++), which don't benefit from Julia's JIT compilation. +- `verify::Bool`: Whether to verify solution correctness (default: true). Set to false to skip + verification and only measure performance. When false, all runs are considered successful. """ -function benchmark_dataset(problem_type::Type{<:AbstractBenchmarkProblem}, dataset_path::String; solver=nothing) +function benchmark_dataset(problem_type::Type{<:AbstractBenchmarkProblem}, + dataset_path::AbstractString; + solver::Union{AbstractSolver, Nothing}=nothing, + verify::Bool=true) actual_solver = isnothing(solver) ? default_solver(problem_type) : solver warmup = actual_solver.warmup solver_info = solver_name(actual_solver) @@ -39,14 +42,11 @@ function benchmark_dataset(problem_type::Type{<:AbstractBenchmarkProblem}, datas successful_runs = 0 failed_runs = 0 - # Warmup and tune benchmark parameters if requested - b = nothing + # Warmup if requested if warmup - @info " Performing warmup and tuning..." - sample_trial_fn = () -> solve_instance(problem_type, instances[1], solver) - b = @benchmarkable $sample_trial_fn() - tune!(b) - @info " Benchmark tuned, starting verification and timing..." + @info " Performing warmup..." + solve_instance(problem_type, instances[1], actual_solver) + @info " Warmup completed, starting verification and timing..." else @info " Skipping warmup (non-Julia solver), starting verification and timing..." end @@ -56,27 +56,34 @@ function benchmark_dataset(problem_type::Type{<:AbstractBenchmarkProblem}, datas for (i, instance) in enumerate(instances) try - result = solve_instance(problem_type, instance, solver) - is_correct = verify_solution(problem_type, instance, result) + # Measure time directly while solving + result = nothing + elapsed_time = @elapsed begin + result = solve_instance(problem_type, instance, actual_solver) + end - if !is_correct - @warn " Instance $i: Incorrect solution" - incorrect_runs += 1 - continue + # For CircuitSAT, print SAT/UNSAT result + if problem_type == CircuitSATProblem && result !== nothing + satisfiable, _ = result + instance_name = hasfield(typeof(instance), :name) ? instance.name : "Instance $i" + println(" $instance_name: ", satisfiable ? "SAT" : "UNSAT", " ($(round(elapsed_time, digits=4))s)") end + # Verify solution if requested + if verify + is_correct = verify_solution(problem_type, instance, result) + if !is_correct + @warn " Instance $i: Incorrect solution" + incorrect_runs += 1 + continue + end + end correct_runs += 1 - trial_fn = () -> solve_instance(problem_type, instance, solver) - b_instance = @benchmarkable $trial_fn() - if warmup && !isnothing(b) - b_instance.params = b.params - end - timing_result = run(b_instance, samples=1) - - push!(all_times, median(timing_result).time / 1e9) - push!(all_memory, median(timing_result).memory) - push!(all_gc_times, median(timing_result).gctime / 1e9) + push!(all_times, elapsed_time) + # Memory and GC time not available without BenchmarkTools, set to 0 + push!(all_memory, 0) + push!(all_gc_times, 0.0) successful_runs += 1 if i % 10 == 0 || i == length(instances) @@ -110,4 +117,3 @@ function benchmark_dataset(problem_type::Type{<:AbstractBenchmarkProblem}, datas return nothing end end - diff --git a/benchmarks/src/circuitIO/aig.jl b/benchmarks/src/circuitIO/aig.jl index 39f5677..2da97c3 100644 --- a/benchmarks/src/circuitIO/aig.jl +++ b/benchmarks/src/circuitIO/aig.jl @@ -96,6 +96,7 @@ Build a ProblemReductions.Circuit from an AIG (no latches allowed). - Each AND gate (lhs, r0, r1) becomes: n_ = ∧(expr(r0), expr(r1)) - Each primary output becomes: out = expr(lit) Inputs do not need explicit assignments; they are just symbols used by gates. +Note: CircuitSAT(...; use_constraints=true) will automatically constrain outputs. """ function aig_to_circuit(aig::AIG; output_prefix::AbstractString="out") if !isempty(aig.latches) @@ -112,9 +113,11 @@ function aig_to_circuit(aig::AIG; output_prefix::AbstractString="out") push!(assigns, "$lhs_nm = ∧($(lit_str(r0)), $(lit_str(r1)))") end - # Outputs: give them stable names + # Outputs: give them stable names and collect them + output_syms = Symbol[] for (i, l) in enumerate(aig.outputs) outnm = Symbol(output_prefix, "_", i) + push!(output_syms, outnm) push!(assigns, string(outnm, " = ", lit_str(l))) end @@ -127,7 +130,14 @@ function aig_to_circuit(aig::AIG; output_prefix::AbstractString="out") code_str = String(take!(src)) # Evaluate macro call to get a `Circuit` - # This is the public, documented entry: @circuit returns a Circuit. [oai_citation:1‡giggleliu.github.io](https://giggleliu.github.io/ProblemReductions.jl/dev/rules/spinglass_sat/) - return Base.invokelatest(eval, Meta.parse(code_str)) + circuit = Base.invokelatest(eval, Meta.parse(code_str)) + + # Add constraint: each output must be true + # This follows the pattern in test/interface.jl + for out_sym in output_syms + push!(circuit.exprs, Assignment([out_sym], BooleanExpr(true))) + end + + return circuit end diff --git a/benchmarks/src/circuitIO/circuitIO.jl b/benchmarks/src/circuitIO/circuitIO.jl index 56d335e..9f5c392 100644 --- a/benchmarks/src/circuitIO/circuitIO.jl +++ b/benchmarks/src/circuitIO/circuitIO.jl @@ -1,12 +1,13 @@ module CircuitIO using ProblemReductions - using ProblemReductions: Circuit, BooleanExpr, extract_symbols!, simple_form - + using ProblemReductions: Circuit, BooleanExpr, Assignment, extract_symbols!, simple_form, @circuit + using ProblemReductions: ∧, ∨, ¬, ⊻ + include("aig.jl") include("verilog.jl") - export aig_to_circuit + export read_aag, aig_to_circuit + export verilog_to_circuit export write_verilog, circuit_to_verilog - end \ No newline at end of file diff --git a/benchmarks/src/circuitIO/verilog.jl b/benchmarks/src/circuitIO/verilog.jl index 36e387f..8d0a3b3 100644 --- a/benchmarks/src/circuitIO/verilog.jl +++ b/benchmarks/src/circuitIO/verilog.jl @@ -1,4 +1,307 @@ -# ---------- Verilog codegen for Circuit ---------- +# ---------- Verilog I/O for Circuit ---------- + +# ========== Verilog → Circuit Parser ========== + +struct VerilogModule + name::String + inputs::Vector{Symbol} + outputs::Vector{Symbol} + wires::Vector{Symbol} + assignments::Vector{Tuple{Symbol, String}} # (output, expression_string) +end + +""" +Parse a Verilog module from a string or file and convert to Circuit. + +Example: +```julia +circuit = verilog_to_circuit("data/iscas85/c17.v") +``` +""" +function verilog_to_circuit(path::String) + content = read(path, String) + mod = parse_verilog_module(content) + return verilog_module_to_circuit(mod) +end + +function parse_verilog_module(content::String) + # Remove comments + content = replace(content, r"//[^\n]*" => "") + content = replace(content, r"/\*.*?\*/"s => "") + + # Extract module name (support multiline declarations) + # Try to match: module name (...); with flexible whitespace/newlines + mod_match = match(r"module\s+(\w+)\s*\([^)]*\)\s*;"s, content) + if mod_match === nothing + # Try alternative format: module name; (without port list in header) + mod_match = match(r"module\s+(\w+)\s*;", content) + end + mod_match === nothing && error("Cannot find module declaration") + mod_name = mod_match.captures[1] + + # Extract inputs + inputs = Symbol[] + for m in eachmatch(r"input\s+((?:\w+\s*,?\s*)+);", content) + for name in split(replace(m.captures[1], r"\s+" => " "), r"[,\s]+") + name = strip(name) + !isempty(name) && push!(inputs, Symbol(name)) + end + end + + # Extract outputs + outputs = Symbol[] + for m in eachmatch(r"output\s+((?:\w+\s*,?\s*)+);", content) + for name in split(replace(m.captures[1], r"\s+" => " "), r"[,\s]+") + name = strip(name) + !isempty(name) && push!(outputs, Symbol(name)) + end + end + + # Extract wires + wires = Symbol[] + for m in eachmatch(r"wire\s+((?:\w+\s*,?\s*)+);", content) + for name in split(replace(m.captures[1], r"\s+" => " "), r"[,\s]+") + name = strip(name) + !isempty(name) && push!(wires, Symbol(name)) + end + end + + # Extract gate instantiations and assign statements + assignments = Tuple{Symbol, String}[] + + # Parse assign statements: assign output = expression; + for m in eachmatch(r"assign\s+(\w+)\s*=\s*([^;]+);", content) + output = Symbol(m.captures[1]) + expr_str = strip(m.captures[2]) + push!(assignments, (output, expr_str)) + end + + # Parse gate instantiations: gate_type instance_name (output, input1, input2, ...); + # Common gates: and, or, not, nand, nor, xor, xnor, buf + gate_pattern = r"(and|or|not|nand|nor|xor|xnor|buf)\s+\w+\s*\(([^)]+)\)\s*;" + for m in eachmatch(gate_pattern, content) + gate_type = m.captures[1] + ports_str = m.captures[2] + ports = [Symbol(strip(p)) for p in split(ports_str, ',')] + + if length(ports) < 2 + error("Invalid gate instantiation: $(m.match)") + end + + output = ports[1] + inputs_syms = ports[2:end] + + # Convert gate type to expression + expr_str = gate_to_expression(gate_type, inputs_syms) + push!(assignments, (output, expr_str)) + end + + return VerilogModule(mod_name, inputs, outputs, wires, assignments) +end + +function gate_to_expression(gate_type::AbstractString, inputs::Vector{Symbol}) + if gate_type == "not" || gate_type == "buf" + length(inputs) == 1 || error("$gate_type gate expects 1 input") + return gate_type == "not" ? "¬$(inputs[1])" : "$(inputs[1])" + elseif gate_type == "and" + return join(["$(inp)" for inp in inputs], " ∧ ") + elseif gate_type == "or" + return join(["$(inp)" for inp in inputs], " ∨ ") + elseif gate_type == "nand" + return "¬(" * join(["$(inp)" for inp in inputs], " ∧ ") * ")" + elseif gate_type == "nor" + return "¬(" * join(["$(inp)" for inp in inputs], " ∨ ") * ")" + elseif gate_type == "xor" + return join(["$(inp)" for inp in inputs], " ⊻ ") + elseif gate_type == "xnor" + return "¬(" * join(["$(inp)" for inp in inputs], " ⊻ ") * ")" + else + error("Unsupported gate type: $gate_type") + end +end + +function verilog_module_to_circuit(mod::VerilogModule) + # Create a mapping of all symbols that need to be variables + all_symbols = Set{Symbol}() + union!(all_symbols, mod.inputs) + union!(all_symbols, mod.outputs) + union!(all_symbols, mod.wires) + + # Parse expressions and create assignments + exprs = Assignment[] + + for (output, expr_str) in mod.assignments + # Parse the expression string into a BooleanExpr + bool_expr = parse_boolean_expression(expr_str, all_symbols) + push!(exprs, Assignment([output], bool_expr)) + end + + return Circuit(exprs) +end + +# Parse a boolean expression string into a BooleanExpr +function parse_boolean_expression(expr_str::AbstractString, known_vars::Set{Symbol}) + expr_str = String(strip(expr_str)) + + # Handle constants + # Support various Verilog constant formats: + # - Binary: 1'b0, 1'b1 + # - Hex: 1'h0, 1'h1 (and extract LSB for multi-bit hex) + # - Decimal: 1'd0, 1'd1 + # - Simple: 0, 1, true, false + if expr_str in ["1'b1", "1", "true"] + return BooleanExpr(true) + elseif expr_str in ["1'b0", "0", "false"] + return BooleanExpr(false) + elseif match(r"^1'[hH][0-9a-fA-F]+$", expr_str) !== nothing + # Hex format: extract the hex value and check if LSB is 1 + hex_match = match(r"^1'[hH]([0-9a-fA-F]+)$", expr_str) + hex_str = hex_match.captures[1] + # Parse hex and check LSB + hex_val = parse(Int, hex_str, base=16) + return BooleanExpr((hex_val & 1) == 1) + elseif match(r"^1'[dD]\d+$", expr_str) !== nothing + # Decimal format: extract the decimal value and check if LSB is 1 + dec_match = match(r"^1'[dD](\d+)$", expr_str) + dec_val = parse(Int, dec_match.captures[1]) + return BooleanExpr((dec_val & 1) == 1) + end + + # Try to match parentheses and parse recursively + if startswith(expr_str, "(") && endswith(expr_str, ")") + # Check if parentheses are balanced (top-level only) + depth = 0 + all_enclosed = true + for (i, c) in enumerate(expr_str) + if c == '(' + depth += 1 + elseif c == ')' + depth -= 1 + if depth == 0 && i < length(expr_str) + all_enclosed = false + break + end + end + end + + if all_enclosed + inner = expr_str[2:end-1] + return parse_boolean_expression(inner, known_vars) + end + end + + # Check for NOT operation + if startswith(expr_str, "~") + inner = strip(expr_str[nextind(expr_str, 1):end]) + sub_expr = parse_boolean_expression(inner, known_vars) + return ¬sub_expr + elseif startswith(expr_str, "¬") + # Unicode character, need to handle multi-byte indexing + idx = nextind(expr_str, 1) + inner = strip(expr_str[idx:end]) + sub_expr = parse_boolean_expression(inner, known_vars) + return ¬sub_expr + end + + # Try to find binary operators (with precedence handling) + # Priority: OR > XOR > AND + for (op_str, op_func) in [(" | ", ∨), (" ∨ ", ∨)] + if contains(expr_str, op_str) + parts = split_on_operator(expr_str, op_str) + if length(parts) > 1 + sub_exprs = [parse_boolean_expression(strip(p), known_vars) for p in parts] + return reduce(op_func, sub_exprs) + end + end + end + + for (op_str, op_func) in [(" ^ ", ⊻), (" ⊻ ", ⊻)] + if contains(expr_str, op_str) + parts = split_on_operator(expr_str, op_str) + if length(parts) > 1 + sub_exprs = [parse_boolean_expression(strip(p), known_vars) for p in parts] + return reduce(op_func, sub_exprs) + end + end + end + + for (op_str, op_func) in [(" & ", ∧), (" ∧ ", ∧)] + if contains(expr_str, op_str) + parts = split_on_operator(expr_str, op_str) + if length(parts) > 1 + sub_exprs = [parse_boolean_expression(strip(p), known_vars) for p in parts] + return reduce(op_func, sub_exprs) + end + end + end + + # If no operators found, it must be a variable + var_sym = Symbol(expr_str) + if var_sym in known_vars + return BooleanExpr(var_sym) + else + error("Unknown variable: $var_sym") + end +end + +# Split expression on operator while respecting parentheses +function split_on_operator(expr::AbstractString, op::AbstractString) + expr = String(expr) + op = String(op) + + # If operator not in string, return as single part + if !occursin(op, expr) + return [expr] + end + + parts = String[] + current = "" + depth = 0 + + # Use a character-by-character approach with proper Unicode handling + chars = collect(expr) + i = 1 + + while i <= length(chars) + if chars[i] == '(' + depth += 1 + current *= chars[i] + i += 1 + elseif chars[i] == ')' + depth -= 1 + current *= chars[i] + i += 1 + elseif depth == 0 + # Check if we're at the operator + # Build potential operator from current position + potential_op = "" + j = i + while j <= length(chars) && length(potential_op) < length(op) + potential_op *= chars[j] + j += 1 + end + + if potential_op == op + # Found the operator at top level + push!(parts, current) + current = "" + i = j # Skip past the operator + else + current *= chars[i] + i += 1 + end + else + current *= chars[i] + i += 1 + end + end + + push!(parts, current) + return parts +end + + +# ========== Circuit → Verilog Codegen ========== # Make a Verilog-safe identifier from a Symbol (e.g., Symbol("##var#236") -> "__var_236") diff --git a/benchmarks/src/circuitSAT/dataset.jl b/benchmarks/src/circuitSAT/dataset.jl new file mode 100644 index 0000000..e46d427 --- /dev/null +++ b/benchmarks/src/circuitSAT/dataset.jl @@ -0,0 +1,87 @@ +# Dataset management for CircuitSAT benchmarks + +""" + discover_circuit_files(dir::String; format::Symbol) + +Recursively discover circuit files in a directory. +- format: :verilog (*.v files) or :aag (*.aag files) +""" +function discover_circuit_files(dir::String; format::Symbol) + format in (:verilog, :aag) || error("Format must be :verilog or :aag") + + extension = format == :verilog ? ".v" : ".aag" + files = String[] + + for (root, dirs, filenames) in walkdir(dir) + for filename in filenames + if endswith(filename, extension) + push!(files, joinpath(root, filename)) + end + end + end + + sort!(files) + return files +end + +""" + create_circuitsat_configs(files::Vector{String}; format::Symbol) + +Create CircuitSATConfig objects from a list of files. +""" +function create_circuitsat_configs(files::Vector{String}; format::Symbol) + return [CircuitSATConfig(format, path) for path in files] +end + +""" + load_verilog_dataset(dir::String) + +Load all Verilog files from a directory and create configs. +""" +function load_verilog_dataset(dir::String) + files = discover_circuit_files(dir; format=:verilog) + @info "Found $(length(files)) Verilog files in $dir" + return create_circuitsat_configs(files; format=:verilog) +end + +""" + load_aag_dataset(dir::String) + +Load all AAG files from a directory and create configs. +""" +function load_aag_dataset(dir::String) + files = discover_circuit_files(dir; format=:aag) + @info "Found $(length(files)) AAG files in $dir" + return create_circuitsat_configs(files; format=:aag) +end + +""" + load_circuit_datasets(; verilog_dirs=String[], aag_dirs=String[]) + +Load circuit datasets from multiple directories. + +# Example +```julia +configs = load_circuit_datasets( + verilog_dirs=["data/iscas85"], + aag_dirs=["data/aig/arithmetic"] +) +``` +""" +function load_circuit_datasets(; verilog_dirs=String[], aag_dirs=String[]) + configs = CircuitSATConfig[] + + for dir in verilog_dirs + append!(configs, load_verilog_dataset(dir)) + end + + for dir in aag_dirs + append!(configs, load_aag_dataset(dir)) + end + + @info "Total $(length(configs)) circuit configs loaded" + return configs +end + + + diff --git a/benchmarks/src/circuitSAT/interface.jl b/benchmarks/src/circuitSAT/interface.jl new file mode 100644 index 0000000..8c8614c --- /dev/null +++ b/benchmarks/src/circuitSAT/interface.jl @@ -0,0 +1,161 @@ +# Interface functions for CircuitSAT benchmarking + +# Solvers available for CircuitSAT +function available_solvers(::Type{CircuitSATProblem}) + return [BooleanInferenceSolver()] +end + +function default_solver(::Type{CircuitSATProblem}) + return BooleanInferenceSolver() +end + +# Problem identification +function problem_id(config::CircuitSATConfig) + return basename(config.path) +end + +# Load a single circuit instance from file +function load_circuit_instance(config::CircuitSATConfig) + name = problem_id(config) + + circuit = if config.format == :verilog + CircuitIO.verilog_to_circuit(config.path) + elseif config.format == :aag + # Convert AAG to Verilog using Yosys for better performance + circuit = aag_to_circuit_via_yosys(config.path) + else + error("Unsupported format: $(config.format)") + end + + return CircuitSATInstance(name, circuit, config.format, config.path) +end + +# Convert AAG to Circuit via Yosys (AAG -> Verilog -> Circuit) +function aag_to_circuit_via_yosys(aag_path::String) + # Create temporary Verilog file + mktempdir() do tmpdir + verilog_tmp = joinpath(tmpdir, "circuit_tmp.v") + + # Use Yosys to convert AAG to Verilog with clean module name + # The 'rename' command ensures we get a simple module name + yosys_script = "read_aiger $aag_path; rename -top circuit_top; write_verilog $verilog_tmp" + yosys_cmd = `yosys -p $yosys_script` + + try + # Run Yosys conversion + run(pipeline(yosys_cmd, stdout=devnull, stderr=devnull)) + + # Parse the generated Verilog + circuit = CircuitIO.verilog_to_circuit(verilog_tmp) + + # Add constraints for outputs (po* variables must be true) + # This is the standard CircuitSAT problem formulation + circuit = add_output_constraints(circuit) + + return circuit + catch e + @error "Failed to convert AAG via Yosys" exception=e + # Fallback to direct AAG parsing + @warn "Falling back to direct AAG parsing (may be slower)" + aig = CircuitIO.read_aag(aag_path) + return CircuitIO.aig_to_circuit(aig) + end + end +end + +# Add constraints that all outputs (po* variables) must be true +function add_output_constraints(circuit::Circuit) + # Find all output variables (po* symbols) + output_syms = Symbol[] + for expr in circuit.exprs + for out in expr.outputs + out_str = String(out) + if startswith(out_str, "po") && !(out in output_syms) + push!(output_syms, out) + end + end + end + + # Add constraint for each output + for out_sym in output_syms + push!(circuit.exprs, Assignment([out_sym], BooleanExpr(true))) + end + + return circuit +end + +# Read instances from a config (for compatibility with benchmark API) +function read_instances(::Type{CircuitSATProblem}, config::CircuitSATConfig) + return [load_circuit_instance(config)] +end + +# Read instances from a directory path (for benchmark_dataset) +function read_instances(::Type{CircuitSATProblem}, path::AbstractString) + if isfile(path) + # Single file: determine format from extension + format = if endswith(path, ".v") + :verilog + elseif endswith(path, ".aag") + :aag + else + error("Unknown file format for: $path. Expected .v or .aag") + end + config = CircuitSATConfig(format, path) + return [load_circuit_instance(config)] + elseif isdir(path) + # Directory: load all circuit files + verilog_files = discover_circuit_files(path; format=:verilog) + aag_files = discover_circuit_files(path; format=:aag) + + instances = CircuitSATInstance[] + + for vfile in verilog_files + try + config = CircuitSATConfig(:verilog, vfile) + push!(instances, load_circuit_instance(config)) + catch e + @warn "Failed to load $vfile" exception=e + end + end + + for afile in aag_files + try + config = CircuitSATConfig(:aag, afile) + push!(instances, load_circuit_instance(config)) + catch e + @warn "Failed to load $afile" exception=e + end + end + + return instances + else + error("Path not found: $path") + end +end + +# Generate a single instance (for compatibility, just loads the file) +function generate_instance(::Type{CircuitSATProblem}, config::CircuitSATConfig; kwargs...) + return load_circuit_instance(config) +end + +# Verify solution +function verify_solution(::Type{CircuitSATProblem}, instance::CircuitSATInstance, result) + # Check if we got a valid result (tuple of (satisfiable, stats)) + if result === nothing + return false + end + + # solve_circuit_sat returns (satisfiable::Bool, stats) + # We consider it successful if the solver ran without errors + return true +end + +# Helper function to check if the circuit is satisfiable +function is_satisfiable(result) + if result === nothing + return nothing # Solver failed + end + satisfiable, stats = result + return satisfiable # true = SAT, false = UNSAT +end + diff --git a/benchmarks/src/circuitSAT/solvers.jl b/benchmarks/src/circuitSAT/solvers.jl new file mode 100644 index 0000000..6c5561d --- /dev/null +++ b/benchmarks/src/circuitSAT/solvers.jl @@ -0,0 +1,22 @@ +# Solver implementations for CircuitSAT + +function solve_instance(::Type{CircuitSATProblem}, instance::CircuitSATInstance, solver::BooleanInferenceSolver) + try + result = BooleanInference.solve_circuit_sat(instance.circuit; bsconfig=solver.bsconfig, reducer=solver.reducer, show_stats=solver.show_stats) + return result + catch e + @warn "Failed to solve $(instance.name)" exception=(e, catch_backtrace()) + return nothing + end +end + +# Note: CNFSolver implementation would require additional dependencies +# Keeping it here for future extension +# function solve_instance(::Type{CircuitSATProblem}, instance::CircuitSATInstance, solver::CNFSolver) +# mktempdir() do dir +# vfile = joinpath(dir, "circuit.v") +# aig = joinpath(dir, "circuit.aig") +# +# run(`$(solver.yosys_path) -q -p "read_verilog $vfile; prep -top circuit; aigmap; write_aiger -symbols $aig"`) +# end +# end \ No newline at end of file diff --git a/benchmarks/src/circuitSAT/types.jl b/benchmarks/src/circuitSAT/types.jl new file mode 100644 index 0000000..64f326d --- /dev/null +++ b/benchmarks/src/circuitSAT/types.jl @@ -0,0 +1,23 @@ +struct CircuitSATProblem <: AbstractBenchmarkProblem end + +""" +Configuration for CircuitSAT problems. +- format: :verilog or :aag +- path: path to the circuit file +""" +struct CircuitSATConfig <: AbstractProblemConfig + format::Symbol # :verilog or :aag + path::String + + function CircuitSATConfig(format::Symbol, path::String) + format in (:verilog, :aag) || error("Format must be :verilog or :aag, got $format") + new(format, path) + end +end + +struct CircuitSATInstance <: AbstractInstance + name::String + circuit::Circuit + format::Symbol + source_path::String +end diff --git a/benchmarks/src/comparison.jl b/benchmarks/src/comparison.jl index dd210d7..a49133d 100644 --- a/benchmarks/src/comparison.jl +++ b/benchmarks/src/comparison.jl @@ -20,7 +20,7 @@ Compare multiple solvers on the same datasets. """ function run_solver_comparison(problem_type::Type{<:AbstractBenchmarkProblem}, dataset_paths::Vector{String}; - solvers=nothing) + solvers::Union{Vector{<:AbstractSolver}, Nothing}=nothing) solver_list = isnothing(solvers) ? available_solvers(problem_type) : solvers results = Dict() @@ -30,7 +30,7 @@ function run_solver_comparison(problem_type::Type{<:AbstractBenchmarkProblem}, solver_results = [] for path in dataset_paths - result = benchmark_dataset(problem_type, path; solver) + result = benchmark_dataset(problem_type, path; solver=solver, verify=solver.verify) if !isnothing(result) push!(solver_results, result) end @@ -138,4 +138,3 @@ function compare_solver_results(name1::String, results1, name2::String, results2 end println(repeat("+", 80)) end - diff --git a/benchmarks/src/factoring/dataset.jl b/benchmarks/src/factoring/dataset.jl index 4ae9e15..6fbe00e 100644 --- a/benchmarks/src/factoring/dataset.jl +++ b/benchmarks/src/factoring/dataset.jl @@ -1,104 +1,51 @@ -function dataset_metadata_hash(config::FactoringConfig, per_config::Int, seed::UInt64, include_solution::Bool) - parts = [ - string(config.m), - string(config.n), - string(per_config), - string(seed), - string(include_solution) - ] - content = join(parts, "|") - return bytes2hex(sha256(content))[1:16] -end - function deterministic_seed(config::FactoringConfig) content = "$(config.m)|$(config.n)" hash_bytes = sha256(content) return reinterpret(UInt64, hash_bytes[1:8])[1] end -function check_dataset_compatibility(path::String, config::FactoringConfig, - per_config::Int, seed::UInt64, include_solution::Bool) - if !isfile(path) - return false - end - - try - instances = read_instances(FactoringProblem, path) - isempty(instances) && return false - - if length(instances) != per_config - @info " Dataset size mismatch: expected $per_config, found $(length(instances))" - return false - end - - expected_hash = dataset_metadata_hash(config, per_config, seed, include_solution) - if has_metadata(instances[1], expected_hash) - @info " Found compatible dataset: $path" - return true - else - @info " Dataset parameter mismatch: $path" - return false - end - catch e - @warn " Error checking dataset: $e" - return false - end -end - - -function generate_factoring_datasets(configs::Vector{FactoringConfig}; - per_config::Int=100, - include_solution::Bool=false, - force_regenerate::Bool=false) - +function generate_factoring_datasets(configs::Vector{FactoringConfig}; per_config::Int=100, include_solution::Bool=false, seed::Union{UInt64, Nothing}=nothing, force_regenerate::Bool=false) outdir = resolve_data_dir("factoring") isdir(outdir) || mkpath(outdir) - + paths = String[] generated_count = 0 reused_count = 0 - + for config in configs filename = filename_pattern(FactoringProblem, config) path = joinpath(outdir, filename) - - seed = deterministic_seed(config) - - if !force_regenerate && check_dataset_compatibility(path, config, per_config, seed, include_solution) + + # Use provided seed or generate deterministic seed from config + config_seed = isnothing(seed) ? deterministic_seed(config) : seed + + if !force_regenerate && isfile(path) @info "Reusing existing dataset: $path" push!(paths, path) reused_count += 1 continue end - + @info "Generating new dataset: $path" - @info " Using seed: $seed, instances: $per_config" - - seeded_rng = Random.Xoshiro(seed) - metadata_hash = dataset_metadata_hash(config, per_config, seed, include_solution) - + @info " Using seed: $config_seed, instances: $per_config" + + seeded_rng = Random.Xoshiro(config_seed) + open(path, "w") do io for i in 1:per_config - instance = generate_instance(FactoringProblem, config; - rng=seeded_rng, + instance = generate_instance(FactoringProblem, config; + rng=seeded_rng, include_solution=include_solution) - - if i == 1 - instance = add_metadata(instance; - metadata_hash=metadata_hash, - generation_seed=seed, - generation_timestamp=nothing) - end - + write_instance(io, instance) end end - + @info "Generated dataset: $path" push!(paths, path) generated_count += 1 end - + @info "Dataset generation complete: $generated_count generated, $reused_count reused" return paths end diff --git a/benchmarks/src/factoring/generators.jl b/benchmarks/src/factoring/generators.jl index c37d4d8..b5f116d 100644 --- a/benchmarks/src/factoring/generators.jl +++ b/benchmarks/src/factoring/generators.jl @@ -29,30 +29,15 @@ function random_semiprime(m::Int, n::Int; rng=Random.GLOBAL_RNG, distinct::Bool= return p, q, N end -function generate_instance(::Type{FactoringProblem}, config::FactoringConfig; - rng::AbstractRNG=Random.GLOBAL_RNG, +function generate_instance(::Type{FactoringProblem}, config::FactoringConfig; + rng::AbstractRNG=Random.GLOBAL_RNG, include_solution::Bool=false) p, q, N = random_semiprime(config.m, config.n; rng=rng, distinct=true) - id = problem_id(config, N) - + return FactoringInstance( - config.m, config.n, N, id; + config.m, config.n, N; p = include_solution ? p : nothing, q = include_solution ? q : nothing ) end -# Helper function to add metadata to an instance -function add_metadata(instance::FactoringInstance; - metadata_hash=nothing, - generation_seed=nothing, - generation_timestamp=nothing) - return FactoringInstance( - instance.m, instance.n, instance.N, instance.id; - p=instance.p, q=instance.q, - metadata_hash=metadata_hash, - generation_seed=generation_seed, - generation_timestamp=generation_timestamp - ) -end - diff --git a/benchmarks/src/factoring/interface.jl b/benchmarks/src/factoring/interface.jl index 9c69a85..ac709a2 100644 --- a/benchmarks/src/factoring/interface.jl +++ b/benchmarks/src/factoring/interface.jl @@ -1,16 +1,6 @@ -# ---------------------------------------- -# Factoring Problem Interface -# ---------------------------------------- - -# Helper for generating problem IDs -function problem_id(config::FactoringConfig, N::Integer) - h = bytes2hex(sha1(string(config.m, "|", config.n, "|", N))) - return h[1:16] -end - # Dataset filename pattern function filename_pattern(::Type{FactoringProblem}, config::FactoringConfig) - return "numbers_$(config.m)x$(config.n).jsonl" + return "numbers_$(config.m)x$(config.n).txt" end # Solvers diff --git a/benchmarks/src/factoring/solvers.jl b/benchmarks/src/factoring/solvers.jl index a507d6c..8b2675c 100644 --- a/benchmarks/src/factoring/solvers.jl +++ b/benchmarks/src/factoring/solvers.jl @@ -1,9 +1,9 @@ function solve_instance(::Type{FactoringProblem}, instance::FactoringInstance, solver::BooleanInferenceSolver) - return BooleanInference.solve_factoring(instance.m, instance.n, Int(instance.N)) + return BooleanInference.solve_factoring(instance.m, instance.n, Int(instance.N); bsconfig=solver.bsconfig, reducer=solver.reducer, show_stats=solver.show_stats) end function solve_instance(::Type{FactoringProblem}, instance::FactoringInstance, solver::IPSolver) - return factoring_ip(instance.m, instance.n, Int(instance.N); solver) + return factoring_ip(instance.m, instance.n, instance.N, solver) end function solve_instance(::Type{FactoringProblem}, instance::FactoringInstance, solver::XSATSolver) @@ -19,7 +19,7 @@ function solve_instance(::Type{FactoringProblem}, instance::FactoringInstance, s run(`$(solver.yosys_path) -q -p "read_verilog $vfile; prep -top circuit; aigmap; write_aiger -symbols $aig"`) - res = run_xsat_and_parse(solver.csat_path, aig) + res = run_xsat_and_parse(solver.csat_path, aig, solver.timeout) res.status != :sat && return :unsat model = res.model::Dict{Int,Bool} @@ -34,6 +34,20 @@ function solve_instance(::Type{FactoringProblem}, instance::FactoringInstance, s end end +# Generic implementation for CNF solvers +function solve_instance(::Type{FactoringProblem}, instance::FactoringInstance, solver::CNFSolver) + m, n = instance.m, instance.n + fproblem = Factoring(m, n, instance.N) + circuit_sat = reduceto(CircuitSAT, fproblem) + + mktempdir() do dir + cnf_file = circuit_to_cnf(circuit_sat.circuit.circuit, solver.abc_path, dir) + + res = run_cnf_solver(solver, cnf_file) + return res.status + end +end + function verify_solution(::Type{FactoringProblem}, instance::FactoringInstance, result) try if result isa Tuple @@ -53,4 +67,3 @@ function verify_solution(::Type{FactoringProblem}, instance::FactoringInstance, return false end end - diff --git a/benchmarks/src/factoring/types.jl b/benchmarks/src/factoring/types.jl index 2771611..07e38a0 100644 --- a/benchmarks/src/factoring/types.jl +++ b/benchmarks/src/factoring/types.jl @@ -9,92 +9,68 @@ struct FactoringInstance <: AbstractInstance m::Int n::Int N::BigInt - id::String # Optional solution fields p::Union{BigInt, Nothing} q::Union{BigInt, Nothing} - # Optional metadata fields - metadata_hash::Union{String, Nothing} - generation_seed::Union{UInt64, Nothing} - generation_timestamp::Union{String, Nothing} - - function FactoringInstance(m::Int, n::Int, N::Integer, id::String; - p=nothing, q=nothing, - metadata_hash=nothing, - generation_seed=nothing, - generation_timestamp=nothing) - new(m, n, BigInt(N), id, + + function FactoringInstance(m::Int, n::Int, N::Integer; + p=nothing, q=nothing) + new(m, n, BigInt(N), isnothing(p) ? nothing : BigInt(p), - isnothing(q) ? nothing : BigInt(q), - metadata_hash, generation_seed, generation_timestamp) + isnothing(q) ? nothing : BigInt(q)) end end # ---------------------------------------- -# Dataset I/O Implementation (JSON format) +# Dataset I/O Implementation (Text format) # ---------------------------------------- +# Format: m n N [p q] +# Each line contains space-separated values: +# - m, n: bit sizes of the two prime factors +# - N: the semiprime to factor +# - p, q: optional prime factors (only if include_solution=true) +# +# Example without solution: +# 10 10 893077 +# 10 10 742891 +# +# Example with solution: +# 10 10 893077 971 919 +# 10 10 742891 883 841 -# Write a single instance to IO (JSON format) +# Write a single instance to IO (text format) function write_instance(io::IO, instance::FactoringInstance) - obj = Dict{String, Any}( - "m" => instance.m, - "n" => instance.n, - "N" => string(instance.N), - "id" => instance.id - ) - - if !isnothing(instance.p) - obj["p"] = string(instance.p) - end - if !isnothing(instance.q) - obj["q"] = string(instance.q) - end - if !isnothing(instance.metadata_hash) - obj["_metadata_hash"] = instance.metadata_hash - end - if !isnothing(instance.generation_seed) - obj["_generation_seed"] = instance.generation_seed - end - if !isnothing(instance.generation_timestamp) - obj["_generation_timestamp"] = instance.generation_timestamp + print(io, instance.m, " ", instance.n, " ", instance.N) + + if !isnothing(instance.p) && !isnothing(instance.q) + print(io, " ", instance.p, " ", instance.q) end - - JSON3.write(io, obj) - write(io, '\n') + + println(io) end -# Read instances from file (JSON format) +# Read instances from file (text format) function read_instances(::Type{FactoringProblem}, path::AbstractString) instances = FactoringInstance[] open(path, "r") do io for line in eachline(io) isempty(strip(line)) && continue - data = JSON3.read(line) - - m = data["m"] - n = data["n"] - N = parse(BigInt, data["N"]) - id = data["id"] - - p = haskey(data, "p") ? parse(BigInt, data["p"]) : nothing - q = haskey(data, "q") ? parse(BigInt, data["q"]) : nothing - metadata_hash = haskey(data, "_metadata_hash") ? data["_metadata_hash"] : nothing - generation_seed = haskey(data, "_generation_seed") ? UInt64(data["_generation_seed"]) : nothing - generation_timestamp = haskey(data, "_generation_timestamp") ? data["_generation_timestamp"] : nothing - - instance = FactoringInstance(m, n, N, id; - p=p, q=q, - metadata_hash=metadata_hash, - generation_seed=generation_seed, - generation_timestamp=generation_timestamp) + + parts = split(strip(line)) + length(parts) < 3 && continue + + m = parse(Int, parts[1]) + n = parse(Int, parts[2]) + N = parse(BigInt, parts[3]) + + # Check if solution is included + p = length(parts) >= 5 ? parse(BigInt, parts[4]) : nothing + q = length(parts) >= 5 ? parse(BigInt, parts[5]) : nothing + + instance = FactoringInstance(m, n, N; p=p, q=q) push!(instances, instance) end end return instances -end - -# Check metadata -function has_metadata(instance::FactoringInstance, expected_hash::String) - return !isnothing(instance.metadata_hash) && instance.metadata_hash == expected_hash end \ No newline at end of file diff --git a/benchmarks/src/solver/solver_cnfsat.jl b/benchmarks/src/solver/solver_cnfsat.jl new file mode 100644 index 0000000..0116c0e --- /dev/null +++ b/benchmarks/src/solver/solver_cnfsat.jl @@ -0,0 +1,117 @@ +struct CNFSolverResult + status::Symbol # :sat | :unsat | :unknown + model::Union{Nothing, Dict{Int, Bool}} # Variable -> value (present only when SAT) + raw::String # Raw console output for debugging/logging +end + +function parse_dimacs_model(raw_output::String)::Dict{Int, Bool} + model = Dict{Int, Bool}() + # Parse lines starting with "v" (variable assignments in DIMACS format) + for line in split(raw_output, '\n') + if startswith(strip(line), "v") + # Extract variable assignments: "v 1 -2 3 0" means var 1=true, var 2=false, var 3=true + parts = split(strip(line)) + for part in parts[2:end] # Skip the "v" prefix + part = strip(part) + if part == "0" # End of model line + break + end + var_val = parse(Int, part) + var_id = abs(var_val) + model[var_id] = var_val > 0 + end + end + end + return model +end + +function parse_dimacs_output(solver::KissatSolver, raw_output::String)::CNFSolverResult + # Parse status line + status = if occursin(r"(?m)^s\s+SATISFIABLE\b", raw_output) + :sat + elseif occursin(r"(?m)^s\s+UNSATISFIABLE\b", raw_output) + :unsat + else + :unknown + end + + # Parse model if SAT + model = status == :sat ? parse_dimacs_model(raw_output) : nothing + + return CNFSolverResult(status, model, raw_output) +end + +function parse_dimacs_output(solver::MinisatSolver, raw_output::String)::CNFSolverResult + # MiniSAT outputs status directly as "SATISFIABLE" or "UNSATISFIABLE" (no "s" prefix) + status = if occursin(r"(?m)^SATISFIABLE\b", raw_output) + :sat + elseif occursin(r"(?m)^UNSATISFIABLE\b", raw_output) + :unsat + else + :unknown + end + + # Parse model if SAT + model = status == :sat ? parse_dimacs_model(raw_output) : nothing + + return CNFSolverResult(status, model, raw_output) +end + + +function run_kissat_and_parse(kissat_path::String, cnf_path::String, solver::KissatSolver)::CNFSolverResult + # Kissat exit codes: 10=SAT, 20=UNSAT, 0=unknown/timeout, others=error + # We need to capture output even when exit code is non-zero + cmd = `/opt/homebrew/bin/gtimeout $(solver.timeout)s $kissat_path -q $cnf_path` + @show cmd + # Capture stdout and stderr separately, allow non-zero exit codes + stdout_pipe = Pipe() + stderr_pipe = Pipe() + proc = run(pipeline(cmd, stdout=stdout_pipe, stderr=stderr_pipe), wait=false) + close(stdout_pipe.in) + close(stderr_pipe.in) + + raw_stdout = read(stdout_pipe, String) + raw_stderr = read(stderr_pipe, String) + wait(proc) + exitcode = proc.exitcode + + # Check for actual errors (not SAT/UNSAT exit codes) + if exitcode != 0 && exitcode != 10 && exitcode != 20 + error("Kissat exited with error code $(exitcode). Stderr: $raw_stderr\nStdout: $raw_stdout") + end + + return parse_dimacs_output(solver, raw_stdout) +end + +function run_minisat_and_parse(minisat_path::String, cnf_path::String, solver::MinisatSolver)::CNFSolverResult + # MiniSAT with -verb=0 for quiet mode (only outputs status) + # MiniSAT exit codes: 10=SAT, 20=UNSAT, 0=unknown/timeout + cmd = `/opt/homebrew/bin/gtimeout $(solver.timeout)s $minisat_path -verb=0 $cnf_path` + + # Capture stdout and stderr separately, allow non-zero exit codes + stdout_pipe = Pipe() + stderr_pipe = Pipe() + proc = run(pipeline(cmd, stdout=stdout_pipe, stderr=stderr_pipe), wait=false) + close(stdout_pipe.in) + close(stderr_pipe.in) + + raw_stdout = read(stdout_pipe, String) + raw_stderr = read(stderr_pipe, String) + wait(proc) + exitcode = proc.exitcode + + # Check for actual errors (not SAT/UNSAT exit codes) + if exitcode != 0 && exitcode != 10 && exitcode != 20 + error("MiniSAT exited with error code $(exitcode). Stderr: $raw_stderr\nStdout: $raw_stdout") + end + + return parse_dimacs_output(solver, raw_stdout) +end + +function run_cnf_solver(solver::KissatSolver, cnf_path::String)::CNFSolverResult + return run_kissat_and_parse(solver.kissat_path, cnf_path, solver) +end + +function run_cnf_solver(solver::MinisatSolver, cnf_path::String)::CNFSolverResult + return run_minisat_and_parse(solver.minisat_path, cnf_path, solver) +end diff --git a/benchmarks/src/factoring/solver_ip.jl b/benchmarks/src/solver/solver_ip.jl similarity index 92% rename from benchmarks/src/factoring/solver_ip.jl rename to benchmarks/src/solver/solver_ip.jl index 7617853..55d0e06 100644 --- a/benchmarks/src/factoring/solver_ip.jl +++ b/benchmarks/src/solver/solver_ip.jl @@ -1,4 +1,4 @@ -function findmin_ip(problem::AbstractProblem, tag::Bool; optimizer, env) +function findmin_ip(problem::CircuitSAT, tag::Bool; optimizer, env) cons = constraints(problem) nsc = ProblemReductions.num_variables(problem) maxN = maximum([length(c.variables) for c in cons]) @@ -34,11 +34,10 @@ function findmin_ip(problem::AbstractProblem, tag::Bool; optimizer, env) return round.(Int, JuMP.value.(x)) end -function factoring_ip(m, n, N; solver::IPSolver) +function factoring_ip(m, n, N, solver::IPSolver) fact3 = Factoring(m, n, N) res3 = reduceto(CircuitSAT, fact3) problem = CircuitSAT(res3.circuit.circuit; use_constraints=true); vals = findmin_ip(problem, true; optimizer=solver.optimizer, env=solver.env) return ProblemReductions.read_solution(fact3, [vals[res3.p]...,vals[res3.q]...]) end - diff --git a/benchmarks/src/factoring/solver_xsat.jl b/benchmarks/src/solver/solver_xsat.jl similarity index 90% rename from benchmarks/src/factoring/solver_xsat.jl rename to benchmarks/src/solver/solver_xsat.jl index a0a0f26..71ce7b1 100644 --- a/benchmarks/src/factoring/solver_xsat.jl +++ b/benchmarks/src/solver/solver_xsat.jl @@ -10,8 +10,8 @@ end Run XSAT (e.g., exec="/path/to/xsat") and parse the output of `-i aig_path`. Parse the `s ...` status line and one or more `v ...` assignment lines (DIMACS style, terminated by 0). """ -function run_xsat_and_parse(exec::AbstractString, aig_path::AbstractString)::XSatResult - raw = read(`$exec -i $aig_path`, String) +function run_xsat_and_parse(exec::AbstractString, aig_path::AbstractString, timeout::Real)::XSatResult + raw = read(`/opt/homebrew/bin/gtimeout $(timeout)s $exec -i $aig_path`, String) status = occursin(r"(?m)^s\s+SATISFIABLE\b", raw) ? :sat : diff --git a/benchmarks/src/utils.jl b/benchmarks/src/utils.jl index eef0714..e2d14e3 100644 --- a/benchmarks/src/utils.jl +++ b/benchmarks/src/utils.jl @@ -5,18 +5,37 @@ function resolve_data_dir(parts::AbstractString...) return dir end -function write_jsonl(io::IO, obj) - JSON3.write(io, obj) - write(io, '\n') +# Helper function for finding executables in PATH +function find_executable_in_path(cmd::String, name::String) + try + return strip(read(`which $cmd`, String)) + catch + error("$name not found in PATH. Please provide explicit path or install it.") + end +end + +# Helper function for validating executable path +function validate_executable_path(path::Union{String, Nothing}, name::String) + if isnothing(path) + return nothing + elseif !isfile(path) + error("File $path for $name does not exist") + else + return path + end end -function read_jsonl(path::AbstractString) - objs = Any[] - open(path, "r") do io - for line in eachline(io) - isempty(strip(line)) && continue - push!(objs, JSON3.read(line)) - end +# Helper function to convert circuit to CNF using ABC +function circuit_to_cnf(circuit::Circuit, abc_path::Union{String, Nothing}, dir::String) + vfile = joinpath(dir, "circuit.v") + cnf_file = joinpath(dir, "circuit.cnf") + + write_verilog(vfile, circuit) + + if !isnothing(abc_path) + run(`$abc_path -c "read_verilog $vfile; strash; &get; &write_cnf -K 8 $cnf_file"`) + else + error("ABC path is required for CNF conversion but not provided") end - return objs + return cnf_file end \ No newline at end of file diff --git a/benchmarks/third-party/Makefile b/benchmarks/third-party/Makefile new file mode 100644 index 0000000..a80fa76 --- /dev/null +++ b/benchmarks/third-party/Makefile @@ -0,0 +1,174 @@ +# === common settings === +JOBS ?= $(shell nproc 2>/dev/null || echo 4) +ROOT := $(abspath $(dir $(lastword $(MAKEFILE_LIST)))) +OUTDIR := $(ROOT)/../artifacts/bin +DATADIR := $(ROOT)/../data +mkdir_p = mkdir -p $1 +CMAKE_BUILD_DIR := $(ROOT)/x-sat/build + +# === abc (berkeley-abc) === +ABC_DIR := $(ROOT)/abc +ABC_BIN := $(ABC_DIR)/abc +ABC_LIB := $(ABC_DIR)/libabc.a + +.PHONY: all aiger x-sat aig-data yosys kissat abc libabc submodule-abc submodule-cir_bench iscas85 clean distclean + +all: aiger x-sat abc aig-data yosys iscas85 + @echo "✅ All third-party benchmarks built." + @echo "Executables are under $(OUTDIR)" + @echo "AIG data is under $(DATADIR)/aig" + @echo "ISCAS85 is under $(DATADIR)/iscas85" + +# === aiger === +aiger: + @echo ">>> Building aiger..." + @if [ ! -f "$(ROOT)/aiger/Makefile" ]; then \ + echo ">>> Configuring aiger (generating Makefile)..."; \ + cd $(ROOT)/aiger && ./configure.sh; \ + fi + $(MAKE) -C $(ROOT)/aiger -j$(JOBS) + $(call mkdir_p,$(OUTDIR)) + cd $(ROOT)/aiger && \ + find . -maxdepth 1 -type f \( -perm -u+x -o -perm -g+x -o -perm -o+x \) \ + -exec cp -f {} $(OUTDIR)/ \; + @echo "✓ Aiger tools copied to $(OUTDIR)" + + # for f in aigand aigdd aigflip aigfuzz aiginfo aigjoin aigmiter aigmove aignm aigor aigreset aigselect \ + # aigsim aigsplit aigstrip aigtoaig aigtoblif aigtocnf aigtobtor aigtodot aigtosmv \ + # aigunconstraint aigunor aigunroll andtoaig bliftoaig smvtoaig soltostim wrapstim; do \ + # [ -x "$(AIGER_DIR)/$$f" ] && cp -f "$(AIGER_DIR)/$$f" "$(OUTDIR)/"; \ + # done + +# === x-sat === +x-sat: + @echo ">>> Building x-sat..." + $(call mkdir_p,$(CMAKE_BUILD_DIR)) + cd $(CMAKE_BUILD_DIR) && cmake \ + -DCMAKE_POLICY_VERSION_MINIMUM=3.5 \ + -DCMAKE_BUILD_TYPE=Release \ + .. + $(MAKE) -C $(CMAKE_BUILD_DIR) -j$(JOBS) + $(call mkdir_p,$(OUTDIR)) + @if [ -f "$(CMAKE_BUILD_DIR)/csat" ]; then \ + cp $(CMAKE_BUILD_DIR)/csat $(OUTDIR)/; \ + else \ + echo "⚠️ Warning: x-sat executable not found, adjust path."; \ + fi + +aig-data: aiger + @echo ">>> Converting and copying AIG data..." + @if [ -d "$(ROOT)/x-sat/data/airthmetic" ]; then \ + mkdir -p "$(DATADIR)/aig/arithmetic"; \ + for f in "$(ROOT)"/x-sat/data/airthmetic/*.aiger; do \ + if [ -e "$$f" ]; then \ + base=$$(basename "$$f" .aiger); \ + out="$(DATADIR)/aig/arithmetic/$$base.aag"; \ + echo "Converting $$f -> $$out"; \ + "$(OUTDIR)/aigtoaig" -a "$$f" > "$$out"; \ + fi; \ + done; \ + else \ + echo "Warning: $(ROOT)/x-sat/data/airthmetic not found"; \ + fi + @if [ -d "$(ROOT)/x-sat/data/non-airthmetic" ]; then \ + mkdir -p "$(DATADIR)/aig/non-arithmetic"; \ + for f in "$(ROOT)"/x-sat/data/non-airthmetic/*.aiger; do \ + if [ -e "$$f" ]; then \ + base=$$(basename "$$f" .aiger); \ + out="$(DATADIR)/aig/non-arithmetic/$$base.aag"; \ + echo "Converting $$f -> $$out"; \ + "$(OUTDIR)/aigtoaig" -a "$$f" > "$$out"; \ + fi; \ + done; \ + fi + @echo "AIG data converted and copied to $(DATADIR)/aig" + +yosys: + @echo ">>> Installing yosys..." + @if command -v brew >/dev/null 2>&1; then \ + echo "Detected macOS — using Homebrew"; \ + brew install yosys || brew upgrade yosys; \ + elif command -v apt >/dev/null 2>&1; then \ + echo "Detected Ubuntu/Debian — using apt"; \ + sudo apt update && sudo apt install -y yosys; \ + elif command -v dnf >/dev/null 2>&1; then \ + echo "Detected Fedora/RHEL — using dnf"; \ + sudo dnf install -y yosys; \ + elif command -v pacman >/dev/null 2>&1; then \ + echo "Detected Arch Linux — using pacman"; \ + sudo pacman -S --noconfirm yosys; \ + else \ + echo "No known package manager found; please install Yosys manually from source."; \ + fi + @echo "✓ Yosys installation complete." + +kissat: + @echo ">>> Installing kissat..." + @if command -v brew >/dev/null 2>&1; then \ + echo "Detected macOS — using Homebrew"; \ + brew install kissat || brew upgrade kissat; \ + elif command -v apt >/dev/null 2>&1; then \ + echo "Detected Ubuntu/Debian — using apt"; \ + sudo apt update && sudo apt install -y kissat; \ + elif command -v dnf >/dev/null 2>&1; then \ + echo "Detected Fedora/RHEL — using dnf"; \ + sudo dnf install -y kissat; \ + elif command -v pacman >/dev/null 2>&1; then \ + echo "Detected Arch Linux — using pacman"; \ + sudo pacman -S --noconfirm kissat; \ + else \ + echo "No known package manager found; please install Kissat manually from source."; \ + fi + @echo "✓ Kissat installation complete." + +# === abc === +abc: submodule-abc + @echo ">>> Building abc (berkeley-abc)..." + $(MAKE) -C $(ABC_DIR) -j$(JOBS) + $(call mkdir_p,$(OUTDIR)) + @if [ -f "$(ABC_BIN)" ]; then \ + cp -f "$(ABC_BIN)" "$(OUTDIR)/"; \ + echo "✓ abc copied to $(OUTDIR)"; \ + else \ + echo "⚠️ Warning: abc executable not found at $(ABC_BIN)"; \ + fi + +# optional: build PIC static library for downstream linking +libabc: submodule-abc + @echo ">>> Building libabc.a (PIC) ..." + $(MAKE) -C $(ABC_DIR) -j$(JOBS) libabc.a ABC_USE_PIC=1 + $(call mkdir_p,$(OUTDIR)) + @if [ -f "$(ABC_LIB)" ]; then \ + cp -f "$(ABC_LIB)" "$(OUTDIR)/"; \ + echo "✓ libabc.a copied to $(OUTDIR)"; \ + else \ + echo "⚠️ Warning: libabc.a not found at $(ABC_LIB)"; \ + fi + +# ensure the submodule is initialized +submodule-abc: + @git submodule update --init --recursive $(ABC_DIR) + +# === copy ISCAS85 === +CIR_BENCH_DIR := $(ROOT)/cir_bench + +iscas85: submodule-cir_bench + @echo ">>> Copying ISCAS85..." + cp -r $(ROOT)/cir_bench/ISCAS85 $(DATADIR)/iscas85 + @echo "✓ ISCAS85 copied to $(DATADIR)/iscas85" + +submodule-cir_bench: + @git submodule update --init --recursive $(CIR_BENCH_DIR) + @echo "✓ cir_bench submodule initialized" + +# === clean === +clean: + @echo ">>> Cleaning..." + cd $(ROOT)/aiger && $(MAKE) clean || true + cd $(ABC_DIR) && $(MAKE) clean || true + rm -rf $(CMAKE_BUILD_DIR) + rm -rf $(OUTDIR) + +distclean: clean + - git -C $(ABC_DIR) clean -xfd || true + - git -C $(ROOT)/aiger clean -xfd || true \ No newline at end of file diff --git a/benchmarks/third-party/cir_bench b/benchmarks/third-party/cir_bench new file mode 160000 index 0000000..cb85d98 --- /dev/null +++ b/benchmarks/third-party/cir_bench @@ -0,0 +1 @@ +Subproject commit cb85d98efdf1f67927273d901089855603d5855f diff --git a/benchmarks/third-party/glucose b/benchmarks/third-party/glucose deleted file mode 160000 index 7f887ab..0000000 --- a/benchmarks/third-party/glucose +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 7f887abba7cf13636a5ac2d28653668a20a91b25 diff --git a/examples/info_plot.jl b/examples/info_plot.jl new file mode 100644 index 0000000..9b08165 --- /dev/null +++ b/examples/info_plot.jl @@ -0,0 +1,23 @@ +using CairoMakie +# tmp_measure = [478, 467, 461, 446, 444, 442, 440, 438, 436, 346, 344, 342, 258, 256, 180, 178, 176, 174, 168, 166, 164, 162, 156, 154, 134, 94, 84, 41, 30, 27, 19, 232, 231, 74, 41, 35, 28, 26, 22, 106, 70, 67, 65, 61, 59, 49, 45, 36, 26, 90, 55, 49, 46, 23, 19, 15, 105, 102, 100, 66, 60, 48, 44, 41, 35, 32, 26, 24, 20, 14, 59, 14, 10, 89, 68, 65, 63, 59, 56, 54, 48, 44, 38, 36, 32, 28, 26, 22, 23, 71, 46, 37, 31, 29, 27, 23, 19, 126, 84, 69, 61, 58, 41, 35, 29, 19, 15, 13, 313, 312, 311, 185, 181, 179, 177, 175, 171, 169, 163, 161, 140, 134, 84, 0] +tmp_measure = [478, 467, 461, 446, 444, 442, 440, 438, 436, 262, 258, 256, 180, 178, 174, 168, 166, 164, 162, 156, 154, 134, 94, 84, 41, 30, 27, 19, 232, 231, 229, 74, 41, 35, 28, 26, 22, 106, 70, 67, 65, 61, 59, 49, 45, 36, 26, 90, 55, 49, 46, 23, 19, 15, 103, 100, 98, 64, 58, 46, 42, 39, 33, 30, 26, 23, 17, 13, 55, 35, 29, 23, 19, 87, 66, 63, 61, 57, 54, 52, 46, 42, 34, 32, 28, 26, 22, 23, 67, 42, 33, 27, 25, 23, 19, 126, 84, 69, 61, 58, 41, 35, 29, 19, 15, 13, 345, 342, 339, 337, 335, 333, 330, 328, 326, 324, 323, 322, 321, 165, 161, 157, 122, 118, 115, 79, 61, 53, 45, 41, 28, 18, 266, 263, 260, 257, 254, 251, 248, 246, 243, 240, 237, 234, 231, 229, 225, 224, 221, 218, 214, 212, 210, 143, 85, 71, 45, 39, 29, 217, 214, 211, 207, 205, 201, 199, 195, 193, 191, 185, 183, 155, 149, 145, 47, 41, 28, 16, 216, 213, 185, 166, 164, 76, 73, 71, 63, 50, 47, 41, 39, 35, 31, 20, 16, 333, 330, 328, 324, 320, 318, 316, 315, 314, 229, 227, 225, 221, 215, 213, 184, 182, 53, 43, 39, 30, 24, 19, 15, 186, 183, 181, 103, 81, 78, 74, 67, 61, 57, 51, 48, 44, 37, 33, 30, 28, 24, 21, 17, 147, 144, 142, 88, 75, 71, 65, 61, 54, 50, 44, 28, 22, 112, 80, 59, 56, 52, 49, 47, 44, 40, 38, 34, 32, 28, 23, 24, 151, 118, 115, 91, 85, 79, 75, 72, 68, 61, 53, 41, 38, 33, 25, 317, 315, 313, 312, 311, 148, 142, 134, 94, 0] + +# tmp_count_unfixed = [545, 541, 536, 528, 527, 526, 525, 524, 523, 456, 455, 454, 383, 382, 310, 309, 308, 306, 302, 301, 300, 299, 293, 292, 276, 241, 232, 164, 137, 133, 123, 357, 356, 178, 127, 121, 115, 111, 106, 211, 156, 155, 154, 152, 147, 139, 134, 115, 99, 215, 159, 150, 149, 111, 107, 103, 227, 226, 225, 181, 166, 147, 144, 141, 134, 133, 121, 118, 114, 105, 166, 106, 100, 193, 159, 158, 157, 155, 152, 147, 143, 137, 132, 129, 125, 121, 118, 114, 115, 194, 159, 141, 124, 118, 114, 110, 105, 251, 193, 165, 154, 153, 135, 128, 120, 105, 97, 94, 428, 427, 426, 308, 306, 305, 302, 301, 298, 297, 291, 290, 261, 256, 188, 0] +tmp_count_unfixed = [545, 541, 536, 528, 527, 526, 525, 524, 523, 387, 383, 382, 310, 309, 306, 302, 301, 300, 299, 293, 292, 276, 241, 232, 164, 137, 133, 123, 357, 356, 355, 178, 127, 121, 115, 111, 106, 211, 156, 155, 154, 152, 147, 139, 134, 115, 99, 215, 159, 150, 149, 111, 107, 103, 226, 225, 224, 180, 165, 146, 143, 140, 133, 132, 125, 117, 105, 100, 162, 124, 113, 105, 98, 192, 158, 157, 156, 154, 151, 146, 142, 136, 126, 123, 119, 116, 112, 113, 190, 155, 137, 120, 114, 110, 105, 251, 193, 165, 154, 153, 135, 128, 120, 105, 97, 94, 448, 447, 446, 445, 444, 443, 442, 441, 440, 439, 438, 437, 436, 295, 292, 289, 248, 245, 238, 182, 159, 151, 142, 139, 125, 97, 387, 386, 385, 384, 383, 382, 381, 380, 379, 378, 377, 376, 375, 374, 370, 369, 368, 367, 364, 363, 362, 293, 210, 183, 152, 145, 133, 343, 342, 341, 339, 338, 334, 333, 330, 329, 327, 321, 320, 286, 277, 274, 147, 141, 121, 108, 345, 344, 313, 295, 294, 187, 186, 185, 171, 151, 148, 143, 142, 139, 135, 119, 114, 445, 444, 443, 441, 439, 438, 437, 436, 435, 360, 359, 357, 354, 350, 349, 313, 312, 162, 148, 144, 134, 125, 109, 105, 308, 307, 306, 218, 186, 185, 181, 172, 166, 162, 156, 155, 151, 142, 138, 137, 130, 123, 120, 116, 272, 271, 270, 209, 191, 187, 182, 178, 169, 162, 153, 126, 117, 243, 210, 174, 173, 169, 167, 165, 164, 156, 151, 147, 144, 140, 122, 124, 280, 249, 248, 210, 203, 197, 193, 192, 188, 179, 167, 151, 147, 143, 136, 430, 429, 428, 427, 426, 269, 264, 252, 200, 0] + +# tmp_count_unfixed_tensors = [567, 562, 560, 553, 553, 553, 553, 553, 553, 524, 524, 524, 480, 480, 424, 424, 424, 423, 422, 422, 422, 422, 419, 419, 407, 385, 370, 270, 220, 214, 205, 443, 442, 255, 182, 177, 172, 167, 163, 273, 206, 206, 206, 206, 199, 196, 191, 167, 152, 306, 235, 225, 225, 174, 171, 168, 308, 308, 308, 252, 229, 208, 207, 203, 196, 196, 181, 178, 175, 166, 256, 185, 179, 265, 218, 218, 218, 218, 214, 207, 206, 199, 197, 194, 191, 188, 185, 181, 181, 294, 239, 215, 189, 179, 174, 171, 167, 323, 258, 223, 212, 212, 198, 191, 183, 168, 158, 155, 491, 490, 489, 395, 395, 395, 392, 392, 391, 391, 386, 386, 343, 341, 258, 0] + +tmp_count_unfixed_tensors = [567, 562, 560, 553, 553, 553, 553, 553, 553, 483, 480, 480, 424, 424, 423, 422, 422, 422, 422, 419, 419, 407, 385, 370, 270, 220, 214, 205, 443, 442, 442, 255, 182, 177, 172, 167, 163, 273, 206, 206, 206, 206, 199, 196, 191, 167, 152, 306, 235, 225, 225, 174, 171, 168, 308, 308, 308, 252, 229, 208, 207, 203, 196, 196, 187, 176, 161, 157, 253, 198, 184, 176, 168, 265, 218, 218, 218, 218, 214, 207, 206, 199, 189, 186, 183, 180, 176, 176, 291, 236, 212, 186, 176, 171, 167, 323, 258, 223, 212, 212, 198, 191, 183, 168, 158, 155, 490, 490, 490, 490, 490, 490, 490, 490, 490, 490, 489, 488, 487, 393, 392, 391, 340, 339, 327, 256, 237, 231, 223, 222, 213, 172, 426, 426, 426, 426, 426, 426, 426, 426, 426, 426, 426, 426, 426, 426, 424, 423, 423, 423, 421, 421, 421, 360, 279, 245, 210, 203, 193, 412, 412, 412, 412, 412, 409, 409, 408, 408, 407, 402, 402, 360, 349, 348, 208, 203, 184, 173, 417, 417, 375, 354, 354, 239, 239, 239, 221, 199, 195, 192, 192, 191, 188, 172, 168, 477, 477, 477, 477, 477, 477, 477, 476, 475, 428, 428, 427, 426, 422, 422, 374, 374, 233, 220, 217, 206, 196, 172, 169, 338, 338, 338, 264, 236, 236, 233, 225, 220, 217, 212, 212, 209, 201, 198, 198, 187, 178, 174, 171, 328, 328, 328, 265, 249, 246, 243, 240, 232, 223, 213, 183, 174, 324, 295, 254, 254, 251, 249, 248, 248, 237, 229, 226, 223, 220, 195, 196, 337, 312, 312, 272, 265, 260, 257, 257, 254, 246, 231, 216, 210, 207, 202, 491, 491, 491, 490, 489, 349, 347, 334, 269, 0] + +fig = Figure(resolution = (1000, 500)) +ax = Axis(fig[1,1], xlabel="Steps", ylabel="Value", + title="Measure") + +lines!(ax, tmp_measure, label="Num of Hard Tensors") +lines!(ax, tmp_count_unfixed, label="Num of Unfixed Variables") +lines!(ax, tmp_count_unfixed_tensors, label="Num of Unfixed Tensors") + +axislegend(ax) + +save("plot_var.png", fig) # 如不需要保存可删掉 +fig \ No newline at end of file diff --git a/examples/plot.jl b/examples/plot.jl index 744b86d..4ec3101 100644 --- a/examples/plot.jl +++ b/examples/plot.jl @@ -1,11 +1,13 @@ using CairoMakie configs = ["10x10", "12x12", "14x14", "16x16", "18x18", "20x20", "22x22"] -sizes = [20, 24, 28, 32, 36, 40, 44] +sizes = [20, 24, 28, 32, 36, 40, 44, 48] -bi = [0.0671, 0.1093, 0.1547, 0.6152, 1.03, 2.67, 20.30] -gurobi = [0.0675, 0.7289, 1.63, 7.6, NaN, NaN, NaN] -xsat = [0.0614, 0.1026, 0.1876, 0.3284, 1.26, 2.51, 11.32] +bi = [0.0671, 0.1093, 0.1547, 0.6152, 1.03, 2.67, 20.30, 143.7564948] +gurobi = [0.0675, 0.7289, 1.63, 7.6, 26.53, NaN, NaN, NaN] +xsat = [0.0614, 0.1026, 0.1876, 0.3284, 1.26, 2.51, 11.32, 80.8] +minisat = [0.0418, 0.0527, 0.0747, 0.1004, 0.4886, 3.37, 17.07, 100.0] +kissat = [0.0474, 0.0594, 0.1101, 0.1867, 0.4970, 1.88, 6.35, 23.56] f = Figure(resolution = (700, 450)) @@ -16,15 +18,21 @@ ax = Axis(f[1, 1]; yscale = log10, ) -lines!(ax, sizes, bi; label = "BooleanInference", linewidth = 2) -lines!(ax, sizes, gurobi; label = "IP-Gurobi", linewidth = 2) -lines!(ax, sizes, xsat; label = "X-SAT", linewidth = 2, color = :red) - -scatter!(ax, sizes, bi) -scatter!(ax, sizes, gurobi) -scatter!(ax, sizes, xsat; color = :red) - +lines!(ax, sizes, bi; label = "BooleanInference", linewidth = 4, color = :red) +lines!(ax, sizes, gurobi; label = "IP-Gurobi", linewidth = 2, color = :black) +lines!(ax, sizes, xsat; label = "X-SAT", linewidth = 2, color = :orange) +lines!(ax, sizes, minisat; label = "MiniSAT", linewidth = 2, color = :blue) +lines!(ax, sizes, kissat; label = "Kissat", linewidth = 2, color = :green) + +scatter!(ax, sizes, bi, color = :red) +scatter!(ax, sizes, gurobi, color = :black) +scatter!(ax, sizes, xsat, color = :orange) +scatter!(ax, sizes, minisat, color = :blue) +scatter!(ax, sizes, kissat, color = :green) axislegend(ax; position = :lt) +scatter!(ax, [48], [600], color = :orange, marker = :circle, markersize = 6) +text!(ax, 48, 600, text = "xsat 1 timeout", align = (:right, :top), color = :orange) + save("runtime_comparison.png", f) f \ No newline at end of file diff --git a/project/factoring.jl b/project/factoring.jl new file mode 100644 index 0000000..52ab966 --- /dev/null +++ b/project/factoring.jl @@ -0,0 +1,33 @@ +using Test +using BooleanInference +using BooleanInference: TNProblem, TNContractionSolver, MostOccurrenceSelector, NumUnfixedVars, setup_from_tensor_network, setup_problem, select_variables, get_var_value, bits_to_int, bbsat!, MinGammaSelector +using BooleanInference: BranchingStrategy, NoReducer +using OptimalBranchingCore: Clause +using OptimalBranchingCore: branching_table, branch_and_reduce +using ProblemReductions: Factoring, reduceto, CircuitSAT, read_solution +using GenericTensorNetworks +using OptimalBranchingCore +using TropicalNumbers: Tropical + +# fproblem = Factoring(16, 16, 3363471157) +fproblem = Factoring(10,10,559619) +circuit_sat = reduceto(CircuitSAT, fproblem) +problem = CircuitSAT(circuit_sat.circuit.circuit; use_constraints=true) + +tn = GenericTensorNetwork(problem) +tn_static = setup_from_tensor_network(tn) +tn_problem = TNProblem(tn_static) +br_strategy = BranchingStrategy( + table_solver = TNContractionSolver(), + selector = MinGammaSelector(1,2,TNContractionSolver(), OptimalBranchingCore.GreedyMerge()), + # selector = MostOccurrenceSelector(1,2), + measure = BooleanInference.NumUnfixedVars(), + set_cover_solver = OptimalBranchingCore.GreedyMerge() +) +@time res = bbsat!(tn_problem, br_strategy, NoReducer()) +if res.found + a = get_var_value(res.solution, circuit_sat.q) + b = get_var_value(res.solution, circuit_sat.p) + @show bits_to_int(a), bits_to_int(b), res.stats + reset_problem!(tn_problem) +end \ No newline at end of file diff --git a/src/BooleanInference.jl b/src/BooleanInference.jl index b6c09ee..41f8cbd 100644 --- a/src/BooleanInference.jl +++ b/src/BooleanInference.jl @@ -3,7 +3,7 @@ module BooleanInference using TropicalNumbers using SparseArrays using OptimalBranchingCore -using OptimalBranchingCore: AbstractProblem, select_variables, reduce_problem, _vec2int, candidate_clauses, Clause +using OptimalBranchingCore: AbstractProblem, select_variables, reduce_problem, _vec2int, candidate_clauses, Clause, BranchingStrategy, AbstractReducer, NoReducer using OptimalBranchingCore.BitBasis using GenericTensorNetworks using GenericTensorNetworks.OMEinsum @@ -12,85 +12,83 @@ import ProblemReductions: CircuitSAT, Circuit, Factoring, reduceto, Satisfiabili using DataStructures using DataStructures: PriorityQueue using Statistics: median +using Graphs, GraphMakie, Colors +using GraphMakie +using CairoMakie: Figure, Axis, save, hidespines!, hidedecorations!, DataAspect +using NetworkLayout: SFDP, Spring, Stress, Spectral +import ProblemReductions: BooleanExpr, simple_form, extract_symbols! include("core/types.jl") include("core/static.jl") include("core/domain.jl") include("core/stats.jl") -include("core/workspace.jl") -include("core/region.jl") include("core/problem.jl") +include("core/region.jl") include("utils/utils.jl") +include("utils/circuit_analysis.jl") -include("algorithms/knn.jl") -include("algorithms/contraction.jl") -include("algorithms/propagate.jl") - +include("branching/propagate.jl") include("branching/measure.jl") -include("branching/selector.jl") -include("branching/branchtable.jl") -include("branching/greedymerge.jl") + +include("branch_table/knn.jl") +include("branch_table/selector.jl") +include("branch_table/contraction.jl") +include("branch_table/branchtable.jl") +include("branch_table/regioncache.jl") + +include("utils/visualization.jl") include("branching/branch.jl") include("interface.jl") -export Variable, EdgeRef, BoolTensor, TNStatic, DomainMask, TNProblem -export DM_BOTH, DM_0, DM_1 -export Region, RegionCacheEntry, RegionCacheState -export DynamicWorkspace -export is_fixed, has0, has1, init_doms, get_var_value +export Variable, EdgeRef, BoolTensor, BipartiteGraph, DomainMask, TNProblem, Result +export DM_BOTH, DM_0, DM_1, DM_NONE +export Region + +export is_fixed, has0, has1, init_doms, get_var_value, bits export setup_problem, setup_from_tensor_network, setup_from_cnf, setup_from_circuit, setup_from_sat +export factoring_problem, factoring_circuit, factoring_csp -export is_solved, cache_branch_solution!, reset_last_branch_problem!, has_last_branch_problem, last_branch_problem +export is_solved export solve, solve_sat_problem, solve_sat_with_assignments, solve_factoring -export solve_sat_problem_lookahead, solve_sat_problem_hybrid -export solve_sat_problem_region, solve_sat_problem_region_lookahead -export solve_sat_problem_cdcl +export solve_circuit_sat export NumUnfixedVars -export MostOccurrenceSelector, MinGammaSelector, AbstractSelector -export RegionAwareSelector, PropagationAwareSelector -export RegionQualityMetrics, evaluate_region_quality, score_region_quality -export evaluate_propagation_power, compute_propagation_score, evaluate_propagation_for_branch +export MostOccurrenceSelector, LeastOccurrenceSelector, MinGammaSelector, LocalTensorSelector, AbstractSelector -export TNContractionSolver, AbstractTableSolver +export TNContractionSolver, SingleTensorSolver, AbstractTableSolver, NewTNContractionSolver +export partition_tensor_variables export contract_region, contract_tensors, slicing, tensor_unwrapping export propagate, get_active_tensors, build_tensor_masks -export TensorMasks, PropagationBuffers -export look_ahead_propagation, look_ahead_score, LookAheadResult - -export propagate_incremental, propagate_from_assignment, propagate_from_assignments -export propagate_adaptive, should_use_incremental - -export propagate_cdcl, propagate_after_assignment_cdcl, propagate_with_state! -export CDCLState, LearnedClause, TrailEntry -export solve_cdcl, get_solution, print_cdcl_stats -export propagate_bcp!, analyze_conflict!, make_decision!, backtrack! +export TensorMasks export cache_region!, get_cached_region, clear_all_region_caches! -export k_neighboring, KNNWorkspace +export k_neighboring export get_unfixed_vars, count_unfixed, bits_to_int +export circuit_output_distances +export compute_circuit_info, map_tensor_to_circuit_info -export get_branching_stats, reset_branching_stats!, print_branching_stats +export get_branching_stats, reset_problem!, print_branching_stats -export BranchingStats, DetailedStats -export record_depth!, record_branch!, record_unsat_leaf!, record_solved_leaf!, record_skipped_subproblem! -export record_propagation!, record_propagation_fixpoint!, record_domain_reduction!, record_early_unsat! -export record_branching_time!, record_contraction_time!, record_filtering_time!, record_cache_hit!, record_cache_miss! -export record_variable_selection! +export BranchingStats export print_stats_summary -export reset! export extract_inner_configs, combine_configs, slice_region_contraction export handle_no_boundary_case_unfixed +export to_graph, visualize_problem, visualize_highest_degree_vars +export get_highest_degree_variables, get_tensors_containing_variables + +export branching_table!, branch_and_reduce!, bbsat! +export BranchingStrategy, AbstractReducer, NoReducer +export NumHardTensors, NumUnfixedVars, NumUnfixedTensors end diff --git a/src/algorithms/contraction.jl b/src/algorithms/contraction.jl deleted file mode 100644 index f455dbc..0000000 --- a/src/algorithms/contraction.jl +++ /dev/null @@ -1,124 +0,0 @@ -function contract_region(tn::TNStatic, region::Region, doms::Vector{DomainMask}) - # @show region.id - # println(union(region.boundary_vars, region.inner_vars)) - n_tensors = length(region.tensors) - - sliced_tensors = Vector{Vector{Tropical{Float64}}}(undef, n_tensors) - tensor_indices = Vector{Vector{Int}}(undef, n_tensors) - - @inbounds for (i, tensor_id) in enumerate(region.tensors) - # Get original tensor and its variable axes - original_tensor = tn.tensors[tensor_id] - var_axes = original_tensor.var_axes - tensor_data = original_tensor.tensor - - # Slice tensor according to fixed variables - sliced = slicing(tensor_data, doms, var_axes) - sliced_tensors[i] = sliced - - # Determine remaining (unfixed) variable indices - # After slicing, only unfixed variables remain as indices - remaining_vars = Int[] - for var_id in var_axes - if !is_fixed(doms[var_id]) - push!(remaining_vars, var_id) - end - end - tensor_indices[i] = remaining_vars - end - - # Output: only unfixed variables in the region - # (fixed variables have already been sliced out) - output_vars = Int[] - - # Collect unfixed variables - for var_id in region.boundary_vars - if !is_fixed(doms[var_id]) - push!(output_vars, var_id) - end - end - for var_id in region.inner_vars - if !is_fixed(doms[var_id]) - push!(output_vars, var_id) - end - end - - if isempty(output_vars) - # if all variables are fixed, output is scalar - contracted = contract_tensors(sliced_tensors, tensor_indices, Int[]) - @assert length(contracted) == 1 - return contracted, Int[] - else - contracted = contract_tensors(sliced_tensors, tensor_indices, output_vars) - return contracted, output_vars - end -end - -function contract_tensors(tensors::Vector{Vector{T}}, ixs::Vector{Vector{Int}}, iy::Vector{Int}) where T - eincode = EinCode(ixs, iy) - optcode = optimize_code(eincode, uniformsize(eincode, 2), GreedyMethod()) - unwrapped_tensors = [tensor_unwrapping(t) for t in tensors] - result = optcode(unwrapped_tensors...) - return result -end - - -@inline function slicing(tensor::Vector{T}, doms::Vector{DomainMask}, axis_vars::Vector{Int}) where T - # Number of axes (Boolean => size 2 per axis) - k = trailing_zeros(length(tensor)) # log2 - - # Pre-allocate with size hints - fixed_axes = Int[] - fixed_vals = Int[] - free_axes = Int[] - sizehint!(fixed_axes, k) - sizehint!(fixed_vals, k) - sizehint!(free_axes, k) - - @inbounds for axis in 1:k # each variable - var_id = axis_vars[axis] - dom_mask = doms[var_id] - if is_fixed(dom_mask) - push!(fixed_axes, axis) - push!(fixed_vals, ifelse(has1(dom_mask), 1, 0)) - else - push!(free_axes, axis) - end - end - - n_free = length(free_axes) - out_len = 1 << n_free # 2^n_free - out = Vector{T}(undef, out_len) - - # Precompute fixed part of the index - fixed_idx = 0 - @inbounds for (axis, val) in zip(fixed_axes, fixed_vals) - fixed_idx |= (val << (axis-1)) - end - - # Iterate over all assignments to free variables - @inbounds for free_idx in 0:(out_len-1) - # Build full index starting from fixed part - full_idx = fixed_idx - - # Set free variable bits - for (i, axis) in enumerate(free_axes) - bit = (free_idx >> (i-1)) & 0x1 # get the i-th bit of free_idx - full_idx |= (bit << (axis-1)) # set free-idx in the full_idx - end - - out[free_idx+1] = tensor[full_idx+1] - end - - return out -end - - -function tensor_unwrapping(vec::Vector{T}) where T - len = length(vec) - @assert len > 0 - k = trailing_zeros(len) - @assert (1 << k) == len "vector length is not power-of-two" - dims = ntuple(_->2, k) - return reshape(vec, dims) -end \ No newline at end of file diff --git a/src/algorithms/knn.jl b/src/algorithms/knn.jl deleted file mode 100644 index d81e0b5..0000000 --- a/src/algorithms/knn.jl +++ /dev/null @@ -1,124 +0,0 @@ -# Local workspace for k-neighboring algorithm -mutable struct KNNWorkspace - epoch::Int - visited_vars::Vector{Int} - visited_tensors::Vector{Int} - frontier::Vector{Int} - next_frontier::Vector{Int} - collected_vars::Vector{Int} - collected_tensors::Vector{Int} -end - -function KNNWorkspace(var_num::Int, tensor_num::Int) - return KNNWorkspace( - 1, - zeros(Int, var_num), - zeros(Int, tensor_num), - Int[], - Int[], - Int[], - Int[] - ) -end - -@inline function _mark_var!(ws::KNNWorkspace, var::Int) - ws.visited_vars[var] = ws.epoch -end -@inline function _mark_tensor!(ws::KNNWorkspace, tensor::Int) - ws.visited_tensors[tensor] = ws.epoch -end -@inline function _check_seen_var(ws::KNNWorkspace, var::Int) - return ws.visited_vars[var] == ws.epoch -end -@inline function _check_seen_tensor(ws::KNNWorkspace, tensor::Int) - return ws.visited_tensors[tensor] == ws.epoch -end - -@inline function _bump_epoch!(ws::KNNWorkspace) - ws.epoch += 1 -end - -function expand_one_var!( - tn::TNStatic, - ws::KNNWorkspace, - doms::Vector{DomainMask}, - max_tensors::Int -)::Bool # returns `true` if STOPPED EARLY due to limits; `false` otherwise - empty!(ws.next_frontier) - @inbounds for var in ws.frontier - for tensor_id in tn.v2t[var] - if !_check_seen_tensor(ws, tensor_id) - _mark_tensor!(ws, tensor_id) - push!(ws.collected_tensors, tensor_id) - if length(ws.collected_tensors) >= max_tensors - return true - end - end - for e in tn.t2v[tensor_id] - var_id = e.var - # Only expand to unfixed variables - if !_check_seen_var(ws, var_id) - _mark_var!(ws, var_id) - push!(ws.collected_vars, var_id) - push!(ws.next_frontier, var_id) - end - end - end - end - return false -end - -function classify_inner_boundary!(tn::TNStatic, ws::KNNWorkspace, vars::Vector{Int}) - inner = Int[] - boundary = Int[] - @inbounds for vid in vars - deg_total = tn.vars[vid].deg - deg_in = 0 - for tensor_id in tn.v2t[vid] - _check_seen_tensor(ws, tensor_id) && (deg_in += 1) - end - if deg_in == deg_total - push!(inner, vid) - else - push!(boundary, vid) - end - end - return inner, boundary -end - - -function k_neighboring( - tn::TNStatic, - doms::Vector{DomainMask}, - focus_var::Int; - max_tensors::Int, - k::Int = 2, -) - @debug "k_neighboring: focus_var = $focus_var" - @assert k ≥ 0 - @assert !is_fixed(doms[focus_var]) "Focus variable must be unfixed" - - # Create local workspace for this call - ws = KNNWorkspace(length(tn.vars), length(tn.tensors)) - - # Initialize with focus variable - _mark_var!(ws, focus_var) - push!(ws.frontier, focus_var) - push!(ws.collected_vars, focus_var) - - # k var-hops (only expanding to unfixed variables) - stopped = false - @inbounds for _ in 1:k - stopped = expand_one_var!(tn, ws, doms, max_tensors) - ws.frontier, ws.next_frontier = ws.next_frontier, ws.frontier - empty!(ws.next_frontier) - (stopped || isempty(ws.frontier)) && break - end - - # classify inner/boundary using current epoch marks for tensor-membership - inner, boundary = classify_inner_boundary!(tn, ws, ws.collected_vars) - - # deterministic ordering - sort!(inner); sort!(boundary); sort!(ws.collected_tensors) - return Region(focus_var, ws.collected_tensors, inner, boundary) -end \ No newline at end of file diff --git a/src/algorithms/propagate.jl b/src/algorithms/propagate.jl deleted file mode 100644 index 4935eb1..0000000 --- a/src/algorithms/propagate.jl +++ /dev/null @@ -1,270 +0,0 @@ -# function get_active_tensors(static::TNStatic, doms::Vector{DomainMask}) -# active = Int[] -# sizehint!(active, length(static.tensors)) -# @inbounds for (tid, tensor) in enumerate(static.tensors) -# # Check if any variable in this tensor is unfixed -# has_unfixed = false -# for var_id in tensor.var_axes -# dm_bits = doms[var_id].bits -# # Unfixed if domain allows both 0 and 1, or is not yet determined -# has_unfixed |= dm_bits == 0x03 -# end -# has_unfixed && push!(active, tid) -# end -# return active -# end - -# Backward compatible interface: propagate all tensors when changed_vars not specified -function propagate(static::TNStatic, doms::Vector{DomainMask}, ws::Union{Nothing, DynamicWorkspace}=nothing) - # When no changed_vars specified, propagate all tensors - all_vars = collect(1:length(doms)) - return propagate(static, doms, all_vars, ws) -end - -function propagate(static::TNStatic, doms::Vector{DomainMask}, changed_vars::Vector{Int}, ws::Union{Nothing, DynamicWorkspace}=nothing) - isempty(changed_vars) && return doms - working_doms = copy(doms) - - stats = !isnothing(ws) ? ws.branch_stats : nothing - has_detailed = !isnothing(stats) && !isnothing(stats.detailed) - - # Record propagation time (nanosecond precision) - propagation_start_time = has_detailed ? time_ns() : 0 - - # Build the propagation queue with tensors affected by the changed variables - tensor_queue = Int[] - in_queue = falses(length(static.tensors)) - @inbounds for var_id in changed_vars - @inbounds for tid in static.v2t[var_id] - if !in_queue[tid] - push!(tensor_queue, tid) - in_queue[tid] = true - end - end - end - - # Reuse propagation buffers to avoid reallocating BitVectors - buffers = if !isnothing(ws) && !isnothing(ws.prop_buffers) - ws.prop_buffers - else - buf = PropagationBuffers(static) - !isnothing(ws) && (ws.prop_buffers = buf) - buf - end - - # Count initial domain assignments - initial_domain_count = has_detailed ? sum(count_ones(d.bits & 0x03) for d in doms) : 0 - - queue_pos = 1 - iteration_count = 0 - while queue_pos <= length(tensor_queue) - iteration_count += 1 - tensor_idx = tensor_queue[queue_pos] - queue_pos += 1 - in_queue[tensor_idx] = false - - tensor = static.tensors[tensor_idx] - # Use the precomputed masks directly without cache lookups - masks = static.tensor_to_masks[tensor_idx] - - # Check constraint and propagate - if !propagate_tensor!(working_doms, tensor, masks, static.v2t, - tensor_queue, in_queue, buffers) - # Contradiction detected - if has_detailed - record_early_unsat!(stats) - end - return fill(DomainMask(0x00), length(working_doms)) - end - end - - # Check whether we reached a fixed point (iteration count) - if has_detailed && iteration_count == 1 && queue_pos > length(tensor_queue) - record_propagation_fixpoint!(stats) - end - - # Record domain reduction counts and elapsed time - if has_detailed - propagation_time = (time_ns() - propagation_start_time) / 1e9 # Convert to seconds - record_propagation!(stats, propagation_time) - - final_domain_count = sum(count_ones(d.bits & 0x03) for d in working_doms) - domain_reduction = initial_domain_count - final_domain_count - if domain_reduction > 0 - record_domain_reduction!(stats, domain_reduction) - end - end - - return working_doms -end - -# Propagate constraints from a single tensor. Returns false if contradiction detected. -function propagate_tensor!(working_doms::Vector{DomainMask}, tensor::BoolTensor, masks::TensorMasks, v2t::Vector{Vector{Int}}, tensor_queue::Vector{Int}, in_queue::BitVector, buffers::PropagationBuffers) - # Step 1: Compute feasible configurations given current domains - compute_feasible_configs!(buffers.feasible, working_doms, tensor, masks) || return false - n_feasible = count(buffers.feasible) - - # Step 2: Different propagation strategies based on number of feasible configs - if n_feasible == 1 - # Only one valid config -> fix all variables to that config - return propagate_unit_constraint!(working_doms, tensor, buffers.feasible, v2t, tensor_queue, in_queue) - else - # Multiple configs -> prune unsupported values - return propagate_support_pruning!(working_doms, tensor, masks, buffers.feasible, buffers.temp, v2t, tensor_queue, in_queue) - end -end - -# Compute which tensor configurations are feasible given current variable domains. -# Returns false if no feasible configuration exists. -@inline function compute_feasible_configs!(feasible::BitVector, working_doms::Vector{DomainMask}, tensor::BoolTensor, masks::TensorMasks) - n_cfg = length(masks.sat) - - copyto!(feasible, 1, masks.sat, 1, n_cfg) - - n_words = (n_cfg + 63) >> 6 - feas_chunks = feasible.chunks - - # Clear stale bits beyond n_cfg in the final UInt64 to avoid reuse artefacts - bits_in_last_word = n_cfg & 63 # n_cfg % 64 - if bits_in_last_word != 0 - # Keep only the lowest bits_in_last_word bits in the last word - mask_val = (UInt64(1) << bits_in_last_word) - 1 - feas_chunks[n_words] &= mask_val - end - - @inbounds for (axis, var_id) in enumerate(tensor.var_axes) - dm_bits = working_doms[var_id].bits - - # Skip unconstrained variables (both 0 and 1 are allowed) - dm_bits == 0x03 && continue - # Contradiction: variable has no feasible assignment - dm_bits == 0x00 && return false - - # Pick the corresponding mask (0 or 1) - mask_chunks = dm_bits == 0x01 ? masks.axis_masks0[axis].chunks : masks.axis_masks1[axis].chunks - - # Apply the mask and ensure a feasible configuration remains - # Optimization: merge computation and checking to avoid extra memory traffic - has_nonzero = false - for i in 1:n_words - feas_chunks[i] &= mask_chunks[i] - has_nonzero |= (feas_chunks[i] != 0) - end - - # No feasible configuration left, exit early - has_nonzero || return false - end - - return true -end - -# When tensor has exactly one feasible configuration, fix all its variables to that config. -@inline function propagate_unit_constraint!(working_doms::Vector{DomainMask}, tensor::BoolTensor, feasible::BitVector, v2t::Vector{Vector{Int}}, tensor_queue::Vector{Int}, in_queue::BitVector) - first_idx = findfirst(feasible) - config = first_idx - 1 - - @inbounds for (axis, var_id) in enumerate(tensor.var_axes) - bit_val = (config >> (axis - 1)) & 1 - # Branchless: avoid conditional for better performance - required_bits = ifelse(bit_val == 1, DM_1.bits, DM_0.bits) - - old_bits = working_doms[var_id].bits - new_bits = old_bits & required_bits - - # Check for contradiction - new_bits == 0x00 && return false - - # Update domain and enqueue affected tensors - if new_bits != old_bits - working_doms[var_id] = DomainMask(new_bits) - enqueue_affected_tensors!(tensor_queue, in_queue, v2t, var_id) - end - end - return true -end - -# Prune domain values that have no support in any feasible configuration. -@inline function propagate_support_pruning!(working_doms::Vector{DomainMask}, tensor::BoolTensor, masks::TensorMasks, feasible::BitVector, temp::BitVector, v2t::Vector{Vector{Int}}, tensor_queue::Vector{Int}, in_queue::BitVector) - n_cfg = length(masks.sat) - n_words = (n_cfg + 63) >> 6 - feas_chunks = feasible.chunks - - @inbounds for (axis, var_id) in enumerate(tensor.var_axes) - dm = working_doms[var_id] - dm_bits = dm.bits - - if (dm_bits & 0x01) != 0 - has_support_0 = false - mask_chunks = masks.axis_masks0[axis].chunks - for i in 1:n_words - if (feas_chunks[i] & mask_chunks[i]) != 0 - has_support_0 = true - break - end - end - if !has_support_0 - if !update_domain!(working_doms, var_id, dm_bits, DM_1.bits, - v2t, tensor_queue, in_queue) - return false - end - end - end - - if (dm_bits & 0x02) != 0 - has_support_1 = false - mask_chunks = masks.axis_masks1[axis].chunks - for i in 1:n_words - if (feas_chunks[i] & mask_chunks[i]) != 0 - has_support_1 = true - break - end - end - if !has_support_1 - if !update_domain!(working_doms, var_id, dm_bits, DM_0.bits, v2t, tensor_queue, in_queue) - return false - end - end - end - end - - return true -end - -# Add all tensors containing the variable to the propagation queue. -@inline function enqueue_affected_tensors!( - tensor_queue::Vector{Int}, - in_queue::BitVector, - v2t::Vector{Vector{Int}}, - var_id::Int -) - @inbounds for tensor_id in v2t[var_id] - if !in_queue[tensor_id] - push!(tensor_queue, tensor_id) - in_queue[tensor_id] = true - end - end -end - -# Update variable domain by intersecting with keep_mask. Returns false if contradiction. -@inline function update_domain!( - working_doms::Vector{DomainMask}, - var_id::Int, - old_bits::UInt8, - keep_bits::UInt8, - v2t::Vector{Vector{Int}}, - tensor_queue::Vector{Int}, - in_queue::BitVector -) - new_bits = old_bits & keep_bits - - # Check for contradiction - new_bits == 0x00 && return false - - # Update if changed - if new_bits != old_bits - working_doms[var_id] = DomainMask(new_bits) - enqueue_affected_tensors!(tensor_queue, in_queue, v2t, var_id) - end - - return true -end diff --git a/src/branch_table/branchtable.jl b/src/branch_table/branchtable.jl new file mode 100644 index 0000000..1c90077 --- /dev/null +++ b/src/branch_table/branchtable.jl @@ -0,0 +1,49 @@ +struct TNContractionSolver <: AbstractTableSolver end + +function branching_table!(problem::TNProblem, ::TNContractionSolver, region::Region; cache::Bool=true) + contracted_tensor, output_var_ids = contract_region(problem.static, region, problem.doms) + # Scan the contracted tensor: every entry equal to one(Tropical) + configs = map(packint, findall(isone, contracted_tensor)) + # propagate the configurations to get the feasible solutions + feasible_configs = collect_feasible!(problem, region, configs; cache) + table = BranchingTable(length(output_var_ids), [[c] for c in feasible_configs]) + return table, output_var_ids +end + +packint(bits::NTuple{N, Int}) where {N} = reduce(|, (UInt64(b) << (i - 1) for (i, b) in enumerate(bits)); init = UInt64(0)) +packint(i::Int) = packint((i - 1,)) +packint(ci::CartesianIndex{N}) where {N} = packint(ntuple(j -> ci.I[j] - 1, N)) + +# Apply a clause to domain masks, fixing variables according to the clause's mask and values +function apply_config!(config::UInt64, variables::Vector{Int}, original_doms::Vector{DomainMask}) + changed_indices = Int[] + @inbounds for (bit_idx, var_id) in enumerate(variables) + original_doms[var_id] = (config >> (bit_idx - 1)) & 1 == 1 ? DM_1 : DM_0 + push!(changed_indices, var_id) + end + return changed_indices +end + +function is_feasible_solution(problem::TNProblem, region::Region, config::UInt64) + doms = copy(problem.doms) + @assert !has_contradiction(doms) "Domain has contradiction before applying config $config" + changed_indices = apply_config!(config, region.vars, doms) + propagated_doms, _ = propagate(problem.static, doms, changed_indices) + has_contradiction(propagated_doms) && return false, propagated_doms + return true, propagated_doms +end + +function collect_feasible!(problem::TNProblem, region::Region, configs::Vector{UInt64}; cache::Bool) + feasible_configs = UInt64[] + isempty(configs) && return feasible_configs + bit_length = UInt64(ndigits(UInt64(configs[end]), base=2)) + @inbounds for config in configs + feasible, propagated_doms = is_feasible_solution(problem, region, config) + feasible || continue + + push!(feasible_configs, config) + cache && (problem.propagated_cache[Clause(bit_length, config)] = propagated_doms) + end + return feasible_configs +end + diff --git a/src/branch_table/contraction.jl b/src/branch_table/contraction.jl new file mode 100644 index 0000000..a9c9c42 --- /dev/null +++ b/src/branch_table/contraction.jl @@ -0,0 +1,57 @@ +function contract_region(tn::BipartiteGraph, region::Region, doms::Vector{DomainMask}) + sliced_tensors = Vector{Vector{Tropical{Float64}}}(undef, length(region.tensors)) + tensor_indices = Vector{Vector{Int}}(undef, length(region.tensors)) + + @inbounds for (i, tensor_id) in enumerate(region.tensors) + tensor = tn.tensors[tensor_id] + sliced_tensors[i] = slicing(tensor.tensor, doms, tensor.var_axes) + tensor_indices[i] = filter(v -> !is_fixed(doms[v]), tensor.var_axes) + end + + # Collect unfixed variables from the region + output_vars = filter(v -> !is_fixed(doms[v]), region.vars) + contracted = contract_tensors(sliced_tensors, tensor_indices, output_vars) + + isempty(output_vars) && @assert length(contracted) == 1 + return contracted, output_vars +end + +function contract_tensors(tensors::Vector{Vector{T}}, ixs::Vector{Vector{Int}}, iy::Vector{Int}) where T + eincode = EinCode(ixs, iy) + optcode = optimize_code(eincode, uniformsize(eincode, 2), GreedyMethod()) + return optcode([tensor_unwrapping(t) for t in tensors]...) +end + +function slicing(tensor::Vector{T}, doms::Vector{DomainMask}, axis_vars::Vector{Int}) where T + k = trailing_zeros(length(tensor)) # log2(length) + + fixed_idx = 0; free_axes = Int[] + + @inbounds for axis in 1:k # each variable + if is_fixed(doms[axis_vars[axis]]) + has1(doms[axis_vars[axis]]) && (fixed_idx |= (1 << (axis-1))) + else + push!(free_axes, axis) + end + end + + out = Vector{T}(undef, 1 << length(free_axes)) + + @inbounds for free_idx in eachindex(out) + full_idx = fixed_idx + for (i, axis) in enumerate(free_axes) + ((free_idx-1) >> (i-1)) & 0x1 == 1 && (full_idx |= (1 << (axis-1))) + end + out[free_idx] = tensor[full_idx+1] + end + + return out +end + + +function tensor_unwrapping(vec::Vector{T}) where T + k = trailing_zeros(length(vec)) + @assert (1 << k) == length(vec) "vector length is not power-of-two" + dims = ntuple(_->2, k) + return reshape(vec, dims) +end \ No newline at end of file diff --git a/src/branch_table/knn.jl b/src/branch_table/knn.jl new file mode 100644 index 0000000..bc307ec --- /dev/null +++ b/src/branch_table/knn.jl @@ -0,0 +1,66 @@ +function _k_neighboring(tn::BipartiteGraph, doms::Vector{DomainMask}, focus_var::Int; max_tensors::Int, k::Int = 2, hard_only::Bool = false) + @assert !is_fixed(doms[focus_var]) "Focus variable must be unfixed" + + visited_vars = Set{Int}() + visited_tensors = Set{Int}() + collected_vars = Int[focus_var] + collected_tensors = Int[] + + push!(visited_vars, focus_var) + + # Use BFS with two separate queues for variables and tensors + var_queue = [focus_var] + + for hop in 1:k + # Step 1: From current variables to tensors + tensor_queue = Int[] + for var_id in var_queue + for tensor_id in tn.v2t[var_id] + if tensor_id ∉ visited_tensors + if hard_only && !is_hard(tn, doms)[tensor_id] + continue + end + push!(visited_tensors, tensor_id) + push!(collected_tensors, tensor_id) + push!(tensor_queue, tensor_id) + if length(collected_tensors) >= max_tensors + break + end + end + end + if length(collected_tensors) >= max_tensors + break + end + end + + # Step 2: From current tensors to next layer variables + # Always collect variables from the tensors we got, even if max_tensors is reached + var_queue = Int[] + for tensor_id in tensor_queue + for next_var in tn.tensors[tensor_id].var_axes + if next_var ∉ visited_vars && !is_fixed(doms[next_var]) + push!(visited_vars, next_var) + push!(collected_vars, next_var) + push!(var_queue, next_var) + end + end + end + + # Stop after collecting variables if max_tensors is reached + if length(collected_tensors) >= max_tensors + break + end + end + + sort!(collected_vars) + sort!(collected_tensors) + return Region(focus_var, collected_tensors, collected_vars) +end + +function k_neighboring(tn::BipartiteGraph, doms::Vector{DomainMask}, focus_var::Int; max_tensors::Int, k::Int = 2) + return _k_neighboring(tn, doms, focus_var; max_tensors = max_tensors, k = k, hard_only = false) +end + +function k_neighboring_hard(tn::BipartiteGraph, doms::Vector{DomainMask}, focus_var::Int; max_tensors::Int, k::Int = 2) + return _k_neighboring(tn, doms, focus_var; max_tensors = max_tensors, k = k, hard_only = true) +end \ No newline at end of file diff --git a/src/branch_table/regioncache.jl b/src/branch_table/regioncache.jl new file mode 100644 index 0000000..2cb600b --- /dev/null +++ b/src/branch_table/regioncache.jl @@ -0,0 +1,129 @@ +struct RegionCache + var_to_region::Vector{Region} # Fixed at initialization: var_to_region[var_id] gives the region for variable var_id + var_to_configs::Vector{Vector{UInt64}} # Cached full configs from initial contraction for each variable's region +end + +function init_cache(problem::TNProblem{INT}, table_solver::AbstractTableSolver, measure::AbstractMeasure, set_cover_solver::AbstractSetCoverSolver, selector::AbstractSelector) where {INT} + num_vars = length(problem.static.vars) + unfixed_vars = get_unfixed_vars(problem) + + var_to_region = Vector{Region}(undef, num_vars) + var_to_configs = Vector{Vector{UInt64}}(undef, num_vars) + fill!(var_to_configs, Vector{UInt64}()) + + # For each unfixed variable, create region and cache full contraction configs + @inbounds for var_id in unfixed_vars + region = create_region(problem, var_id, selector) + var_to_region[var_id] = region + + # Compute full branching table with initial doms (all variables unfixed) + contracted_tensor, _ = contract_region(problem.static, region, problem.doms) + configs = map(packint, findall(isone, contracted_tensor)) + var_to_configs[var_id] = configs + end + + return RegionCache(var_to_region, var_to_configs) +end + +# Filter cached configs based on current doms and compute branching result for a specific variable +function compute_branching_result(cache::RegionCache, problem::TNProblem{INT}, var_id::Int, measure::AbstractMeasure, set_cover_solver::AbstractSetCoverSolver) where {INT} + region = cache.var_to_region[var_id] + cached_configs = cache.var_to_configs[var_id] + + # Filter configs that are compatible with current doms + feasible_configs = filter_feasible_configs(problem, region, cached_configs) + isempty(feasible_configs) && return nothing + + # Build branching table from filtered configs + table = BranchingTable(length(region.vars), [[c] for c in feasible_configs]) + + # Compute optimal branching rule + result = OptimalBranchingCore.optimal_branching_rule(table, region.vars, problem, measure, set_cover_solver) + return result +end + +# Filter configs to only those compatible with current variable domains +function filter_feasible_configs(problem::TNProblem, region::Region, configs::Vector{UInt64}) + feasible = UInt64[] + @inbounds for config in configs + if is_config_compatible(config, region.vars, problem.doms) + doms = copy(problem.doms) + changed_indices = Int[] + for (bit_idx, var_id) in enumerate(region.vars) + doms[var_id] = (config >> (bit_idx - 1)) & 1 == 1 ? DM_1 : DM_0 + push!(changed_indices, var_id) + end + touched_tensors = unique(vcat([problem.static.v2t[v] for v in changed_indices]...)) + propagated_doms, propagated_vars = propagate(problem.static, doms, touched_tensors) + !has_contradiction(propagated_doms) && push!(feasible, config) + end + end + return feasible +end + +# Check if a config is compatible with current domains +function is_config_compatible(config::UInt64, variables::Vector{Int}, doms::Vector{DomainMask}) + @inbounds for (bit_idx, var_id) in enumerate(variables) + is_fixed(doms[var_id]) || continue + + # Extract the bit value for this variable from config + config_value = (config >> (bit_idx - 1)) & 1 + required_value = has1(doms[var_id]) ? 1 : 0 + + # If config assigns a different value than what's fixed, it's incompatible + config_value != required_value && return false + end + return true +end + +# Apply clause assignments to domains +function apply_clause(clause::Clause, variables::Vector{Int}, original_doms::Vector{DomainMask}) + doms = copy(original_doms) + changed_vars = Int[] + + @inbounds for (var_idx, var_id) in enumerate(variables) + if ismasked(clause, var_idx) + new_domain = getbit(clause, var_idx) ? DM_1 : DM_0 + if doms[var_id] != new_domain + doms[var_id] = new_domain + push!(changed_vars, var_id) + end + end + end + return doms, changed_vars +end + +# Find the best variable to branch on +function findbest(cache::RegionCache, problem::TNProblem{INT}, measure::AbstractMeasure, set_cover_solver::AbstractSetCoverSolver) where {INT} + best_subproblem = nothing + best_gamma = Inf + + # Check all unfixed variables + unfixed_vars = get_unfixed_vars(problem) + @inbounds for var_id in unfixed_vars + reset_propagated_cache!(problem) + result = compute_branching_result(cache, problem, var_id, measure, set_cover_solver) + isnothing(result) && continue + # @info "var_id: $var_id, γ: $(result.γ)" + + if result.γ < best_gamma + best_gamma = result.γ + clauses = OptimalBranchingCore.get_clauses(result) + @show keys(problem.propagated_cache) + @show clauses + + @assert haskey(problem.propagated_cache, clauses[1]) + best_subproblem = [problem.propagated_cache[clauses[i]] for i in 1:length(clauses)] + + best_gamma == 1.0 && break + end + end + println("best_γ: $best_gamma") + best_gamma === Inf && return [] + + # If any subproblem is already fully fixed, return it directly + fixed_indices = findall(iszero, count_unfixed.(best_subproblem)) + !isempty(fixed_indices) && return [best_subproblem[fixed_indices[1]]] + + return best_subproblem +end diff --git a/src/branch_table/selector.jl b/src/branch_table/selector.jl new file mode 100644 index 0000000..75a8255 --- /dev/null +++ b/src/branch_table/selector.jl @@ -0,0 +1,45 @@ +function create_region(problem::TNProblem, variable::Int, selector::AbstractSelector) + return k_neighboring(problem.static, problem.doms, variable; max_tensors = selector.max_tensors, k = selector.k) +end + +struct MostOccurrenceSelector <: AbstractSelector + k::Int + max_tensors::Int +end + +function select_region(problem::TNProblem, ::AbstractMeasure, selector::MostOccurrenceSelector) + unfixed_vars = get_unfixed_vars(problem) + most_show_var_idx = argmax(length(problem.static.v2t[u]) for u in unfixed_vars) + return create_region(problem, unfixed_vars[most_show_var_idx], selector) +end + +struct MinGammaSelector <: AbstractSelector + k::Int + max_tensors::Int + table_solver::AbstractTableSolver + set_cover_solver::AbstractSetCoverSolver +end + +# Constructor will be defined after TNContractionSolver is available +function select_region(problem::TNProblem, measure::AbstractMeasure, selector::MinGammaSelector) + unfixed_vars = get_unfixed_vars(problem) + best_region = nothing + best_gamma = Inf + + @inbounds for var in unfixed_vars + region = create_region(problem, var, selector) + # TODO: improve the performance + tbl, variables = branching_table!(problem, selector.table_solver, region; cache=false) + isempty(tbl.table) && continue + + # Compute optimal branching rule for this variable + result = OptimalBranchingCore.optimal_branching_rule(tbl, variables, problem, measure, selector.set_cover_solver) + + # Update best variable if this gamma is smaller + if result.γ < best_gamma + best_gamma = result.γ + best_region = copy(region) + end + end + return best_region +end \ No newline at end of file diff --git a/src/branching/branch.jl b/src/branching/branch.jl index 83df429..0e7201d 100644 --- a/src/branching/branch.jl +++ b/src/branching/branch.jl @@ -1,349 +1,50 @@ -function OptimalBranchingCore.branch_and_reduce( - problem::TNProblem, - config::OptimalBranchingCore.BranchingStrategy, - reducer::OptimalBranchingCore.AbstractReducer, - result_type::Type{TR}; - show_progress::Bool=false, - tag::Vector{Tuple{Int,Int}}=Tuple{Int,Int}[] -) where TR - try - stats = problem.ws.branch_stats - current_depth = length(tag) +function apply_branch!(problem::TNProblem, clause::OptimalBranchingCore.Clause, variables::Vector{Int}) + doms, changed_vars = apply_clause(clause, variables, problem.doms) + isempty(changed_vars) && return problem.doms - # Step 1: Check if problem is solved (all variables fixed) - if is_solved(problem) - record_solved_leaf!(stats, current_depth, problem.ws.current_path) - @debug "problem is solved at depth $current_depth" - cache_branch_solution!(problem) - return one(result_type) - end + touched_tensors = unique(vcat([problem.static.v2t[v] for v in changed_vars]...)) + propagated_doms, _ = propagate(problem.static, doms, touched_tensors) - record_depth!(stats, current_depth) - @debug "======= Decision Level: $(current_depth + 1) =======" - # println("======= Decision Level: $(current_depth + 1) =======") - # Step 2: Try to reduce the problem - @assert reducer isa NoReducer - - # record branching time (only if detailed stats are enabled) - has_detailed = !isnothing(stats.detailed) - branching_start_time = has_detailed ? time_ns() : 0 - - # Step 3: Select variables for branching - variable = OptimalBranchingCore.select_variables(problem, config.measure, config.selector) - - # Record variable selection statistics and push to current path (only if tracking) - record_variable_selection!(stats, variable, problem.n_unfixed, current_depth) - needs_path_tracking(stats) && push!(problem.ws.current_path, variable) - @debug "Variable $variable selected at depth $current_depth" - - # Step 4: Compute branching table - tbl, variables = OptimalBranchingCore.branching_table(problem, config.table_solver, variable) - - # Check if table is empty (UNSAT - no valid configurations) - if isempty(tbl.table) - @debug "Empty branching table - UNSAT" - has_detailed && record_branching_time!(stats, (time_ns() - branching_start_time) / 1e9) - record_unsat_leaf!(stats, current_depth) - # Pop current variable before returning (restore path for parent) - needs_path_tracking(stats) && !isempty(problem.ws.current_path) && pop!(problem.ws.current_path) - return zero(result_type) - end - - # Step 5: Compute optimal branching rule - result = OptimalBranchingCore.optimal_branching_rule(tbl, variables, problem, config.measure, config.set_cover_solver) - - # record branching time (only if detailed stats are enabled) - has_detailed && record_branching_time!(stats, (time_ns() - branching_start_time) / 1e9) - - # @show tbl - # Step 6: Branch and recurse - clauses = OptimalBranchingCore.get_clauses(result) - @debug "A new branch-level search starts with $(length(clauses)) clauses: $(clauses)" - # @show clauses - # Record branching statistics - record_branch!(stats, length(clauses), current_depth) - # @show clauses - - # Use explicit loop instead of sum() to avoid closure allocation overhead - accum = zero(result_type) - - @inbounds for (i, branch) in enumerate(clauses) - show_progress && (OptimalBranchingCore.print_sequence(stdout, tag); println(stdout)) - @debug "branch=$branch, n_unfixed=$(problem.n_unfixed)" - - # Apply branch to get subproblem - subproblem, local_value, changed_vars = OptimalBranchingCore.apply_branch(problem, branch, variables) - - @debug "local_value=$local_value, n_unfixed=$(subproblem.n_unfixed)" - - # If branch led to contradiction (UNSAT), skip this branch - if local_value == 0 || subproblem.n_unfixed == 0 && any(dm -> dm.bits == 0x00, subproblem.doms) - @debug "Skipping branch: local_value=$local_value, n_unfixed=$(subproblem.n_unfixed), has_contradiction=$(any(dm -> dm.bits == 0x00, subproblem.doms))" - record_skipped_subproblem!(stats) - record_unsat_leaf!(stats, current_depth + 1) - continue # Skip to next branch instead of creating zero value - end - - # Recursively solve subproblem - # Use mutable tag buffer: push before recursion, pop after - # This avoids allocating new arrays on each recursive call - push!(tag, (i, length(clauses))) - # Save path length before recursion to restore after (only if tracking) - path_length_before = needs_path_tracking(stats) ? length(problem.ws.current_path) : 0 - sub_result = OptimalBranchingCore.branch_and_reduce(subproblem, config, reducer, result_type; tag=tag, show_progress=show_progress) - # Restore path to length before recursion (pop variables added during recursion) - if needs_path_tracking(stats) - while length(problem.ws.current_path) > path_length_before - pop!(problem.ws.current_path) - end - end - pop!(tag) - - # Combine results - accum = accum + sub_result * result_type(local_value) - - # Early exit: if we found a solution (accum > 0), return immediately - # This ensures we only find one solution path - if accum > zero(result_type) - @debug "Found solution, early exit at depth $current_depth" - needs_path_tracking(stats) && !isempty(problem.ws.current_path) && pop!(problem.ws.current_path) - return accum - end - end - - # Pop current variable before returning (restore path for parent) - needs_path_tracking(stats) && !isempty(problem.ws.current_path) && pop!(problem.ws.current_path) - return accum - finally - clear_branch_cache!(problem.ws, Base.objectid(problem.doms)) - end -end - -@inline function lookup_branch_cache(problem::TNProblem, - clause::OptimalBranchingCore.Clause{INT}, - variables::Vector{Int} -) where {INT} - ws = problem.ws - doms_id = Base.objectid(problem.doms) - inner = get(ws.branch_cache, doms_id, nothing) - inner === nothing && return nothing - key = (Base.objectid(variables), clause_key(clause)) - return get(inner, key, nothing) -end - -@inline function store_branch_cache!( - problem::TNProblem, - clause::OptimalBranchingCore.Clause{INT}, - variables::Vector{Int}, - doms::Vector{DomainMask}, - n_unfixed::Int, - local_value::Int -) where {INT} - ws = problem.ws - doms_id = Base.objectid(problem.doms) - inner = get!(ws.branch_cache, doms_id) do - Dict{Tuple{UInt, Any}, Any}() - end - key = (Base.objectid(variables), clause_key(clause)) - inner[key] = (doms=doms, n_unfixed=n_unfixed, local_value=local_value) - return nothing -end - -function OptimalBranchingCore.optimal_branching_rule(tbl::OptimalBranchingCore.BranchingTable, variables::Vector{T}, problem::TNProblem, measure::OptimalBranchingCore.AbstractMeasure, solver::OptimalBranchingCore.GreedyMerge) where T - candidates = OptimalBranchingCore.bit_clauses(tbl) - return OptimalBranchingCore.greedymerge(candidates, problem, variables, measure) -end - -function OptimalBranchingCore.optimal_branching_rule( - tbl::OptimalBranchingCore.BranchingTable{INT}, - variables::Vector{T}, - problem::TNProblem, - measure::OptimalBranchingCore.AbstractMeasure, - solver::OptimalBranchingCore.AbstractSetCoverSolver -) where {INT<:Integer, T} - candidates = OptimalBranchingCore.candidate_clauses(tbl) - valid_clauses = Vector{OptimalBranchingCore.Clause{INT}}() - reductions = Float64[] - - for clause in candidates - reduction = Float64(OptimalBranchingCore.size_reduction(problem, measure, clause, variables)) - if isfinite(reduction) && reduction > 0 - push!(valid_clauses, clause) - push!(reductions, reduction) - end - end - - if isempty(valid_clauses) - empty_clauses = Vector{OptimalBranchingCore.Clause{INT}}() - return OptimalBranchingCore.OptimalBranchingResult( - OptimalBranchingCore.DNF(empty_clauses), - Float64[], - Inf, - ) - end - - covered_mask = BitVector(undef, length(tbl.table)) - @inbounds for (idx, group) in pairs(tbl.table) - covered_mask[idx] = any(valid_clauses) do clause - any(config -> OptimalBranchingCore.covered_by(config, clause), group) - end - end - - if !all(covered_mask) - if !any(covered_mask) - empty_clauses = Vector{OptimalBranchingCore.Clause{INT}}() - return OptimalBranchingCore.OptimalBranchingResult( - OptimalBranchingCore.DNF(empty_clauses), - Float64[], - Inf, - ) - end - filtered_groups = tbl.table[findall(covered_mask)] - tbl = OptimalBranchingCore.BranchingTable{INT}(tbl.bit_length, filtered_groups) - end - - return OptimalBranchingCore.minimize_γ(tbl, valid_clauses, reductions, solver) -end - -function OptimalBranchingCore.optimal_branching_rule( - tbl::OptimalBranchingCore.BranchingTable{INT}, - variables::Vector{T}, - problem::TNProblem, - measure::OptimalBranchingCore.AbstractMeasure, - solver::OptimalBranchingCore.NaiveBranch -) where {INT<:Integer, T} - return invoke( - OptimalBranchingCore.optimal_branching_rule, - Tuple{ - OptimalBranchingCore.BranchingTable, - Vector, - OptimalBranchingCore.AbstractProblem, - OptimalBranchingCore.AbstractMeasure, - OptimalBranchingCore.NaiveBranch, - }, - tbl, - variables, - problem, - measure, - solver, - ) + @assert !has_contradiction(propagated_doms) "Contradiction found when applying clause $clause" + problem.propagated_cache[clause] = propagated_doms + return propagated_doms end -# Apply a clause to domain masks, fixing variables according to the clause's mask and values. Returns the number of variables that were fixed. -function apply_clause_to_doms!(new_doms::Vector{DomainMask}, clause::OptimalBranchingCore.Clause{INT}, variables::Vector{Int}, original_doms::Vector{DomainMask}, changed_flags::BitVector, changed_indices::Vector{Int}) where {INT<:Integer} - n_fixed = 0 - - @inbounds for i in 1:length(variables) - mask_bit = OptimalBranchingCore.readbit(clause.mask, i) - if mask_bit == 1 - # This variable is fixed by the clause - var_id = variables[i] - bit_val = OptimalBranchingCore.readbit(clause.val, i) - new_val = ifelse(bit_val == 1, DM_1, DM_0) - - old_bits = original_doms[var_id].bits - # Branchless: check if not fixed (bits == 0x03) - if old_bits == 0x03 - new_doms[var_id] = new_val - n_fixed += 1 - changed_flags[var_id] = true - push!(changed_indices, var_id) - end - end - end - - return n_fixed -end - -function OptimalBranchingCore.apply_branch( - problem::TNProblem, - clause::OptimalBranchingCore.Clause{INT}, - variables::Vector{Int} -) where {INT<:Integer} - if (cached = lookup_branch_cache(problem, clause, variables)) !== nothing - subproblem = TNProblem(problem.static, cached.doms, cached.n_unfixed, problem.ws) - return (subproblem, cached.local_value, Int[]) - end - - new_doms = copy(problem.doms) - - changed_flags = problem.ws.changed_vars_flags # BitVector: tracking variable changes - changed_indices = problem.ws.changed_vars_indices - empty!(changed_indices) - - # Apply clause: fix variables according to mask and values - n_fixed = apply_clause_to_doms!(new_doms, clause, variables, problem.doms, changed_flags, changed_indices) - - # @debug "apply_branch: Clause $(clause) Fixed $n_fixed variables" - - propagated_doms = propagate(problem.static, new_doms, changed_indices, problem.ws) - - @inbounds for i in eachindex(propagated_doms) - if propagated_doms[i].bits != problem.doms[i].bits && !changed_flags[i] - changed_flags[i] = true - push!(changed_indices, i) - end - end - - if has_contradiction(propagated_doms) - # UNSAT: contradiction detected during propagation - @debug "apply_branch: Clause $(clause) Contradiction detected during propagation" - doms_zero = fill(DomainMask(0x00), length(propagated_doms)) - store_branch_cache!(problem, clause, variables, doms_zero, problem.n_unfixed, 0) - return (TNProblem(problem.static, doms_zero, problem.n_unfixed, problem.ws), 0, Int[]) - end - - # Count unfixed variables - new_n_unfixed = count_unfixed(propagated_doms) - - @debug "apply_branch: Clause $(clause) n_unfixed: $(problem.n_unfixed) -> $new_n_unfixed" - - # Safety check: problem must have gotten smaller OR we fixed at least one variable - if new_n_unfixed == problem.n_unfixed && n_fixed == 0 - @debug "apply_branch: No progress made (n_unfixed same and n_fixed=0)" - doms_zero = fill(DomainMask(0x00), length(propagated_doms)) - store_branch_cache!(problem, clause, variables, doms_zero, 0, 0) - return (TNProblem(problem.static, doms_zero, 0, problem.ws), 0, Int[]) - end +function OptimalBranchingCore.size_reduction(p::TNProblem{INT}, m::AbstractMeasure, cl::Clause{INT}, variables::Vector{Int}) where {INT} - new_problem = TNProblem(problem.static, propagated_doms, new_n_unfixed, problem.ws) - - @inbounds for idx in changed_indices - changed_flags[idx] = false - end - - store_branch_cache!(problem, clause, variables, propagated_doms, new_n_unfixed, 1) - return (new_problem, 1, Int[]) # local_value = 1 (no scoring for now) + newdoms = haskey(p.propagated_cache, cl) ? p.propagated_cache[cl] : apply_branch!(p, cl, variables) + r = measure(p, m) - measure(TNProblem(p.static, newdoms, INT), m) + return r end -function OptimalBranchingCore.reduce_problem(::Type{T}, problem::TNProblem, ::OptimalBranchingCore.NoReducer) where T - return (problem, one(T)) +# Main branch-and-reduce algorithm +function bbsat!(problem::TNProblem, config::OptimalBranchingCore.BranchingStrategy, reducer::OptimalBranchingCore.AbstractReducer) + cache = init_cache(problem, config.table_solver, config.measure, config.set_cover_solver, config.selector) + return _bbsat!(problem, config, reducer, cache) end -# function reduce_problem(::Type{T}, problem::TNProblem, reducer::UnitPropagationReducer) where T -# propagated = propagate(problem.static, problem.doms) +# const tmp_measure = Int[] +# const tmp_count_unfixed = Int[] +# const tmp_count_unfixed_tensors = Int[] -# doms = problem.doms -# changed = false -# n_unfixed::Int = 0 +# reset_temp!() = (empty!(tmp_measure); empty!(tmp_count_unfixed); empty!(tmp_count_unfixed_tensors)) -# @inbounds for i in eachindex(doms) -# dm_new = propagated[i] -# bits = dm_new.bits +function _bbsat!(problem::TNProblem, config::OptimalBranchingCore.BranchingStrategy, reducer::OptimalBranchingCore.AbstractReducer, region_cache::RegionCache) + stats = problem.stats + println("================================================") + is_solved(problem) && return Result(true, problem.doms, copy(stats)) -# if bits == 0x00 -# clear_region_cache!(problem) -# return (TNProblem(problem.static, propagated, 0, problem.ws), zero(T)) -# end + subproblems = findbest(region_cache, problem, config.measure, config.set_cover_solver) + isempty(subproblems) && return Result(false, DomainMask[], copy(stats)) + record_branch!(stats, length(subproblems)) + @inbounds for (i, subproblem_doms) in enumerate(subproblems) + subproblem = TNProblem(problem.static, subproblem_doms, problem.stats, Dict{Clause{UInt64}, Vector{DomainMask}}()) + # push!(tmp_measure, measure(subproblem, NumHardTensors())) + # push!(tmp_count_unfixed_tensors, measure(subproblem, NumUnfixedTensors())) + # push!(tmp_count_unfixed, count_unfixed(subproblem.doms)) -# changed |= bits != doms[i].bits -# n_unfixed += is_fixed(dm_new) ? 0 : 1 -# end - -# if !changed -# return (problem, one(T)) -# end - -# clear_region_cache!(problem) -# return (TNProblem(problem.static, propagated, n_unfixed, problem.ws), one(T)) -# end + result = _bbsat!(subproblem, config, reducer, region_cache) + result.found && return result + end + return Result(false, DomainMask[], copy(stats)) +end \ No newline at end of file diff --git a/src/branching/branchtable.jl b/src/branching/branchtable.jl deleted file mode 100644 index eb6b04a..0000000 --- a/src/branching/branchtable.jl +++ /dev/null @@ -1,246 +0,0 @@ -struct TNContractionSolver <: AbstractTableSolver - k::Int - max_tensors::Int -end -TNContractionSolver() = TNContractionSolver(1, 2) - -@inline function bit_extract(config::UInt64, positions::Vector{Int})::UInt64 - out::UInt64 = 0 - @inbounds for (newpos, oldpos) in enumerate(positions) - out |= ((config >> (oldpos-1)) & 0x1) << (newpos-1) - end - return out -end - -@inline bit_match(config::UInt64, mask::UInt64, pattern::UInt64) = (config & mask) == pattern - -function _build_axismap(output_vars::Vector{Int}) - isempty(output_vars) && return Int[] - max_var = maximum(output_vars) - axismap = zeros(Int, max_var) - @inbounds for (idx, var_id) in enumerate(output_vars) - axismap[var_id] = idx - end - return axismap -end - -function extract_inner_configs(contracted::AbstractArray{T, N}, n_inner::Int) where {T, N} - @assert n_inner == N - configs = Vector{UInt64}() - one_tropical = one(Tropical{Float64}) - - @inbounds for lin in eachindex(contracted) - if contracted[lin] == one_tropical - linear_idx = LinearIndices(contracted)[lin] - 1 - config_bits = UInt64(linear_idx) - push!(configs, config_bits) - end - end - return configs -end - -function combine_configs(boundary_bits::UInt64, inner_configs::Vector{UInt64}, n_boundary::Int) - n_configs = length(inner_configs) - full_configs = Vector{UInt64}(undef, n_configs) - - @inbounds for i in 1:n_configs - full_configs[i] = boundary_bits | (inner_configs[i] << n_boundary) - end - - return full_configs -end - -function slice_region_contraction( - tensor::AbstractArray{Tropical{Float64}}, - assignments::Vector{Tuple{Int,Bool}}, - axismap::Vector{Int}, -) - isempty(assignments) && return tensor - nd = ndims(tensor) - nd == 0 && return tensor - - indices = Any[Colon() for _ in 1:nd] - - @inbounds for (var_id, value) in assignments - axis = axismap[var_id] - @assert axis > 0 "Boundary variable $var_id not found in contraction axes" - indices[axis] = value ? 2 : 1 - end - - return @view tensor[indices...] -end - -function handle_no_boundary_case_unfixed( - region::Region, - contracted::AbstractArray{Tropical{Float64}}, - inner_output_vars::Vector{Int}, -) - n_inner = length(region.inner_vars) - free_inner_configs = extract_inner_configs(contracted, length(inner_output_vars)) - - if !isempty(free_inner_configs) - return BranchingTable(n_inner, [free_inner_configs]) - else - return BranchingTable(0, [UInt64[]]) - end -end - -function create_region(problem::TNProblem, variable::Int, solver::TNContractionSolver) - # Compute k-neighboring region using all-unfixed domains - # This ensures the region is consistent across different branches - all_unfixed_doms = fill(DM_BOTH, length(problem.doms)) - k_neighboring(problem.static, all_unfixed_doms, variable; max_tensors = solver.max_tensors, k = solver.k) -end - -# Filter cached BranchingTable: filter rows by fixed values, extract columns for unfixed vars -function filter_branching_table(region::Region, table::BranchingTable, problem::TNProblem) - stats = problem.ws.branch_stats - has_detailed = !isnothing(stats) && !isnothing(stats.detailed) - filtering_start_time = has_detailed ? time_ns() : 0 - - var_ids = vcat(region.boundary_vars, region.inner_vars) - n_vars = length(var_ids) - - fixed_positions = Tuple{Int, Bool}[] - unfixed_positions = Int[] - - @inbounds for (i, var_id) in enumerate(var_ids) - if is_fixed(problem.doms[var_id]) - required_value = has1(problem.doms[var_id]) - push!(fixed_positions, (i, required_value)) - else - push!(unfixed_positions, i) - end - end - - if isempty(fixed_positions) - if has_detailed - filtering_time = (time_ns() - filtering_start_time) / 1e9 - record_filtering_time!(stats, filtering_time) - end - return table, var_ids - end - - n_unfixed = length(unfixed_positions) - - mask::UInt64 = 0x0 - pattern::UInt64 = 0x0 - @inbounds for (pos, val) in fixed_positions - pos_mask = UInt64(1) << (pos - 1) - mask |= pos_mask - if val - pattern |= pos_mask - end - end - - filtered_table = similar(table.table, 0) - sizehint!(filtered_table, length(table.table)) - - @inbounds for config_group in table.table - filtered_group = similar(config_group, 0) - sizehint!(filtered_group, length(config_group)) - - for config_bits in config_group - if bit_match(UInt64(config_bits), mask, pattern) - new_config = bit_extract(UInt64(config_bits), unfixed_positions) - push!(filtered_group, typeof(config_bits)(new_config)) - end - end - - if !isempty(filtered_group) - push!(filtered_table, filtered_group) - end - end - - if has_detailed - filtering_time = (time_ns() - filtering_start_time) / 1e9 - record_filtering_time!(stats, filtering_time) - end - - isempty(filtered_table) && return BranchingTable(0, eltype(table.table)[]), Int[] - - unfixed_var_ids = [var_ids[i] for i in unfixed_positions] - - return BranchingTable(n_unfixed, filtered_table), unfixed_var_ids -end - -function OptimalBranchingCore.branching_table(problem::TNProblem, solver::TNContractionSolver, variable::Int) - stats = problem.ws.branch_stats - - cached_region, cached_table = get_cached_region(variable) - if !isnothing(cached_region) && !isnothing(cached_table) - record_cache_hit!(stats) - filtered_table, unfixed_vars = filter_branching_table(cached_region, cached_table, problem) - return filtered_table, unfixed_vars - end - - record_cache_miss!(stats) - region = create_region(problem, variable, solver) - n_boundary = length(region.boundary_vars) - n_inner = length(region.inner_vars) - n_total = n_boundary + n_inner - - # Contract with all-unfixed doms for consistent caching - all_unfixed_doms = fill(DM_BOTH, length(problem.doms)) - - stats = problem.ws.branch_stats - contraction_start_time = time_ns() - contracted_tensor, output_vars = contract_region(problem.static, region, all_unfixed_doms) - contraction_time = (time_ns() - contraction_start_time) / 1e9 - record_contraction_time!(stats, contraction_time) - axismap = _build_axismap(output_vars) - - inner_output_vars = Int[] - @inbounds for var_id in output_vars - if var_id in region.inner_vars - push!(inner_output_vars, var_id) - end - end - - if n_boundary == 0 - table = handle_no_boundary_case_unfixed(region, contracted_tensor, inner_output_vars) - variables = vcat(region.boundary_vars, region.inner_vars) - cache_region!(region, table) - filtered_table, unfixed_vars = filter_branching_table(region, table, problem) - return filtered_table, unfixed_vars - end - - free_boundary_vars = region.boundary_vars - n_free_boundary = length(free_boundary_vars) - - valid_config_groups = Vector{Vector{UInt64}}() - assignments = Tuple{Int,Bool}[] - resize!(assignments, n_free_boundary) - - for free_config in 0:(2^n_free_boundary - 1) - for (j, var_id) in enumerate(free_boundary_vars) - bit = (free_config >> (j-1)) & 0x1 - assignments[j] = (var_id, bit == 1) - end - - contracted_slice = slice_region_contraction(contracted_tensor, assignments, axismap) - free_inner_configs = extract_inner_configs(contracted_slice, length(inner_output_vars)) - - isempty(free_inner_configs) && continue - - boundary_bits = UInt64(free_config) - full_configs = combine_configs(boundary_bits, free_inner_configs, n_boundary) - - push!(valid_config_groups, full_configs) - end - - if isempty(valid_config_groups) - table = BranchingTable(0, [UInt64[]]) - cache_region!(region, table) - return table, Int[] - end - - table = BranchingTable(n_total, valid_config_groups) - cache_region!(region, table) - - filtered_table, unfixed_vars = filter_branching_table(region, table, problem) - return filtered_table, unfixed_vars -end - -# Constructor for MinGammaSelector (defined here after TNContractionSolver is available) -MinGammaSelector() = MinGammaSelector(TNContractionSolver(2,5), OptimalBranchingCore.GreedyMerge()) diff --git a/src/branching/greedymerge.jl b/src/branching/greedymerge.jl deleted file mode 100644 index 793510d..0000000 --- a/src/branching/greedymerge.jl +++ /dev/null @@ -1,222 +0,0 @@ -# Calculate size reduction after applying a clause to the problem -function OptimalBranchingCore.size_reduction(p::TNProblem, m::OptimalBranchingCore.AbstractMeasure, cl::OptimalBranchingCore.Clause{INT}, variables::Vector{Int}) where {INT<:Integer} - subproblem, _, _ = OptimalBranchingCore.apply_branch(p, cl, variables) - if any(dm -> dm.bits == 0x00, subproblem.doms) - return -Inf - end - reduction = OptimalBranchingCore.measure(p, m) - OptimalBranchingCore.measure(subproblem, m) - return reduction -end - -# Generate a key for a clause based on its fields -@inline clause_key(cl::Clause{INT}) where {INT} = (getfield(cl, 1), getfield(cl, 2)) - -# Get size reduction from cache or compute and cache it -function cached_size_reduction!( - cache::Dict{Tuple{INT,INT},Float64}, - problem::OptimalBranchingCore.AbstractProblem, - m::OptimalBranchingCore.AbstractMeasure, - variables::Vector{Int}, - clause::Clause{INT} -) where {INT} - key = clause_key(clause) - return get!(cache, key) do - Float64(OptimalBranchingCore.size_reduction(problem, m, clause, variables)) - end -end - -# Select the best representative clause from each row based on size reduction -function select_representatives!( - cls::Vector{Vector{Clause{INT}}}, - cache::Dict{Tuple{INT,INT},Float64}, - problem::OptimalBranchingCore.AbstractProblem, - variables::Vector{Int}, - m::OptimalBranchingCore.AbstractMeasure -) where {INT} - size_reductions = Vector{Float64}(undef, length(cls)) - @inbounds for (idx, row) in pairs(cls) - best_val = -Inf - best_pos = 0 - @inbounds for k in eachindex(row) - reduction = cached_size_reduction!(cache, problem, m, variables, row[k]) - if reduction > best_val && reduction > 0 && isfinite(reduction) - best_val = reduction - best_pos = k - end - end - size_reductions[idx] = best_val - if best_pos > 1 - row[1], row[best_pos] = row[best_pos], row[1] - end - end - return size_reductions -end - -# Remove rows with invalid (non-finite or non-positive) size reductions -function drop_invalid_rows!(cls::Vector{Vector{Clause{INT}}}, size_reductions::Vector{Float64}) where {INT} - keep = isfinite.(size_reductions) .& (size_reductions .> 0) - all(keep) && return cls, size_reductions - return cls[keep], size_reductions[keep] -end - -# Remove duplicate singleton clauses from the clause set -function deduplicate_singletons!(cls::Vector{Vector{Clause{INT}}}, size_reductions::Vector{Float64}) where {INT} - seen = Dict{Tuple{INT,INT},Int}() - mask = trues(length(cls)) - @inbounds for i in 1:length(cls) - if length(cls[i]) == 1 - key = clause_key(cls[i][1]) - if haskey(seen, key) - mask[i] = false - else - seen[key] = i - end - end - end - if all(mask) - return cls, size_reductions - end - return cls[mask], size_reductions[mask] -end - -# Find the best clause to merge from two clause vectors -function best_merge_clause( - cache::Dict{Tuple{INT,INT},Float64}, - problem::OptimalBranchingCore.AbstractProblem, - m::OptimalBranchingCore.AbstractMeasure, - variables::Vector{Int}, - left::Vector{Clause{INT}}, - right::Vector{Clause{INT}} -) where {INT} - best_clause = nothing - best_reduction = -Inf - nvars = length(variables) - @inbounds for cl_left in left - @inbounds for cl_right in right - merged = OptimalBranchingCore.gather2(nvars, cl_left, cl_right) - iszero(merged.mask) && continue - reduction = cached_size_reduction!(cache, problem, m, variables, merged) - if reduction > best_reduction && reduction > 0 && isfinite(reduction) - best_clause = merged - best_reduction = reduction - end - end - end - return best_clause, best_reduction -end - -# Enqueue a merge pair if it's beneficial (finite positive reduction with negative energy change) -@inline function maybe_enqueue!(queue::PriorityQueue{NTuple{2,Int},Float64}, idx_a::Int, idx_b::Int, reduction::Float64, weights::Vector{Float64}, γ::Float64) - if !isfinite(reduction) || reduction <= 0 - return - end - dE = γ^(-reduction) - weights[idx_a] - weights[idx_b] - dE <= -1e-12 && enqueue!(queue, (idx_a, idx_b), dE) -end - -# Enqueue all beneficial merge pairs from the clause set -function enqueue_beneficial_merges!( - queue::PriorityQueue{NTuple{2,Int},Float64}, - cls::Vector{Vector{Clause{INT}}}, - γ::Float64, - weights::Vector{Float64}, - cache::Dict{Tuple{INT,INT},Float64}, - problem::OptimalBranchingCore.AbstractProblem, - variables::Vector{Int}, - m::OptimalBranchingCore.AbstractMeasure -) where {INT} - nc = length(cls) - @inbounds for i in 1:nc-1 - row_i = cls[i] - for j in i+1:nc - clause, reduction = best_merge_clause(cache, problem, m, variables, row_i, cls[j]) - clause === nothing && continue - maybe_enqueue!(queue, i, j, reduction, weights, γ) - end - end -end - -# Remove queue entries related to a specific row -function purge_queue_entries!(queue::PriorityQueue{NTuple{2,Int},Float64}, mask::BitVector, rowid::Int, nc::Int) - mask[rowid] = false - @inbounds for l in 1:nc - if mask[l] - a, b = minmax(rowid, l) - haskey(queue, (a, b)) && delete!(queue, (a, b)) - end - end -end - -# Process the merge queue and perform beneficial merges -function process_merge_queue!( - queue::PriorityQueue{NTuple{2,Int},Float64}, - cls::Vector{Vector{Clause{INT}}}, size_reductions::Vector{Float64}, - weights::Vector{Float64}, mask::BitVector, γ::Float64, - cache::Dict{Tuple{INT,INT},Float64}, - problem::OptimalBranchingCore.AbstractProblem, - variables::Vector{Int}, - m::OptimalBranchingCore.AbstractMeasure -) where {INT} - nc = length(cls) - any_merge = false - while !isempty(queue) - (i, j) = dequeue!(queue) - if !mask[i] || !mask[j] - continue - end - clause, new_reduction = best_merge_clause(cache, problem, m, variables, cls[i], cls[j]) - clause === nothing && continue - - purge_queue_entries!(queue, mask, i, nc) - purge_queue_entries!(queue, mask, j, nc) - - mask[i] = true - cls[i] = [clause] - size_reductions[i] = new_reduction - weights[i] = γ^(-new_reduction) - any_merge = true - - @inbounds for l in 1:nc - if i !== l && mask[l] - a, b = minmax(i, l) - _, reduction = best_merge_clause(cache, problem, m, variables, cls[a], cls[b]) - maybe_enqueue!(queue, a, b, reduction, weights, γ) - end - end - end - return any_merge -end - -# Greedy merge algorithm to find optimal branching clauses -function OptimalBranchingCore.greedymerge(cls::Vector{Vector{Clause{INT}}}, problem::TNProblem, variables::Vector{T}, m::OptimalBranchingCore.AbstractMeasure) where {INT<:Integer, T} - cache = Dict{Tuple{INT,INT},Float64}() - working = copy(cls) - size_reductions = select_representatives!(working, cache, problem, variables, m) - working, size_reductions = drop_invalid_rows!(working, size_reductions) - if isempty(working) - @debug "greedymerge: no valid clauses remain after filtering; returning empty result" - return OptimalBranchingResult(DNF(Clause{INT}[]), Float64[], Inf) - end - - while true - working, size_reductions = deduplicate_singletons!(working, size_reductions) - nc = length(working) - mask = trues(nc) - γ = OptimalBranchingCore.complexity_bv(size_reductions) - weights = map(s -> γ^(-s), size_reductions) - queue = PriorityQueue{NTuple{2, Int}, Float64}() - - enqueue_beneficial_merges!(queue, working, γ, weights, cache, problem, variables, m) - if isempty(queue) - return OptimalBranchingResult(DNF(first.(working)), size_reductions, γ) - end - - any_merge = process_merge_queue!(queue, working, size_reductions, weights, mask, γ, cache, problem, variables, m) - if !any_merge - return OptimalBranchingResult(DNF(first.(working)), size_reductions, γ) - end - - working = working[mask] - size_reductions = size_reductions[mask] - end -end diff --git a/src/branching/measure.jl b/src/branching/measure.jl index fb4cd52..635b5ee 100644 --- a/src/branching/measure.jl +++ b/src/branching/measure.jl @@ -1,16 +1,28 @@ struct NumUnfixedVars <: AbstractMeasure end function OptimalBranchingCore.measure(problem::TNProblem, ::NumUnfixedVars) - # problem.n_unfixed == 0 && println("n_unfixed is 0") return Int(problem.n_unfixed) end -# struct NumUnfixedTensors <: AbstractMeasure end -# function OptimalBranchingCore.measure(problem::TNProblem, ::NumUnfixedTensors) -# problem.doms -# end - -# struct NumUnfixedTensors <: AbstractMeasure end -# function OptimalBranchingCore.measure(problem::TNProblem, ::NumUnfixedTensors) -# length(problem.ws.active_tensors) -# end +struct NumUnfixedTensors <: AbstractMeasure end +function OptimalBranchingCore.measure(problem::TNProblem, ::NumUnfixedTensors) + return length(get_active_tensors(problem.static, problem.doms)) +end +struct NumHardTensors <: AbstractMeasure end +function OptimalBranchingCore.measure(problem::TNProblem, ::NumHardTensors) + active_tensors = get_active_tensors(problem.static, problem.doms) + hard_tensor_num = 0 + for tensor_id in active_tensors + vars = problem.static.tensors[tensor_id].var_axes + degree = 0 + for var in vars + if !is_fixed(problem.doms[var]) + degree += 1 + end + end + if degree > 2 + hard_tensor_num += 1 + end + end + return hard_tensor_num +end \ No newline at end of file diff --git a/src/branching/propagate.jl b/src/branching/propagate.jl new file mode 100644 index 0000000..55715dd --- /dev/null +++ b/src/branching/propagate.jl @@ -0,0 +1,63 @@ +# Main propagate function: returns (new_doms, propagated_vars) +function propagate(static::BipartiteGraph, doms::Vector{DomainMask}, touched_tensors::Vector{Int}) + isempty(touched_tensors) && return doms, Int[] + working_doms = copy(doms); propagated_vars = Int[] + + queue_index = 1 + while queue_index <= length(touched_tensors) + tensor_id = touched_tensors[queue_index] + queue_index += 1 + + tensor = static.tensors[tensor_id] + feasible_configs = find_feasible_configs(working_doms, tensor) + isempty(feasible_configs) && return fill(DM_NONE, length(working_doms)), propagated_vars + + updated_vars = update_domains_from_configs!(working_doms, tensor, feasible_configs) + append!(propagated_vars, updated_vars) + + new_tensors = unique(vcat([static.v2t[v] for v in updated_vars]...)) + append!(touched_tensors, filter(t -> t ∉ touched_tensors[queue_index:end], new_tensors)) + end + return working_doms, propagated_vars +end + +# Find all configurations of the tensor that are feasible given current variable domains +function find_feasible_configs(doms::Vector{DomainMask}, tensor::BoolTensor) + num_configs = 1 << length(tensor.var_axes) + + is_config_feasible(config) = begin + # Check if this configuration satisfies the tensor constraint + tensor.tensor[config + 1] != Tropical(0.0) && return false + + # Check if configuration is compatible with current variable domains + all(enumerate(tensor.var_axes)) do (axis, var_id) + bit_value = (config >> (axis - 1)) & 1 + domain = doms[var_id] + (bit_value == 0 && domain ∉ (DM_1, DM_NONE)) || (bit_value == 1 && domain ∉ (DM_0, DM_NONE)) + end + end + + return filter(is_config_feasible, 0:(num_configs-1)) +end + +# Update variable domains based on feasible configurations +function update_domains_from_configs!(doms::Vector{DomainMask}, tensor::BoolTensor, feasible_configs::Vector{Int}) + updated_vars = Int[] + + for (axis, var_id) in enumerate(tensor.var_axes) + current_domain = doms[var_id] + (current_domain == DM_0 || current_domain == DM_1) && continue + + bit_values = [(config >> (axis - 1)) & 1 for config in feasible_configs] + has_zero, has_one = (0 ∈ bit_values), (1 ∈ bit_values) + + new_domain = has_zero && has_one ? DM_BOTH : has_zero ? DM_0 : has_one ? DM_1 : DM_NONE + + if new_domain != current_domain + doms[var_id] = new_domain + push!(updated_vars, var_id) + end + end + + return updated_vars +end diff --git a/src/branching/selector.jl b/src/branching/selector.jl deleted file mode 100644 index 84378b2..0000000 --- a/src/branching/selector.jl +++ /dev/null @@ -1,87 +0,0 @@ -struct MostOccurrenceSelector <: AbstractSelector end - -function OptimalBranchingCore.select_variables( - problem::TNProblem, - measure::AbstractMeasure, - selector::MostOccurrenceSelector -) - unfixed_vars = get_unfixed_vars(problem.doms) - isempty(unfixed_vars) && return Int[] - least_show_var_idx = argmax(length(problem.static.v2t[u]) for u in unfixed_vars) - - return unfixed_vars[least_show_var_idx] -end - -""" - MinGammaSelector <: AbstractSelector - -Selector that chooses the variable with minimum branching gamma. -For each unfixed variable, it computes the branching gamma on the corresponding -region and selects the variable with the smallest gamma value. - -This selector does not consider performance optimization and will iterate through -all unfixed variables to find the best one. -""" -struct MinGammaSelector <: AbstractSelector - table_solver::AbstractTableSolver - set_cover_solver::OptimalBranchingCore.AbstractSetCoverSolver -end - -# Constructor will be defined after TNContractionSolver is available - -function OptimalBranchingCore.select_variables( - problem::TNProblem, - measure::AbstractMeasure, - selector::MinGammaSelector -) - unfixed_vars = get_unfixed_vars(problem.doms) - isempty(unfixed_vars) && return Int[] - - best_var = unfixed_vars[1] - best_gamma = Inf - - @debug "Selecting variables with MinGammaSelector, n_unfixed=$(length(unfixed_vars))" - # println("Selecting variables with MinGammaSelector, n_unfixed=$(length(unfixed_vars))") - # Iterate through all unfixed variables - for var in unfixed_vars - # Compute branching table for this variable - tbl, variables = OptimalBranchingCore.branching_table( - problem, - selector.table_solver, - var - ) - # @show tbl - # Skip if table is empty (UNSAT) - if isempty(tbl.table) - continue - end - - # Compute optimal branching rule for this variable - result = OptimalBranchingCore.optimal_branching_rule( - tbl, - variables, - problem, - measure, - selector.set_cover_solver - ) - - @debug "Optimal branching rule for variable $var: $(OptimalBranchingCore.get_clauses(result))" - # println("Optimal branching rule for variable $var: $(OptimalBranchingCore.get_clauses(result))") - - # Get the gamma value - gamma = result.γ - @debug "Gamma for variable $var: $gamma" - # println("Gamma for variable $var: $gamma") - - # Update best variable if this gamma is smaller - if gamma < best_gamma - @debug "Updating best variable to $var with gamma $gamma" - # println("Updating best variable to $var with gamma $gamma") - best_gamma = gamma - best_var = var - end - end - - return best_var -end - diff --git a/src/core/domain.jl b/src/core/domain.jl index 9903926..6fda683 100644 --- a/src/core/domain.jl +++ b/src/core/domain.jl @@ -1,21 +1,57 @@ -struct DomainMask - bits::UInt8 +@enum DomainMask::UInt8 begin + DM_NONE = 0x00 + DM_0 = 0x01 + DM_1 = 0x02 + DM_BOTH = 0x03 end -const DM_BOTH = DomainMask(0x03) -const DM_0 = DomainMask(0x01) -const DM_1 = DomainMask(0x02) +init_doms(static::BipartiteGraph) = fill(DM_BOTH, length(static.vars)) +# Get the underlying bits value +@inline bits(dm::DomainMask)::UInt8 = UInt8(dm) + +# Convert UInt8 to DomainMask (allows any UInt8 value, not just enum values) +Base.convert(::Type{DomainMask}, bits::UInt8) = reinterpret(DomainMask, bits) + +@inline is_fixed(dm::DomainMask) = (dm == DM_0) || (dm == DM_1) +@inline has0(dm::DomainMask)::Bool = (bits(dm) & 0x01) != 0 +@inline has1(dm::DomainMask)::Bool = (bits(dm) & 0x02) != 0 -@inline is_fixed(dm::DomainMask) = (dm.bits == 0x01) || (dm.bits == 0x02) -@inline has0(dm::DomainMask)::Bool = (dm.bits & 0x01) != 0 -@inline has1(dm::DomainMask)::Bool = (dm.bits & 0x02) != 0 function get_var_value(dms::Vector{DomainMask}, var_id::Int) dm = dms[var_id] - dm.bits == 0x01 && return 0 - dm.bits == 0x02 && return 1 - return -1 # not fixed + dm == DM_0 && return 0 + dm == DM_1 && return 1 + @assert false "Variable $var_id is not fixed" +end +function get_var_value(dms::Vector{DomainMask}, var_ids::Vector{Int}) + return Bool[get_var_value(dms, var_id) for var_id in var_ids] +end + +function active_degree(tn::BipartiteGraph, doms::Vector{DomainMask}) + degree = zeros(Int, length(tn.tensors)) + @inbounds for (tensor_id, tensor) in enumerate(tn.tensors) + vars = tensor.var_axes + degree[tensor_id] = sum(!is_fixed(doms[var_id]) for var_id in vars) + end + return degree end +is_hard(tn::BipartiteGraph, doms::Vector{DomainMask}) = active_degree(tn, doms) .> 2 + +@inline has_contradiction(doms::Vector{DomainMask}) = any(dm -> dm == DM_NONE, doms) -init_doms(static::TNStatic) = fill(DM_BOTH, length(static.vars)) +const DOMAIN_MASK_NAMES = ("NONE", "0", "1", "BOTH") + +function Base.show(io::IO, dm::DomainMask) + if 1 <= bits(dm) + 1 <= length(DOMAIN_MASK_NAMES) + @inbounds print(io, DOMAIN_MASK_NAMES[bits(dm) + 1]) + else + print(io, "UNDEF") + end +end -@inline has_contradiction(doms::Vector{DomainMask}) = any(dm -> dm.bits == 0x00, doms) \ No newline at end of file +function Base.show(io::IO, ::MIME"text/plain", dm::DomainMask) + if 1 <= bits(dm) + 1 <= length(DOMAIN_MASK_NAMES) + @inbounds print(io, DOMAIN_MASK_NAMES[bits(dm) + 1]) + else + print(io, "UNDEF") + end +end \ No newline at end of file diff --git a/src/core/problem.jl b/src/core/problem.jl index e5429a2..7022c5c 100644 --- a/src/core/problem.jl +++ b/src/core/problem.jl @@ -1,54 +1,58 @@ -struct TNProblem <: AbstractProblem - static::TNStatic - doms::Vector{DomainMask} - n_unfixed::Int - ws::DynamicWorkspace +# Result type for branch-and-reduce solving +struct Result + found::Bool + solution::Vector{DomainMask} + stats::BranchingStats end -function TNProblem(static::TNStatic; verbose::Bool = false)::TNProblem - doms = init_doms(static) - ws = DynamicWorkspace(length(static.vars), verbose) - doms = propagate(static, doms, collect(1:length(static.vars)), ws) - n_unfixed = count_unfixed(doms) - return TNProblem(static, doms, n_unfixed, ws) +function Base.show(io::IO, r::Result) + if r.found + print(io, "Result(found=true, solution=available)") + else + print(io, "Result(found=false)") + end end -function Base.show(io::IO, problem::TNProblem) - print(io, "TNProblem(unfixed=$(problem.n_unfixed)/$(length(problem.static.vars)))") +struct TNProblem{INT<:Integer} <: AbstractProblem + static::BipartiteGraph # TODO: simplify the graph type + doms::Vector{DomainMask} + n_unfixed::Int # Do not store the number of unfixed variables. + stats::BranchingStats + propagated_cache::Dict{Clause{INT}, Vector{DomainMask}} + + function TNProblem{INT}(static::BipartiteGraph, doms::Vector{DomainMask}, stats::BranchingStats=BranchingStats(), propagated_cache::Dict{Clause{INT}, Vector{DomainMask}}=Dict{Clause{INT}, Vector{DomainMask}}()) where {INT<:Integer} + n_unfixed = count_unfixed(doms) + new{INT}(static, doms, n_unfixed, stats, propagated_cache) + end end -get_var_value(problem::TNProblem, var_id::Int) = get_var_value(problem.doms, var_id) -get_var_value(problem::TNProblem, var_ids::Vector{Int}) = Bool[get_var_value(problem.doms, var_id) for var_id in var_ids] +function TNProblem(static::BipartiteGraph, ::Type{INT}=UInt64) where {INT<:Integer} + doms, _ = propagate(static, init_doms(static), collect(1:length(static.tensors))) + has_contradiction(doms) && error("Domain has contradiction") + return TNProblem{INT}(static, doms) +end -is_solved(problem::TNProblem) = problem.n_unfixed == 0 +### Reduce the number of interfaces +# Constructor with explicit domains +function TNProblem(static::BipartiteGraph, doms::Vector{DomainMask}, ::Type{INT}=UInt64) where {INT<:Integer} + return TNProblem{INT}(static, doms) +end -function cache_branch_solution!(problem::TNProblem) - ws = problem.ws - copyto!(ws.cached_doms, problem.doms) - ws.has_cached_solution = true - return nothing +# Constructor with all parameters (for internal use) +function TNProblem(static::BipartiteGraph, doms::Vector{DomainMask}, stats::BranchingStats, propagated_cache::Dict{Clause{INT}, Vector{DomainMask}}) where {INT<:Integer} + return TNProblem{INT}(static, doms, stats, propagated_cache) end -function reset_last_branch_problem!(problem::TNProblem) - problem.ws.has_cached_solution = false - return nothing +function Base.show(io::IO, problem::TNProblem) + print(io, "TNProblem(unfixed=$(problem.n_unfixed)/$(length(problem.static.vars)))") end -@inline has_last_branch_problem(problem::TNProblem) = problem.ws.has_cached_solution +get_var_value(problem::TNProblem, var_id::Int) = get_var_value(problem.doms, var_id) +get_var_value(problem::TNProblem, var_ids::Vector{Int}) = Bool[get_var_value(problem.doms, var_id) for var_id in var_ids] -function last_branch_problem(problem::TNProblem) - has_last_branch_problem(problem) || return nothing - doms = copy(problem.ws.cached_doms) - fixed = count(x -> is_fixed(x), doms) - @assert fixed == length(doms) - return TNProblem(problem.static, doms, 0, problem.ws) -end +is_solved(problem::TNProblem) = problem.n_unfixed == 0 -function get_branching_stats(problem::TNProblem) - return copy(problem.ws.branch_stats) -end +get_branching_stats(problem::TNProblem) = copy(problem.stats) -function reset_branching_stats!(problem::TNProblem) - reset!(problem.ws.branch_stats) - return nothing -end +reset_problem!(problem::TNProblem) = (reset!(problem.stats); empty!(problem.propagated_cache)) +reset_propagated_cache!(problem::TNProblem) = empty!(problem.propagated_cache) \ No newline at end of file diff --git a/src/core/region.jl b/src/core/region.jl index bc3e78f..cabb91a 100644 --- a/src/core/region.jl +++ b/src/core/region.jl @@ -1,41 +1,27 @@ struct Region id::Int tensors::Vector{Int} - inner_vars::Vector{Int} - boundary_vars::Vector{Int} + vars::Vector{Int} end function Base.show(io::IO, region::Region) - print(io, "Region(focus=$(region.id), tensors=$(length(region.tensors)), inner_vars=$(region.inner_vars), boundary_vars=$(region.boundary_vars))") + print(io, "Region(focus=$(region.id), tensors=$(region.tensors), vars=$(region.vars))") end -struct RegionCacheEntry - region::Region - table::BranchingTable +function Base.copy(region::Region) + return Region(region.id, region.tensors, region.vars) end -mutable struct RegionCacheState - entries::Dict{Int, RegionCacheEntry} -end - -RegionCacheState() = RegionCacheState(Dict{Int, RegionCacheEntry}()) - -# global region cache -const REGION_CACHE = RegionCacheState() - -function cache_region!(region::Region, table::BranchingTable) - REGION_CACHE.entries[region.id] = RegionCacheEntry(region, table) - return nothing -end - -function get_cached_region(region_id::Int) - entry = get(REGION_CACHE.entries, region_id, nothing) - (isnothing(entry) || isnothing(entry.table)) && return nothing, nothing - return entry.region, entry.table -end - -function clear_all_region_caches!() - empty!(REGION_CACHE.entries) - return nothing +function get_region_tensor_type(problem::TNProblem, region::Region) + symbols = Symbol[] + fanin = Vector{Int}[] + fanout = Vector{Int}[] + active_vars = get_unfixed_vars(problem, region.tensors) + for tensor_id in region.tensors + push!(symbols, problem.static.tensor_symbols[tensor_id]) + push!(fanin, problem.static.tensor_fanin[tensor_id]) + push!(fanout, problem.static.tensor_fanout[tensor_id]) + end + return symbols, fanin, fanout, active_vars end diff --git a/src/core/static.jl b/src/core/static.jl index db7c839..583e158 100644 --- a/src/core/static.jl +++ b/src/core/static.jl @@ -1,100 +1,67 @@ -struct TNStatic +struct BipartiteGraph vars::Vector{Variable} tensors::Vector{BoolTensor} v2t::Vector{Vector{Int}} - t2v::Vector{Vector{EdgeRef}} - axis_of_t::Dict{Tuple{Int,Int},Int} - # Precomputed tensor masks: maps tensor.tensor to TensorMasks - # Reuse masks for identical tensor shapes to avoid recomputation - precomputed_masks::Dict{Vector{Tropical{Float64}}, TensorMasks} - # Map each tensor instance to its precomputed masks (indexing optimization) - tensor_to_masks::Vector{TensorMasks} + tensor_depths::Vector{Int} + tensor_fanin::Vector{Vector{Int}} + tensor_fanout::Vector{Vector{Int}} + tensor_symbols::Vector{Symbol} # Circuit gate type for each tensor (:and, :or, :not, :var, etc.) end -function Base.show(io::IO, tn::TNStatic) - print(io, "TNStatic(vars=$(length(tn.vars)), tensors=$(length(tn.tensors)))") +function Base.show(io::IO, tn::BipartiteGraph) + print(io, "BipartiteGraph(vars=$(length(tn.vars)), tensors=$(length(tn.tensors)))") end -function Base.show(io::IO, ::MIME"text/plain", tn::TNStatic) - println(io, "TNStatic:") +function Base.show(io::IO, ::MIME"text/plain", tn::BipartiteGraph) + println(io, "BipartiteGraph:") println(io, " variables: $(length(tn.vars))") println(io, " tensors: $(length(tn.tensors))") println(io, " variable-tensor incidence: $(length(tn.v2t))") - println(io, " tensor-variable incidence: $(length(tn.t2v))") - println(io, " axis mappings: $(length(tn.axis_of_t))") end function setup_problem(var_num::Int, tensors_to_vars::Vector{Vector{Int}}, - tensor_data::Vector{Vector{Tropical{Float64}}}) + tensor_data::Vector{Vector{Tropical{Float64}}}; + tensor_depths::Vector{Int}=Int[], + tensor_fanin::Vector{Vector{Int}}=Vector{Int}[], + tensor_fanout::Vector{Vector{Int}}=Vector{Int}[], + tensor_symbols::Vector{Symbol}=Symbol[]) F = length(tensors_to_vars) tensors = Vector{BoolTensor}(undef, F) vars_to_tensors = [Int[] for _ in 1:var_num] - tensors_to_edges = [EdgeRef[] for _ in 1:F] for i in 1:F var_axes = tensors_to_vars[i] @assert length(tensor_data[i]) == 1 << length(var_axes) - tensors[i] = BoolTensor(i, var_axes, tensor_data[i]) - for (j, v) in enumerate(var_axes) + tensors[i] = BoolTensor(var_axes, tensor_data[i]) + for v in var_axes push!(vars_to_tensors[v], i) - push!(tensors_to_edges[i], EdgeRef(v, j)) - end - end - - axis_of_t = Dict{Tuple{Int,Int},Int}() - for (fid, tensor) in enumerate(tensors) - for (axis, vid) in enumerate(tensor.var_axes) - axis_of_t[(fid, vid)] = axis end end vars = Vector{Variable}(undef, var_num) for i in 1:var_num - vars[i] = Variable(i, 2, length(vars_to_tensors[i])) + vars[i] = Variable(length(vars_to_tensors[i])) end - # Precompute masks for every unique tensor - # Strategy: use hash values to quickly find identical tensors and avoid recomputation - tensor_to_masks = Vector{TensorMasks}(undef, F) - - # Dictionary keyed by hash for fast lookup - hash_to_masks = Dict{UInt, TensorMasks}() - hash_to_tensor = Dict{UInt, Vector{Tropical{Float64}}}() - - for (i, tensor) in enumerate(tensors) - # Compute the hash of the tensor contents - tensor_hash = hash(tensor.tensor) - - if haskey(hash_to_masks, tensor_hash) - # Hash collision check: ensure the contents truly match - if hash_to_tensor[tensor_hash] == tensor.tensor - # Reuse the previously computed masks - tensor_to_masks[i] = hash_to_masks[tensor_hash] - else - error("Hash collision: $tensor_hash") - end - else - # First time we see this hash, compute the masks - masks = build_tensor_masks(tensor) - hash_to_masks[tensor_hash] = masks - hash_to_tensor[tensor_hash] = tensor.tensor - tensor_to_masks[i] = masks - end + if isempty(tensor_depths) + tensor_depths = zeros(Int, F) + end + if isempty(tensor_fanin) + tensor_fanin = [Int[] for _ in 1:F] + end + if isempty(tensor_fanout) + tensor_fanout = [Int[] for _ in 1:F] + end + if isempty(tensor_symbols) + tensor_symbols = fill(:unknown, F) end - # Build the precomputed_masks dictionary for statistics (from unique tensors) - precomputed_masks = Dict{Vector{Tropical{Float64}}, TensorMasks}( - hash_to_tensor[h] => hash_to_masks[h] for h in keys(hash_to_masks) - ) - - return TNStatic(vars, tensors, vars_to_tensors, tensors_to_edges, axis_of_t, - precomputed_masks, tensor_to_masks) + return BipartiteGraph(vars, tensors, vars_to_tensors, tensor_depths, tensor_fanin, tensor_fanout, tensor_symbols) end -function setup_from_tensor_network(tn)::TNStatic +function setup_from_tensor_network(tn; tensor_depths::Vector{Int}=Int[], tensor_fanin::Vector{Vector{Int}}=Vector{Int}[], tensor_fanout::Vector{Vector{Int}}=Vector{Int}[], tensor_symbols::Vector{Symbol}=Symbol[])::BipartiteGraph t2v = getixsv(tn.code) tensors = GenericTensorNetworks.generate_tensors(Tropical(1.0), tn) - vec_tensors = [vec(t) for t in tensors] - new_tensors = [replace(t, Tropical(1.0) => zero(Tropical{Float64})) for t in vec_tensors] - return setup_problem(length(tn.problem.symbols), t2v, new_tensors) + new_tensors = [replace(vec(t), Tropical(1.0) => zero(Tropical{Float64})) for t in tensors] + return setup_problem(length(tn.problem.symbols), t2v, new_tensors; tensor_depths, tensor_fanin, tensor_fanout, tensor_symbols) end diff --git a/src/core/stats.jl b/src/core/stats.jl index a2b0761..2d2f145 100644 --- a/src/core/stats.jl +++ b/src/core/stats.jl @@ -1,122 +1,18 @@ -# Detailed statistics (optional, only allocated when needed) -mutable struct DetailedStats - # Depth distribution (node count per depth) - depth_distribution::Vector{Int} - - # Branching factor history (actual child count per branch) - branching_factors::Vector{Int} - - # Propagation efficiency - propagation_calls::Int - domain_reductions::Int - early_unsat_detections::Int - - # Time breakdown (seconds) - time_propagation::Float64 - time_branching::Float64 - time_contraction::Float64 - time_filtering::Float64 - - # Cache efficiency - cache_hits::Int - cache_misses::Int - - # Branch decision quality - variable_selection_counts::Dict{Int, Int} - remaining_vars_at_branch::Vector{Int} - depth_at_selection::Vector{Int} # Depth when each variable was selected - variable_selection_sequence::Vector{Int} # Variable selection order (by pick sequence) - successful_paths::Vector{Vector{Int}} # Successful paths from root to solution (variable sequence) -end - -DetailedStats() = DetailedStats( - Int[], - Int[], - 0, 0, 0, - 0.0, 0.0, 0.0, 0.0, - 0, 0, - Dict{Int, Int}(), - Int[], - Int[], - Int[], - Vector{Int}[] -) - mutable struct BranchingStats total_branches::Int total_subproblems::Int - max_depth::Int - solved_leaves::Int - - detailed::Union{Nothing, DetailedStats} end -BranchingStats(verbose::Bool = false) = BranchingStats( - 0, 0, 0, 0, - verbose ? DetailedStats() : nothing -) +BranchingStats() = BranchingStats(0, 0) function reset!(stats::BranchingStats) stats.total_branches = 0 stats.total_subproblems = 0 - stats.max_depth = 0 - stats.solved_leaves = 0 - - if !isnothing(stats.detailed) - d = stats.detailed - empty!(d.depth_distribution) - empty!(d.branching_factors) - d.propagation_calls = 0 - d.domain_reductions = 0 - d.early_unsat_detections = 0 - d.time_propagation = 0.0 - d.time_branching = 0.0 - d.time_contraction = 0.0 - d.time_filtering = 0.0 - d.cache_hits = 0 - d.cache_misses = 0 - empty!(d.variable_selection_counts) - empty!(d.remaining_vars_at_branch) - empty!(d.depth_at_selection) - empty!(d.variable_selection_sequence) - empty!(d.successful_paths) - end - return stats end function Base.copy(stats::BranchingStats) - detailed_copy = if stats.detailed !== nothing - d = stats.detailed - DetailedStats( - copy(d.depth_distribution), - copy(d.branching_factors), - d.propagation_calls, - d.domain_reductions, - d.early_unsat_detections, - d.time_propagation, - d.time_branching, - d.time_contraction, - d.time_filtering, - d.cache_hits, - d.cache_misses, - copy(d.variable_selection_counts), - copy(d.remaining_vars_at_branch), - copy(d.depth_at_selection), - copy(d.variable_selection_sequence), - [copy(path) for path in d.successful_paths] - ) - else - nothing - end - - return BranchingStats( - stats.total_branches, - stats.total_subproblems, - stats.max_depth, - stats.solved_leaves, - detailed_copy - ) + return BranchingStats(stats.total_branches, stats.total_subproblems) end function Base.getproperty(stats::BranchingStats, name::Symbol) @@ -133,237 +29,21 @@ function Base.propertynames(::BranchingStats; private::Bool=false) return (fieldnames(BranchingStats)..., :avg_branching_factor) end -@inline function record_depth!(stats::BranchingStats, depth::Int) - depth > stats.max_depth && (stats.max_depth = depth) - return nothing -end - -@inline function record_branch!(stats::BranchingStats, subproblem_count::Int, depth::Int) +@inline function record_branch!(stats::BranchingStats, subproblem_count::Int) stats.total_branches += 1 stats.total_subproblems += subproblem_count - record_depth!(stats, depth) - - # Record detailed statistics - if stats.detailed !== nothing - d = stats.detailed - push!(d.branching_factors, subproblem_count) - - # Update the depth distribution - while length(d.depth_distribution) <= depth - push!(d.depth_distribution, 0) - end - d.depth_distribution[depth + 1] += 1 - end - - return nothing -end - -@inline function record_unsat_leaf!(stats::BranchingStats, depth::Int) - record_depth!(stats, depth) return nothing end -@inline function record_solved_leaf!(stats::BranchingStats, depth::Int, current_path::Vector{Int} = Int[]) - stats.solved_leaves += 1 - record_depth!(stats, depth) - if stats.detailed !== nothing && !isempty(current_path) - push!(stats.detailed.successful_paths, copy(current_path)) - end - return nothing -end - -@inline function record_skipped_subproblem!(stats::BranchingStats) - return nothing -end - -# === Detailed statistics recording functions === - -@inline function record_propagation!(stats::BranchingStats, time_elapsed::Float64 = 0.0) - if stats.detailed !== nothing - stats.detailed.propagation_calls += 1 - stats.detailed.time_propagation += time_elapsed - end - return nothing -end - -@inline function record_domain_reduction!(stats::BranchingStats, reduction_count::Int) - if stats.detailed !== nothing - stats.detailed.domain_reductions += reduction_count - end - return nothing -end - -@inline function record_early_unsat!(stats::BranchingStats) - if stats.detailed !== nothing - stats.detailed.early_unsat_detections += 1 - end - return nothing -end - -@inline function record_branching_time!(stats::BranchingStats, time_elapsed::Float64) - if stats.detailed !== nothing - stats.detailed.time_branching += time_elapsed - end - return nothing -end - -@inline function record_contraction_time!(stats::BranchingStats, time_elapsed::Float64) - if stats.detailed !== nothing - stats.detailed.time_contraction += time_elapsed - end - return nothing -end - -@inline function record_filtering_time!(stats::BranchingStats, time_elapsed::Float64) - if stats.detailed !== nothing - stats.detailed.time_filtering += time_elapsed - end - return nothing -end - -@inline function record_cache_hit!(stats::BranchingStats) - if stats.detailed !== nothing - stats.detailed.cache_hits += 1 - end - return nothing -end - -@inline function record_cache_miss!(stats::BranchingStats) - if stats.detailed !== nothing - stats.detailed.cache_misses += 1 - end - return nothing -end - -@inline function record_variable_selection!(stats::BranchingStats, var::Int, remaining_vars::Int, depth::Int) - if stats.detailed !== nothing - d = stats.detailed - d.variable_selection_counts[var] = get(d.variable_selection_counts, var, 0) + 1 - push!(d.remaining_vars_at_branch, remaining_vars) - push!(d.depth_at_selection, depth) - push!(d.variable_selection_sequence, var) - end - return nothing -end - -# Check if we need to track paths (only when detailed stats are enabled) -@inline needs_path_tracking(stats::BranchingStats) = !isnothing(stats.detailed) - -# === Statistics analysis and visualization === +# === Statistics output === function print_stats_summary(stats::BranchingStats; io::IO = stdout) println(io, "=== Branching Statistics ===") - println(io, "Branch decisions: ", stats.total_branches) - println(io, "Child nodes: ", stats.total_subproblems) - println(io, "Max depth: ", stats.max_depth + 1) - println(io, "Solved leaves: ", stats.solved_leaves) - - if stats.detailed !== nothing - println(io, "\n=== Detailed Statistics ===") - d = stats.detailed - - # Propagation statistics - println(io, "\nPropagation:") - println(io, " Calls: ", d.propagation_calls) - println(io, " Domain reductions: ", d.domain_reductions) - println(io, " Early UNSAT detections: ", d.early_unsat_detections) - if d.propagation_calls > 0 - println(io, " Avg domains reduced per call: ", - round(d.domain_reductions / d.propagation_calls, digits=2)) - end - - # Timing statistics - total_time = d.time_propagation + d.time_branching + d.time_contraction + d.time_filtering - println(io, "\nTime breakdown:") - if total_time > 0 - println(io, " Propagation: ", round(d.time_propagation, digits=5), "s (", - round(100 * d.time_propagation / total_time, digits=5), "%)") - println(io, " Branching: ", round(d.time_branching, digits=5), "s (", - round(100 * d.time_branching / total_time, digits=5), "%)") - println(io, " Contraction: ", round(d.time_contraction, digits=5), "s (", - round(100 * d.time_contraction / total_time, digits=5), "%)") - println(io, " Filtering: ", round(d.time_filtering, digits=5), "s (", - round(100 * d.time_filtering / total_time, digits=5), "%)") - println(io, " Total: ", round(total_time, digits=5), "s") - else - println(io, " (Time statistics not recorded)") - end - - # Cache statistics - cache_total = d.cache_hits + d.cache_misses - if cache_total > 0 - println(io, "\nCache efficiency:") - println(io, " Hits: ", d.cache_hits) - println(io, " Misses: ", d.cache_misses) - println(io, " Hit rate: ", - round(100 * d.cache_hits / cache_total, digits=1), "%") - end - - # Branching factor distribution - if !isempty(d.branching_factors) - println(io, "\nBranching factor distribution:") - println(io, " Min: ", minimum(d.branching_factors)) - println(io, " Max: ", maximum(d.branching_factors)) - println(io, " Mean: ", round(sum(d.branching_factors) / length(d.branching_factors), digits=2)) - println(io, " Median: ", median(d.branching_factors)) - end - - # Depth distribution - if !isempty(d.depth_distribution) - println(io, "\nDepth distribution:") - # Compute cumulative node counts per depth to align with branching_factors - cumulative_nodes = 0 - for (depth_idx, node_count) in enumerate(d.depth_distribution) - if node_count > 0 - depth = depth_idx # Display depth starting from 1 - # Branching factor indices at this depth: cumulative_nodes+1 to cumulative_nodes+node_count - start_idx = cumulative_nodes + 1 - end_idx = cumulative_nodes + node_count - - if start_idx <= length(d.branching_factors) - end_idx = min(end_idx, length(d.branching_factors)) - depth_branching_factors = d.branching_factors[start_idx:end_idx] - avg_bf = round(sum(depth_branching_factors) / length(depth_branching_factors), digits=2) - total_subproblems = sum(depth_branching_factors) - println(io, " Depth ", depth, ": ", node_count, " nodes, ", - total_subproblems, " subproblems, avg branching factor: ", avg_bf) - else - println(io, " Depth ", depth, ": ", node_count, " nodes") - end - cumulative_nodes += node_count - end - end - end - - # Variable selection statistics - if !isempty(d.variable_selection_counts) - println(io, "\nVariable selection (top 10):") - sorted_vars = sort(collect(d.variable_selection_counts), by=x->x[2], rev=true) - # Compute the average remaining variable count and depth per variable - if !isempty(d.variable_selection_sequence) && - length(d.variable_selection_sequence) == length(d.remaining_vars_at_branch) && - length(d.variable_selection_sequence) == length(d.depth_at_selection) - for (var, count) in sorted_vars[1:min(10, length(sorted_vars))] - # Locate every position where this variable was selected - var_indices = [i for (i, v) in enumerate(d.variable_selection_sequence) if v == var] - avg_remaining = round(sum(d.remaining_vars_at_branch[i] for i in var_indices) / length(var_indices), digits=1) - avg_depth = round(sum(d.depth_at_selection[i] for i in var_indices) / length(var_indices), digits=1) - println(io, " Var ", var, ": ", count, " times, ", - "avg remaining vars: ", avg_remaining, ", ", - "avg depth: ", avg_depth + 1) - end - else - # Fallback display: show selection counts only - for (var, count) in sorted_vars[1:min(10, length(sorted_vars))] - println(io, " Var ", var, ": ", count, " times") - end - end - end + println(io, "Total branches: ", stats.total_branches) + println(io, "Total subproblems: ", stats.total_subproblems) - if !isempty(d.successful_paths) - println(io, "\nSuccessful paths:") - for (path_idx, path) in enumerate(d.successful_paths) - println(io, " Path ", path_idx, ": ", join([string(v) for v in path], " -> ")) - end - end + # Average branching factor + if stats.total_branches > 0 + avg_bf = stats.total_subproblems / stats.total_branches + println(io, "Average branching factor: ", round(avg_bf, digits=2)) end end diff --git a/src/core/types.jl b/src/core/types.jl index a4c8783..2af56e7 100644 --- a/src/core/types.jl +++ b/src/core/types.jl @@ -1,63 +1,18 @@ -struct Variable - id::Int - dom_size::Int +struct Variable deg::Int end function Base.show(io::IO, v::Variable) - print(io, "Variable($(v.id), dom_size=$(v.dom_size), deg=$(v.deg))") -end - -struct EdgeRef - var::Int - axis::Int -end - -function Base.show(io::IO, e::EdgeRef) - print(io, "EdgeRef($(e.var), axis=$(e.axis))") + print(io, "Variable(deg=$(v.deg))") end struct BoolTensor - id::Int var_axes::Vector{Int} tensor::Vector{Tropical{Float64}} end function Base.show(io::IO, f::BoolTensor) - print(io, "BoolTensor($(f.id), vars=[$(join(f.var_axes, ", "))], size=$(length(f.tensor)))") -end - -struct TensorMasks - sat::BitVector - axis_masks0::Vector{BitVector} - axis_masks1::Vector{BitVector} + print(io, "BoolTensor(vars=[$(join(f.var_axes, ", "))], size=$(length(f.tensor)))") end -# Build support masks for a tensor by enumerating all configurations. -function build_tensor_masks(tensor::BoolTensor) - nvars = length(tensor.var_axes) - n_cfg = 1 << nvars - - sat = falses(n_cfg) - axis_masks0 = [falses(n_cfg) for _ in 1:nvars] - axis_masks1 = [falses(n_cfg) for _ in 1:nvars] - - @inbounds for cfg in 0:(n_cfg-1) - # Check if this configuration satisfies the constraint - if tensor.tensor[cfg+1] == Tropical(0.0) # one(Tropical{Float64}) - sat[cfg+1] = true - end - - # Record which value each variable takes in this config - @inbounds for axis in 1:nvars - bit = (cfg >> (axis - 1)) & 1 - if bit == 0 - axis_masks0[axis][cfg+1] = true - else - axis_masks1[axis][cfg+1] = true - end - end - end - return TensorMasks(sat, axis_masks0, axis_masks1) -end diff --git a/src/core/workspace.jl b/src/core/workspace.jl deleted file mode 100644 index 56a5aeb..0000000 --- a/src/core/workspace.jl +++ /dev/null @@ -1,49 +0,0 @@ -mutable struct PropagationBuffers - feasible::BitVector - temp::BitVector - max_configs::Int -end - -function PropagationBuffers(static::TNStatic) - max_nvars = maximum(length(t.var_axes) for t in static.tensors; init=0) - max_configs = max_nvars > 0 ? (1 << max_nvars) : 1 - return PropagationBuffers(falses(max_configs), falses(max_configs), max_configs) -end - -mutable struct DynamicWorkspace - # Cache the full solution from the last branch for quick restoration - cached_doms::Vector{DomainMask} - has_cached_solution::Bool - # Branching statistics - branch_stats::BranchingStats - var_values::PriorityQueue{Int, Float64} - # O(1) membership test to avoid O(n) scans - changed_vars_flags::BitVector - changed_vars_indices::Vector{Int} - # Temporary BitVector cache for propagation to avoid reallocations - prop_buffers::Union{Nothing, PropagationBuffers} - # Cache of branch applications to avoid recomputing apply_branch - branch_cache::Dict{UInt, Dict{Tuple{UInt, Any}, Any}} - # Current search path (tracked only when verbose=true) - current_path::Vector{Int} -end - -DynamicWorkspace(var_num::Int, verbose::Bool = false) = DynamicWorkspace( - Vector{DomainMask}(undef, var_num), - false, - BranchingStats(verbose), - PriorityQueue{Int, Float64}(), - falses(var_num), - Int[], - nothing, - Dict{UInt, Dict{Tuple{UInt, Any}, Any}}(), - Int[] -) - -@inline function clear_branch_cache!(ws::DynamicWorkspace, doms_id::UInt) - inner = pop!(ws.branch_cache, doms_id, nothing) - if !isnothing(inner) - empty!(inner) - end - return nothing -end diff --git a/src/interface.jl b/src/interface.jl index b1dbf6d..f433e8d 100644 --- a/src/interface.jl +++ b/src/interface.jl @@ -1,113 +1,127 @@ -# Performance Note: -# For maximum performance on large problems, set verbose=false and show_stats=false. -# This disables all detailed statistics collection (timing, path tracking, etc.) -# and only collects basic counters. +function setup_from_cnf(cnf::CNF) + return setup_from_sat(Satisfiability(cnf; use_constraints=true)) +end -function setup_from_cnf(cnf::CNF; verbose::Bool = false) - return setup_from_sat(Satisfiability(cnf; use_constraints=true); verbose=verbose) +function setup_from_circuit(cir::Circuit) + return setup_from_sat(CircuitSAT(cir; use_constraints=true)) end -function setup_from_circuit(cir::Circuit; verbose::Bool = false) - return setup_from_sat(CircuitSAT(cir; use_constraints=true); verbose=verbose) +# Use multiple dispatch for different SAT types +function setup_from_sat(sat::CircuitSAT) + tn = GenericTensorNetwork(sat) + t2v = getixsv(tn.code) + tensors = GenericTensorNetworks.generate_tensors(Tropical(1.0), tn) + # Merge vec + replace to avoid intermediate allocation + tensor_data = [replace(vec(t), Tropical(1.0) => zero(Tropical{Float64})) for t in tensors] + + # Extract circuit metadata and symbols + circuit = sat.circuit + n_tensors = length(t2v) + tensor_symbols = [circuit.exprs[i].expr.head for i in 1:min(n_tensors, length(circuit.exprs))] + + # Compute circuit topology (depths, fanin, fanout) + circuit_info = compute_circuit_info(sat) + tensor_info = map_tensor_to_circuit_info(tn, circuit_info, sat) + + # Build BipartiteGraph + static = setup_problem(length(sat.symbols), t2v, tensor_data; tensor_depths=tensor_info.depths, tensor_fanin=tensor_info.fanin, tensor_fanout=tensor_info.fanout, tensor_symbols=tensor_symbols) + TNProblem(static) end -function setup_from_sat(sat::ConstraintSatisfactionProblem; verbose::Bool = false) +function setup_from_sat(sat::ConstraintSatisfactionProblem) tn = GenericTensorNetwork(sat) static = setup_from_tensor_network(tn) - TNProblem(static; verbose=verbose) + TNProblem(static) end function solve(problem::TNProblem, bsconfig::BranchingStrategy, reducer::AbstractReducer; show_stats::Bool=false) - reset_branching_stats!(problem) # Reset stats before solving - depth = OptimalBranchingCore.branch_and_reduce(problem, bsconfig, reducer, Tropical{Float64}; show_progress=false) - res = last_branch_problem(problem) - stats = get_branching_stats(problem) - clear_all_region_caches!() - if show_stats - print_stats_summary(stats) - end - return (res, depth, stats) + reset_problem!(problem) # Reset stats before solving + result = bbsat!(problem, bsconfig, reducer) + show_stats && print_stats_summary(result.stats) + return result end function solve_sat_problem( - sat::ConstraintSatisfactionProblem; + sat::ConstraintSatisfactionProblem; bsconfig::BranchingStrategy=BranchingStrategy( - table_solver=TNContractionSolver(1,2), - selector=MostOccurrenceSelector(), + table_solver=TNContractionSolver(), + selector==MinGammaSelector(1,2,TNContractionSolver(), GreedyMerge()), measure=NumUnfixedVars() - ), + ), reducer::AbstractReducer=NoReducer(), - verbose::Bool = false, show_stats::Bool=false ) - verbose = verbose || show_stats - tn_problem = setup_from_sat(sat; verbose=verbose) - result, depth, stats = solve(tn_problem, bsconfig, reducer; show_stats=show_stats) - satisfiable = !isnothing(result) - return satisfiable, result, depth, stats + tn_problem = setup_from_sat(sat) + result = solve(tn_problem, bsconfig, reducer; show_stats=show_stats) + return result.found, result.stats end function solve_sat_with_assignments( sat::ConstraintSatisfactionProblem; bsconfig::BranchingStrategy=BranchingStrategy( - table_solver=TNContractionSolver(1,2), - selector=MostOccurrenceSelector(), + table_solver=TNContractionSolver(), + selector==MinGammaSelector(1,2,TNContractionSolver(), GreedyMerge()), measure=NumUnfixedVars() ), reducer::AbstractReducer=NoReducer(), - verbose::Bool = false, show_stats::Bool=false ) - satisfiable, result, depth, stats = solve_sat_problem(sat; bsconfig, reducer, verbose=verbose, show_stats=show_stats) - if satisfiable && !isnothing(result) - # Convert TNProblem result to variable assignments + # Solve directly to get result + tn_problem = setup_from_sat(sat) + result = solve(tn_problem, bsconfig, reducer; show_stats=show_stats) + + if result.found + # Convert Result to variable assignments assignments = Dict{Symbol, Int}() for (i, symbol) in enumerate(sat.symbols) - assignments[symbol] = get_var_value(result, i) + assignments[symbol] = get_var_value(result.solution, i) end - return satisfiable, assignments, depth, stats + return true, assignments, result.stats else - return false, Dict{Symbol, Int}(), depth, stats + return false, Dict{Symbol, Int}(), result.stats end end +@inline factoring_circuit(n::Int, m::Int, N::Int) = reduceto(CircuitSAT, Factoring(n, m, N)).circuit.circuit +@inline factoring_csp(n::Int, m::Int, N::Int) = CircuitSAT(factoring_circuit(n, m, N); use_constraints=true) +@inline factoring_problem(n::Int, m::Int, N::Int) = setup_from_sat(factoring_csp(n, m, N)) + function solve_factoring( n::Int, m::Int, N::Int; bsconfig::BranchingStrategy=BranchingStrategy( - table_solver=TNContractionSolver(1,2), - # selector=MinGammaSelector(TNContractionSolver(1,2), GreedyMerge()), - selector=MostOccurrenceSelector(), + table_solver=TNContractionSolver(), + selector=MinGammaSelector(1,2,TNContractionSolver(), GreedyMerge()), measure=NumUnfixedVars(), set_cover_solver=GreedyMerge() ), reducer::AbstractReducer=NoReducer(), - verbose::Bool=false, show_stats::Bool=false ) - verbose = verbose || show_stats fproblem = Factoring(n, m, N) circuit_sat = reduceto(CircuitSAT, fproblem) problem = CircuitSAT(circuit_sat.circuit.circuit; use_constraints=true) - tn_problem = setup_from_sat(problem; verbose=verbose) - if verbose - unique_tensors = length(tn_problem.static.precomputed_masks) - total_tensors = length(tn_problem.static.tensors) - println("Unique tensor types: $unique_tensors (out of $total_tensors total)") + tn_problem = setup_from_sat(problem) + result = solve(tn_problem, bsconfig, reducer; show_stats=show_stats) + if !result.found + return nothing, nothing, result.stats end - res, _, stats = solve(tn_problem, bsconfig, reducer; show_stats=show_stats) - isnothing(res) && return nothing, nothing, stats - a = get_var_value(res, circuit_sat.q) - b = get_var_value(res, circuit_sat.p) - return bits_to_int(a), bits_to_int(b), stats + a = get_var_value(result.solution, circuit_sat.q) + b = get_var_value(result.solution, circuit_sat.p) + return bits_to_int(a), bits_to_int(b), result.stats end -# function solve_circuit_sat( -# circuit::CircuitSAT; -# bsconfig::BranchingStrategy=BranchingStrategy(table_solver=TNContractionSolver(), selector=LeastOccurrenceSelector(1, 2), measure=NumUnfixedVars()), -# reducer::AbstractReducer=NoReducer() -# ) -# tn_problem = setup_from_circuit(circuit.circuit) -# res, _, stats = solve(tn_problem, bsconfig, reducer) -# return res, stats -# end \ No newline at end of file +function solve_circuit_sat( + circuit::Circuit; + bsconfig::BranchingStrategy=BranchingStrategy( + table_solver=TNContractionSolver(), + selector=MinGammaSelector(1,2,TNContractionSolver(), GreedyMerge()), + measure=NumUnfixedVars() + ), + reducer::AbstractReducer=NoReducer(), + show_stats::Bool=false +) + tn_problem = setup_from_circuit(circuit) + result = solve(tn_problem, bsconfig, reducer; show_stats=show_stats) + return result.found, result.stats +end diff --git a/src/utils/circuit_analysis.jl b/src/utils/circuit_analysis.jl new file mode 100644 index 0000000..cf33cfd --- /dev/null +++ b/src/utils/circuit_analysis.jl @@ -0,0 +1,136 @@ +function compute_circuit_info(sat::ConstraintSatisfactionProblem) + circuit = sat.circuit + n_exprs = length(circuit.exprs) + + symbols = [circuit.exprs[i].expr.head for i in 1:n_exprs] + + var_to_producer = Dict{Symbol, Int}() + for (i, expr) in enumerate(circuit.exprs) + if expr.expr.head != :var + for v in expr.outputs + var_to_producer[v] = i + end + end + end + + var_to_consumers = Dict{Symbol, Vector{Int}}() + for v in sat.symbols + var_to_consumers[v] = Int[] + end + + for (i, expr) in enumerate(circuit.exprs) + if expr.expr.head == :var + for v in expr.outputs + if !haskey(var_to_consumers, v) + var_to_consumers[v] = Int[] + end + push!(var_to_consumers[v], i) + end + else + for arg in expr.expr.args + if arg isa BooleanExpr && arg.head == :var + var = arg.var + if !haskey(var_to_consumers, var) + var_to_consumers[var] = Int[] + end + push!(var_to_consumers[var], i) + end + end + end + end + + depths = zeros(Int, n_exprs) + + function compute_depth(expr_idx::Int) + if depths[expr_idx] > 0 + return depths[expr_idx] + end + + expr = circuit.exprs[expr_idx] + symbol = expr.expr.head + + if symbol == :var + depths[expr_idx] = 1 + return 1 + end + + max_consumer_depth = 0 + for v in expr.outputs + for consumer_idx in var_to_consumers[v] + consumer_depth = compute_depth(consumer_idx) + max_consumer_depth = max(max_consumer_depth, consumer_depth) + end + end + + depths[expr_idx] = max_consumer_depth + 1 + return depths[expr_idx] + end + + for i in 1:n_exprs + compute_depth(i) + end + + fanin = Vector{Vector{Symbol}}(undef, n_exprs) + fanout = Vector{Vector{Symbol}}(undef, n_exprs) + + for i in 1:n_exprs + expr = circuit.exprs[i] + symbol = expr.expr.head + + output_vars = expr.outputs + + if symbol == :var + fanin[i] = collect(output_vars) + constraint_value = expr.expr.var + fanout[i] = [constraint_value] + + else + input_vars = Symbol[] + for arg in expr.expr.args + if arg isa BooleanExpr && arg.head == :var + push!(input_vars, arg.var) + end + end + + fanin[i] = input_vars + fanout[i] = output_vars + end + end + + return (depths=depths, fanin=fanin, fanout=fanout, symbols=symbols) +end + +function map_tensor_to_circuit_info(tn, circuit_info, sat) + t2v = getixsv(tn.code) + n_tensors = length(t2v) + tensor_depths = zeros(Int, n_tensors) + tensor_fanin = Vector{Vector{Int}}(undef, n_tensors) + tensor_fanout = Vector{Vector{Int}}(undef, n_tensors) + + symbol_to_id = Dict{Symbol, Int}() + for (i, symbol) in enumerate(sat.symbols) + symbol_to_id[symbol] = i + end + + for i in 1:min(n_tensors, length(circuit_info.depths)) + tensor_depths[i] = circuit_info.depths[i] + + fanin_ids = Int[] + for sym in circuit_info.fanin[i] + if haskey(symbol_to_id, sym) + push!(fanin_ids, symbol_to_id[sym]) + end + end + tensor_fanin[i] = fanin_ids + + fanout_ids = Int[] + for sym in circuit_info.fanout[i] + if haskey(symbol_to_id, sym) + push!(fanout_ids, symbol_to_id[sym]) + end + end + tensor_fanout[i] = fanout_ids + end + + return (depths=tensor_depths, fanin=tensor_fanin, fanout=tensor_fanout) +end diff --git a/src/utils/utils.jl b/src/utils/utils.jl index d63bf86..e8ccafe 100644 --- a/src/utils/utils.jl +++ b/src/utils/utils.jl @@ -1,22 +1,46 @@ -@inline function get_unfixed_vars(doms::Vector{DomainMask})::Vector{Int} +@inline function get_unfixed_vars(problem::TNProblem)::Vector{Int} unfixed_vars = Int[] - @inbounds for (i, dm) in enumerate(doms) - if !is_fixed(dm) - push!(unfixed_vars, i) + @inbounds for (i, dm) in enumerate(problem.doms) + !is_fixed(dm) && push!(unfixed_vars, i) + end + return unfixed_vars +end + +function get_unfixed_vars(problem::TNProblem, tensor_ids::Vector{Int}) + unfixed_vars = Vector{Vector{Int}}(undef, length(tensor_ids)) + @inbounds for (i, tensor_id) in enumerate(tensor_ids) + unfixed = Int[] + vars = problem.static.tensors[tensor_id].var_axes + @inbounds for var_id in vars + !is_fixed(problem.doms[var_id]) && push!(unfixed, var_id) end + unfixed_vars[i] = unfixed end return unfixed_vars end -# Convenience: compute number of unfixed variables quickly. -@inline function count_unfixed(doms::Vector{DomainMask})::Int - c::Int = 0 - @inbounds for dm in doms - if !is_fixed(dm) - c += 1 +count_unfixed(doms::Vector{DomainMask}) = count(dom -> !is_fixed(dom), doms) + +bits_to_int(v::Vector{Bool}) = sum(b << (i - 1) for (i, b) in enumerate(v)) + +function get_active_tensors(static::BipartiteGraph, doms::Vector{DomainMask}) + active = Int[] + sizehint!(active, length(static.tensors)) + @inbounds for (tid, tensor) in enumerate(static.tensors) + # Check if any variable in this tensor is unfixed + has_unfixed = false + for var_id in tensor.var_axes + is_fixed(doms[var_id]) && continue + has_unfixed = true + break end + has_unfixed && push!(active, tid) end - return c + return active end -bits_to_int(v::Vector{Bool}) = sum(b << (i - 1) for (i, b) in enumerate(v)) \ No newline at end of file +# Check if a variable is masked (fixed) in the clause +ismasked(clause::Clause, var_idx::Int) = (clause.mask >> (var_idx - 1)) & 1 == 1 + +# Get the value for a variable from the clause +getbit(clause::Clause, var_idx::Int) = (clause.val >> (var_idx - 1)) & 1 == 1 diff --git a/src/utils/visualization.jl b/src/utils/visualization.jl new file mode 100644 index 0000000..c7cbffc --- /dev/null +++ b/src/utils/visualization.jl @@ -0,0 +1,244 @@ +function to_graph(bg::BipartiteGraph) + n_vars = length(bg.vars) + n_tensors = length(bg.tensors) + n_nodes = n_vars + n_tensors + + g = SimpleGraph(n_nodes) + + for (var_id, tensor_ids) in enumerate(bg.v2t) + for tensor_id in tensor_ids + add_edge!(g, var_id, n_vars + tensor_id) + end + end + + node_labels = Dict{Int, String}() + for i in 1:n_vars + node_labels[i] = "$i" + end + for i in 1:n_tensors + node_labels[n_vars + i] = "t$(i)$(bg.tensor_symbols[i])" + end + + return g, node_labels +end + +function to_graph(problem::TNProblem, tensor_indices::Union{Nothing, Vector{Int}}=nothing) + bg = problem.static + n_vars = length(bg.vars) + n_tensors = length(bg.tensors) + + # If tensor_indices is specified, filter tensors + if !isnothing(tensor_indices) + # Validate tensor indices + for idx in tensor_indices + if idx < 1 || idx > n_tensors + error("Invalid tensor index: $idx. Must be in range 1:$n_tensors") + end + end + + # Create filtered bipartite graph + # Find which variables are connected to the selected tensors + relevant_vars = Set{Int}() + for var_id in 1:n_vars + tensor_ids = bg.v2t[var_id] + if any(tid in tensor_indices for tid in tensor_ids) + push!(relevant_vars, var_id) + end + end + + relevant_vars = sort(collect(relevant_vars)) + n_relevant_vars = length(relevant_vars) + n_selected_tensors = length(tensor_indices) + n_nodes = n_relevant_vars + n_selected_tensors + + g = SimpleGraph(n_nodes) + + # Create mappings + var_to_node = Dict(var_id => i for (i, var_id) in enumerate(relevant_vars)) + tensor_to_node = Dict(tid => n_relevant_vars + i for (i, tid) in enumerate(tensor_indices)) + + # Add edges + for var_id in relevant_vars + for tensor_id in bg.v2t[var_id] + if tensor_id in tensor_indices + add_edge!(g, var_to_node[var_id], tensor_to_node[tensor_id]) + end + end + end + + # Create labels + node_labels = Dict{Int, String}() + for (i, var_id) in enumerate(relevant_vars) + node_labels[i] = "$var_id" + end + for (i, tensor_id) in enumerate(tensor_indices) + node_labels[n_relevant_vars + i] = "t$(tensor_id)$(bg.tensor_symbols[tensor_id])" + end + + # Create colors + node_colors = Dict{Int, Int}() + for (i, var_id) in enumerate(relevant_vars) + dom = problem.doms[var_id] + if is_fixed(dom) + node_colors[i] = has1(dom) ? 2 : 1 + else + node_colors[i] = 3 + end + end + for i in 1:n_selected_tensors + node_colors[n_relevant_vars + i] = 4 + end + + return g, node_labels, node_colors + else + # Original behavior: show all tensors + g, labels = to_graph(bg) + + node_colors = Dict{Int, Int}() + + for i in 1:n_vars + dom = problem.doms[i] + if is_fixed(dom) + node_colors[i] = has1(dom) ? 2 : 1 + else + node_colors[i] = 3 + end + end + + for i in 1:length(bg.tensors) + node_colors[n_vars + i] = 4 + end + + return g, labels, node_colors + end +end + + +function get_highest_degree_variables(problem::TNProblem, n::Int=1) + bg = problem.static + n_vars = length(bg.vars) + + # Calculate degree for each variable + degrees = [(var_id, length(bg.v2t[var_id])) for var_id in 1:n_vars] + + # Sort by degree (descending) + sort!(degrees, by=x->x[2], rev=true) + + # Return top n variable indices + return [degrees[i][1] for i in 1:min(n, length(degrees))] +end + + +function get_tensors_containing_variables(problem::TNProblem, var_indices::Vector{Int}) + bg = problem.static + tensor_set = Set{Int}() + + for var_id in var_indices + for tensor_id in bg.v2t[var_id] + push!(tensor_set, tensor_id) + end + end + + return sort(collect(tensor_set)) +end + + +function visualize_highest_degree_vars(problem::TNProblem, file_name::String; + n_vars::Int=1, + layout_algorithm::Symbol=:stress, + nlabels_fontsize::Real=8, + node_size::Real=20, + show_labels::Bool=true, + figure_size::Tuple{Int,Int}=(1200, 1200), + layout_kwargs...) + # Get highest degree variables + high_degree_vars = get_highest_degree_variables(problem, n_vars) + + # Get tensors containing these variables + tensor_indices = get_tensors_containing_variables(problem, high_degree_vars) + + # Print info + println("Highest degree variables: $high_degree_vars") + for var_id in high_degree_vars + degree = length(problem.static.v2t[var_id]) + println(" Variable $var_id: degree = $degree") + end + println("Tensors to visualize ($(length(tensor_indices))): $tensor_indices") + + # Visualize + visualize_problem(problem, file_name; + tensor_indices=tensor_indices, + layout_algorithm=layout_algorithm, + nlabels_fontsize=nlabels_fontsize, + node_size=node_size, + show_labels=show_labels, + figure_size=figure_size, + layout_kwargs...) +end + +function visualize_problem(problem::TNProblem, file_name::String; + tensor_indices::Union{Nothing, Vector{Int}}=nothing, + layout_algorithm::Symbol=:stress, + nlabels_fontsize::Real=8, + node_size::Real=20, + show_labels::Bool=true, + figure_size::Tuple{Int,Int}=(1200, 1200), + layout_kwargs...) + g, labels, colors = to_graph(problem, tensor_indices) + color_list = [colorant"red", colorant"green", colorant"blue", colorant"gray"] + node_colors = [color_list[colors[i]] for i in 1:nv(g)] + node_labels = [labels[i] for i in 1:nv(g)] + + n_vars = length(problem.static.vars) + n_tensors = length(problem.static.tensors) + n_nodes = nv(g) + + # Create figure and plot using GraphMakie + # Use larger figure size to give more space between nodes + fig = Figure(size=figure_size) + ax = Axis(fig[1, 1], + aspect=DataAspect(), # Maintain aspect ratio + xautolimitmargin=(0.15, 0.15), + yautolimitmargin=(0.15, 0.15)) + hidespines!(ax) + hidedecorations!(ax) + + # Select layout algorithm + layout = if layout_algorithm == :bipartite + # Special layout for bipartite graphs: place vars on left, tensors on right + # Use initial positions to separate the two groups + initialpos = Dict{Int, Point2f}() + # Place variable nodes on the left + for i in 1:n_vars + y_pos = (i - 1) / max(1, n_vars - 1) * 2 - 1 # Normalize to [-1, 1] + initialpos[i] = Point2f(-1.5, y_pos) + end + # Place tensor nodes on the right + for i in 1:n_tensors + y_pos = (i - 1) / max(1, n_tensors - 1) * 2 - 1 + initialpos[n_vars + i] = Point2f(1.5, y_pos) + end + # Use SFDP with initial positions + SFDP(Ptype=Float32; tol=0.01, C=0.2, K=1.0, initialpos=initialpos, layout_kwargs...) + elseif layout_algorithm == :spring + Spring(Ptype=Float32; C=2.0, iterations=100, layout_kwargs...) + elseif layout_algorithm == :sfdp + SFDP(Ptype=Float32; tol=0.01, C=0.2, K=1.0, iterations=100, layout_kwargs...) + elseif layout_algorithm == :stress + Stress(Ptype=Float32; iterations=500, layout_kwargs...) + elseif layout_algorithm == :spectral + Spectral(Ptype=Float32, dim=2) + else + error("Unknown layout algorithm: $layout_algorithm. Use :bipartite, :spring, :sfdp, :stress, or :spectral") + end + + p = graphplot!(ax, g, layout=layout, + nlabels=show_labels ? node_labels : nothing, + node_color=node_colors, + node_size=node_size, + nlabels_fontsize=nlabels_fontsize) + + # Save the figure (Makie handles format automatically based on extension) + save(file_name, fig) + return nothing +end \ No newline at end of file diff --git a/test/branch.jl b/test/branch.jl index 728998e..bb81856 100644 --- a/test/branch.jl +++ b/test/branch.jl @@ -1,18 +1,14 @@ using Test using BooleanInference -using BooleanInference: TNProblem, TNContractionSolver, MostOccurrenceSelector, NumUnfixedVars, setup_from_tensor_network, setup_problem, select_variables, get_cached_region, last_branch_problem, reset_last_branch_problem!, has_last_branch_problem, get_var_value, bits_to_int +using BooleanInference: TNProblem, TNContractionSolver, MostOccurrenceSelector, NumUnfixedVars, setup_from_tensor_network, setup_problem, select_variables, get_var_value, bits_to_int, branch_and_reduce!, Result using BooleanInference: BranchingStrategy, NoReducer -using OptimalBranchingCore: Clause -using OptimalBranchingCore: branching_table, branch_and_reduce, apply_branch using ProblemReductions: Factoring, reduceto, CircuitSAT, read_solution using GenericTensorNetworks -using TropicalNumbers: Tropical # using Logging # ENV["JULIA_DEBUG"] = "BooleanInference" @testset "branch" begin - # fproblem = Factoring(16, 16, 3363471157) fproblem = Factoring(10, 10, 559619) circuit_sat = reduceto(CircuitSAT, fproblem) @@ -21,28 +17,14 @@ using TropicalNumbers: Tropical tn = GenericTensorNetwork(problem) tn_static = setup_from_tensor_network(tn) tn_problem = TNProblem(tn_static) - @test !has_last_branch_problem(tn_problem) - br_strategy = BranchingStrategy(table_solver = TNContractionSolver(1,2), selector = MostOccurrenceSelector(), measure = NumUnfixedVars()) - res = branch_and_reduce(tn_problem, br_strategy, NoReducer(), Tropical{Float64}; show_progress=false) - @show res - if res != Tropical(-Inf) - @test has_last_branch_problem(tn_problem) - res = last_branch_problem(tn_problem) - @test res.n_unfixed == 0 - # @show circuit_sat.q, circuit_sat.p - - a = get_var_value(res, circuit_sat.q) - b = get_var_value(res, circuit_sat.p) - # @show a, b - @show bits_to_int(a), bits_to_int(b) + br_strategy = BranchingStrategy(table_solver = TNContractionSolver(), selector = MostOccurrenceSelector(1,2), measure = NumUnfixedVars()) + @time result = branch_and_reduce!(tn_problem, br_strategy, NoReducer(), Result; show_progress=false) + @show result.stats + if result.found + @test !isnothing(result.solution) + @test count_unfixed(result.solution) == 0 + a = get_var_value(result.solution, circuit_sat.q) + b = get_var_value(result.solution, circuit_sat.p) + @test bits_to_int(a) * bits_to_int(b) == 559619 end - clear_all_region_caches!() -end - -@testset "apply_branch" begin - @bools a b c d e f g - cnf = ∧(∨(a, b, ¬d, ¬e), ∨(¬a, d, e, ¬f), ∨(f, g), ∨(¬b, c)) - tn_problem = BooleanInference.setup_from_cnf(cnf) - new_problem, _ = apply_branch(tn_problem, Clause(0b110, 0b100), [1, 2, 3]) - @test new_problem.n_unfixed == 5 end diff --git a/test/branchtable.jl b/test/branchtable.jl new file mode 100644 index 0000000..6197812 --- /dev/null +++ b/test/branchtable.jl @@ -0,0 +1,11 @@ +using Test +using BooleanInference + +@testset "branchtable" begin + tn_problem = factoring_problem(12,12,10371761) + region = BooleanInference.select_region(tn_problem, NumUnfixedVars(), MostOccurrenceSelector(1,3)) + @show region + + table, variables = BooleanInference.branching_table!(tn_problem, TNContractionSolver(), region) + @show table +end \ No newline at end of file diff --git a/test/circuit_analysis.jl b/test/circuit_analysis.jl new file mode 100644 index 0000000..204cd84 --- /dev/null +++ b/test/circuit_analysis.jl @@ -0,0 +1,32 @@ +using BooleanInference +using TropicalNumbers +using ProblemReductions: @circuit, CircuitSAT +using BooleanInference.GenericTensorNetworks +using BooleanInference.GenericTensorNetworks: ∧, ∨, ¬ +using Test + +@testset "circuit analysis" begin + + circuit = @circuit begin + x = a ∨ b # 4 + y = x ∧ c # 3 + c = m ⊻ n # 4 + e = y ∧ f # 2 + e = true # 1 + end + + sat = CircuitSAT(circuit; use_constraints=true) + symbols = [sat.circuit.exprs[i].expr.head for i in 1:length(sat.circuit.exprs)] + @test symbols == [:∨, :∧, :⊻, :∧, :var] + + tn = GenericTensorNetwork(sat) + circuit_info = compute_circuit_info(sat) + tensor_info = map_tensor_to_circuit_info(tn, circuit_info, sat) + + @test circuit_info.depths == [4, 3, 4, 2, 1] + @test circuit_info.fanin == [[:a, :b], [:x, :c], [:m, :n], [:y, :f], [:e]] + @test circuit_info.fanout == [[:x], [:y], [:c], [:e], [Symbol("true")]] + +end + + diff --git a/test/contraction.jl b/test/contraction.jl index 72cc971..7413ad8 100644 --- a/test/contraction.jl +++ b/test/contraction.jl @@ -1,11 +1,9 @@ using Test using BooleanInference -using BooleanInference: setup_from_tensor_network, TNProblem, DynamicWorkspace, setup_problem, select_variables, get_cached_region, MostOccurrenceSelector, NumUnfixedVars +using BooleanInference: setup_from_tensor_network, TNProblem, setup_problem, select_variables, MostOccurrenceSelector, NumUnfixedVars using BooleanInference: Region, slicing, tensor_unwrapping, DomainMask using BooleanInference: DM_BOTH, DM_0, DM_1, has0, has1, is_fixed using BooleanInference: contract_tensors, contract_region, TNContractionSolver -using BooleanInference: extract_inner_configs, combine_configs, handle_no_boundary_case_unfixed -using BooleanInference: clear_all_region_caches! using OptimalBranchingCore: branching_table using TropicalNumbers: Tropical using ProblemReductions: Factoring, reduceto, CircuitSAT @@ -14,13 +12,11 @@ using GenericTensorNetworks @testset "Region constructor" begin region = Region(1, [1, 2], - [3, 4], - [1, 2]) + [1, 2, 3, 4]) @test region.id == 1 @test length(region.tensors) == 2 - @test length(region.inner_vars) == 2 - @test length(region.boundary_vars) == 2 + @test length(region.vars) == 4 end @testset "tensor_unwrapping" begin @@ -204,224 +200,3 @@ end @test result[2,2,1] == zero(Tropical{Float64}) end -function generate_example_problem(n::Int = 12) - fproblem = Factoring(n, n, 6) - res = reduceto(CircuitSAT, fproblem) - problem = CircuitSAT(res.circuit.circuit; use_constraints=true) - return problem -end - -@testset "contract_region" begin - problem = generate_example_problem() - tn = GenericTensorNetwork(problem) - tn_static = setup_from_tensor_network(tn) - tn_problem = TNProblem(tn_static) - variable = select_variables(tn_problem, NumUnfixedVars(), MostOccurrenceSelector()) - @test variable isa Int - - # Create region for the selected variable - solver = TNContractionSolver(1, 2) - all_unfixed_doms = fill(DM_BOTH, length(tn_problem.doms)) - region = k_neighboring(tn_static, all_unfixed_doms, variable; max_tensors=solver.max_tensors, k=solver.k) - @test region !== nothing - - contracted, output_vars = contract_region(tn_static, region, tn_problem.doms) - @test contracted !== nothing - @test length(output_vars) <= length(region.boundary_vars) + length(region.inner_vars) - - table = branching_table(tn_problem, TNContractionSolver(), region.id) - @show vcat([v for v in region.boundary_vars], [v for v in region.inner_vars]) - @show table -end - - -# These test sets are commented out because the functions they test -# (separate_fixed_free_boundary, construct_boundary_config, construct_inner_config) -# are no longer in the codebase - they appear to have been refactored. -# The functionality is now handled internally by other functions. -# @testset "separate_fixed_free_boundary" begin -# region = Region(1, -# [1, 2], -# [5, 6], -# [3, 4]) -# -# doms = fill(DM_BOTH, 10) -# fixed, fixed_vals, free, free_indices = separate_fixed_free_boundary(region, doms) -# @test isempty(fixed) -# @test isempty(fixed_vals) -# @test length(free) == 2 -# @test free == Int[3, 4] -# @test free_indices == [1, 2] -# -# doms[3] = DM_0 -# doms[4] = DM_1 -# fixed, fixed_vals, free, free_indices = separate_fixed_free_boundary(region, doms) -# @test length(fixed) == 2 -# @test fixed == Int[3, 4] -# @test fixed_vals == Int[0, 1] -# @test isempty(free) -# @test isempty(free_indices) -# -# doms[3] = DM_0 -# doms[4] = DM_BOTH -# fixed, fixed_vals, free, free_indices = separate_fixed_free_boundary(region, doms) -# @test length(fixed) == 1 -# @test fixed == Int[3] -# @test fixed_vals == Int[0] -# @test length(free) == 1 -# @test free == Int[4] -# @test free_indices == [2] -# end - -# @testset "construct_boundary_config" begin -# region = Region(1, -# [1], -# [5], -# [3, 4]) -# -# doms = fill(DM_BOTH, 10) -# free_boundary_indices = [1, 2] -# # Build free_pos_of_boundary: maps boundary position to free position -# n_boundary = length(region.boundary_vars) -# free_pos_of_boundary = zeros(Int, n_boundary) -# for (j, boundary_idx) in enumerate(free_boundary_indices) -# free_pos_of_boundary[boundary_idx] = j -# end -# -# config = construct_boundary_config(region, doms, free_pos_of_boundary, 0) -# @test config == [false, false] -# -# config = construct_boundary_config(region, doms, free_pos_of_boundary, 1) -# @test config == [true, false] -# -# config = construct_boundary_config(region, doms, free_pos_of_boundary, 2) -# @test config == [false, true] -# -# config = construct_boundary_config(region, doms, free_pos_of_boundary, 3) -# @test config == [true, true] -# -# doms[3] = DM_1 -# free_boundary_indices = [2] -# # Rebuild free_pos_of_boundary with new free_boundary_indices -# free_pos_of_boundary = zeros(Int, n_boundary) -# for (j, boundary_idx) in enumerate(free_boundary_indices) -# free_pos_of_boundary[boundary_idx] = j -# end -# -# config = construct_boundary_config(region, doms, free_pos_of_boundary, 0) -# @test config == [true, false] -# -# config = construct_boundary_config(region, doms, free_pos_of_boundary, 1) -# @test config == [true, true] -# end - -@testset "extract_inner_configs" begin - T0 = zero(Tropical{Float64}) - T1 = one(Tropical{Float64}) - - # extract_inner_configs now returns Vector{UInt64}, not Vector{Bool} - contracted_1d = reshape([T1, T0], 2) - configs = extract_inner_configs(contracted_1d, 1) - @test length(configs) == 1 - @test configs[1] == UInt64(0) # 0 in binary = [false] - - contracted_2d = reshape([T1, T0, T1, T1], 2, 2) - configs = extract_inner_configs(contracted_2d, 2) - @test length(configs) == 3 - # Julia uses column-major order, so: - # Linear index 1 -> [1,1] -> T1 -> config 0 (0b00 = [false, false]) - # Linear index 2 -> [2,1] -> T0 -> config 1 (0b01 = [false, true]) - NOT satisfied, so not in configs - # Linear index 3 -> [1,2] -> T1 -> config 2 (0b10 = [true, false]) - # Linear index 4 -> [2,2] -> T1 -> config 3 (0b11 = [true, true]) - @test UInt64(0) in configs # [false, false] - @test !(UInt64(1) in configs) # [false, true] - NOT satisfied - @test UInt64(2) in configs # [true, false] - @test UInt64(3) in configs # [true, true] - - contracted_3d = reshape([T1, T1, T1, T1, T1, T1, T1, T1], 2, 2, 2) - configs = extract_inner_configs(contracted_3d, 3) - @test length(configs) == 8 -end - -# construct_inner_config is no longer in the codebase - it appears to have been refactored. -# @testset "construct_inner_config" begin -# region = Region(1, -# [1], -# [5, 6, 7], -# [3]) -# -# doms = fill(DM_BOTH, 10) -# inner_var_ids = Int[5, 6, 7] -# # Build inner_posmap: maps var_id to position in free inner vars -# inner_posmap = zeros(Int, maximum(inner_var_ids)) -# for (j, var_id) in enumerate(inner_var_ids) -# inner_posmap[var_id] = j -# end -# free_inner_configs = [[false, false, false], [true, false, true]] -# -# inner_configs = construct_inner_config(region, doms, inner_posmap, free_inner_configs) -# @test length(inner_configs) == 2 -# @test inner_configs[1] == [false, false, false] -# @test inner_configs[2] == [true, false, true] -# -# doms[5] = DM_1 -# inner_var_ids = Int[6, 7] -# # Rebuild inner_posmap with new inner_var_ids -# inner_posmap = zeros(Int, maximum(inner_var_ids)) -# for (j, var_id) in enumerate(inner_var_ids) -# inner_posmap[var_id] = j -# end -# free_inner_configs = [[false, false], [false, true]] -# -# inner_configs = construct_inner_config(region, doms, inner_posmap, free_inner_configs) -# @test length(inner_configs) == 2 -# @test inner_configs[1] == [true, false, false] -# @test inner_configs[2] == [true, false, true] -# -# doms[6] = DM_0 -# inner_var_ids = Int[7] -# # Rebuild inner_posmap with new inner_var_ids -# inner_posmap = zeros(Int, maximum(inner_var_ids)) -# for (j, var_id) in enumerate(inner_var_ids) -# inner_posmap[var_id] = j -# end -# free_inner_configs = [[false], [true]] -# -# inner_configs = construct_inner_config(region, doms, inner_posmap, free_inner_configs) -# @test length(inner_configs) == 2 -# @test inner_configs[1] == [true, false, false] -# @test inner_configs[2] == [true, false, true] -# end - -@testset "combine_configs" begin - # combine_configs now takes (boundary_bits::UInt64, inner_configs::Vector{UInt64}, n_boundary::Int) - # and returns Vector{UInt64} - # Note: bit representation uses LSB first, so 0b01 = [true, false], 0b10 = [false, true] - boundary_bits = UInt64(0b01) # [true, false] = 1 in binary (bit0=1, bit1=0) - inner_configs = [UInt64(0b01), UInt64(0b10)] # [true, false] and [false, true] - n_boundary = 2 - - full_configs = combine_configs(boundary_bits, inner_configs, n_boundary) - @test length(full_configs) == 2 - # boundary=01 (1), inner=01 (1) -> full = 01 | (01 << 2) = 1 | 4 = 5 (0b101 = [true, false, true, false]) - # boundary=01 (1), inner=10 (2) -> full = 01 | (10 << 2) = 1 | 8 = 9 (0b1001 = [true, false, false, true]) - @test UInt64(5) in full_configs # [true, false, true, false] - @test UInt64(9) in full_configs # [true, false, false, true] - - boundary_bits = UInt64(0b1) # [true] - inner_configs = [UInt64(0b0)] # [false] - n_boundary = 1 - - full_configs = combine_configs(boundary_bits, inner_configs, n_boundary) - @test length(full_configs) == 1 - @test full_configs[1] == UInt64(1) # [true, false] - - boundary_bits = UInt64(0b0) # [] - inner_configs = [UInt64(0b11), UInt64(0b00)] # [true, true] and [false, false] - n_boundary = 0 - - full_configs = combine_configs(boundary_bits, inner_configs, n_boundary) - @test length(full_configs) == 2 - @test UInt64(3) in full_configs # [true, true] - @test UInt64(0) in full_configs # [false, false] -end diff --git a/test/greedymerge.jl b/test/greedymerge.jl index 7d3f853..b603f44 100644 --- a/test/greedymerge.jl +++ b/test/greedymerge.jl @@ -14,7 +14,7 @@ function create_test_problem() fill(Tropical(0.0), 4) ] static = BooleanInference.setup_problem(3, dummy_tensors_to_vars, dummy_tensor_data) - return TNProblem(static) + return TNProblem(static, UInt8) end @@ -25,6 +25,7 @@ end # Test with a valid clause clause = Clause(0b11, 0b10) # variable 1 = 1 + reduction = OptimalBranchingCore.size_reduction(problem, measure, clause, variables) @test isfinite(reduction) @@ -73,7 +74,6 @@ end measure = NumUnfixedVars() # Test that clauses with invalid reductions are filtered out - # This tests drop_invalid_rows! indirectly clauses = [ [Clause(0b11, 0b10)], # Valid [Clause(0b11, 0b00)] # Might be invalid @@ -121,19 +121,6 @@ end @test !isempty(result_clauses) || isempty(clauses) end -@testset "greedymerge - empty clauses" begin - problem = create_test_problem() - variables = [1, 2] - measure = NumUnfixedVars() - - # Test with empty clause set - empty_clauses = Vector{Vector{Clause{UInt64}}}() - result = OptimalBranchingCore.greedymerge(empty_clauses, problem, variables, measure) - @test result.γ == Inf - result_clauses = OptimalBranchingCore.get_clauses(result) - @test isempty(result_clauses) -end - @testset "greedymerge - invalid clauses" begin problem = create_test_problem() variables = [1, 2] diff --git a/test/interface.jl b/test/interface.jl index c81979d..0f73fc7 100644 --- a/test/interface.jl +++ b/test/interface.jl @@ -1,9 +1,9 @@ using BooleanInference -using BooleanInference.GenericTensorNetworks -using BooleanInference.GenericTensorNetworks: ∧, ∨, ¬ +using GenericTensorNetworks +using GenericTensorNetworks: ∧, ∨, ¬ using Test -using BooleanInference.GenericTensorNetworks.ProblemReductions -using BooleanInference.OptimalBranchingCore: BranchingStrategy +using GenericTensorNetworks.ProblemReductions +using OptimalBranchingCore @testset "setup_from_cnf" begin @bools a b c d e f g @@ -11,12 +11,8 @@ using BooleanInference.OptimalBranchingCore: BranchingStrategy he2v = [] tnproblem = setup_from_cnf(cnf) - for tensors in tnproblem.static.t2v - list = [] - for item in tensors - push!(list, item.var) - end - push!(he2v, list) + for tensor in tnproblem.static.tensors + push!(he2v, tensor.var_axes) end @test he2v == [[1, 2, 3, 4], [1, 3, 4, 5], [5, 6], [2, 7], [1]] @show tnproblem.static.tensors[3].tensor[1] == zero(Tropical{Float64}) @@ -30,12 +26,8 @@ end push!(circuit.exprs, Assignment([:c],BooleanExpr(true))) tnproblem = setup_from_circuit(circuit) he2v = [] - for tensors in tnproblem.static.t2v - list = [] - for item in tensors - push!(list, item.var) - end - push!(he2v, list) + for tensor in tnproblem.static.tensors + push!(he2v, tensor.var_axes) end @test he2v == [[1, 2, 3],[1]] @test tnproblem.static.tensors[1].tensor == vec(Tropical.([0.0 0.0; -Inf -Inf;;; 0.0 -Inf; -Inf 0.0])) @@ -48,20 +40,16 @@ end @bools a b c d e f g cnf = ∧(∨(a, b, ¬d, ¬e), ∨(¬a, d, e, ¬f), ∨(f, g), ∨(¬b, c), ∨(¬a)) sat = Satisfiability(cnf; use_constraints=true) - res, dict, _, stats = solve_sat_with_assignments(sat) + res, dict, stats = solve_sat_with_assignments(sat) @test res == true @test satisfiable(cnf, dict) == true # Test that stats are recorded @test stats.total_branches >= 0 - @test stats.max_depth >= 0 + @test stats.total_subproblems >= 0 cnf = ∧(∨(a), ∨(a,¬c), ∨(d,¬b), ∨(¬c,¬d), ∨(a,e), ∨(a,e,¬c), ∨(¬a)) sat = Satisfiability(cnf; use_constraints=true) - res, dict, _, stats = solve_sat_with_assignments(sat) - @test res == false - # @test satisfiable(cnf, dict) == false - @test isempty(dict) - @test stats.total_branches >= 0 + @test_throws ErrorException setup_from_sat(sat) end @testset "solve_factoring" begin @@ -69,7 +57,7 @@ end @test a*b == 31*29 @test stats.total_branches >= 0 @test stats.total_subproblems >= 0 - println("Factoring stats: branches=$(stats.total_branches), subproblems=$(stats.total_subproblems), max_depth=$(stats.max_depth)") + println("Factoring stats: branches=$(stats.total_branches), subproblems=$(stats.total_subproblems)") end @testset "branching_statistics" begin @@ -83,49 +71,26 @@ end initial_stats = get_branching_stats(tn_problem) @test initial_stats.total_branches == 0 @test initial_stats.total_subproblems == 0 - @test initial_stats.max_depth == 0 - + # Solve and check stats are recorded - result, depth, stats = BooleanInference.solve(tn_problem, - BranchingStrategy(table_solver=TNContractionSolver(1, 2), - selector=MostOccurrenceSelector(), - measure=NumUnfixedVars()), + result = BooleanInference.solve(tn_problem, + BranchingStrategy(table_solver=TNContractionSolver(), + selector=MostOccurrenceSelector(1,2), + measure=NumUnfixedVars()), NoReducer()) - + # Stats should have been recorded - @test stats.total_branches > 0 || result !== nothing # Either branched or solved immediately - @test stats.total_subproblems >= 0 # Each branch creates at least 2 subproblems - @test stats.max_depth >= 0 - @test stats.avg_branching_factor >= 0.0 - + @test result.stats.total_branches >= 0 + @test result.stats.total_subproblems >= 0 + @test result.stats.avg_branching_factor >= 0.0 + # Print stats for debugging println("\nBranching Statistics:") - print_stats_summary(stats) + print_stats_summary(result.stats) # Test reset functionality - reset_branching_stats!(tn_problem) + reset_problem!(tn_problem) reset_stats = get_branching_stats(tn_problem) @test reset_stats.total_branches == 0 @test reset_stats.total_subproblems == 0 - @test reset_stats.max_depth == 0 end - -# @testset "benchmark" begin -# table_solver = TNContractionSolver() -# reducer = NoReducer() -# for selector in [] -# for measure in [NumOfVertices(), NumOfClauses(), NumOfDegrees()] -# println("$measure,$selector") -# solve_factoring(8, 8, 1019 * 1021; bsconfig = BranchingStrategy(; table_solver, selector, measure), reducer) -# end -# end -# end - -# @testset "interface" begin -# solve_factoring(8, 8, 1019 * 1021; bsconfig = BranchingStrategy(; table_solver= TNContractionSolver(), selector=KNeighborSelector(1, 1), measure=NumOfDegrees()), reducer= NoReducer()) -# solve_factoring(5, 5, 899; bsconfig = BranchingStrategy(; table_solver= TNContractionSolver(), selector=KNeighborSelector(1, 1), measure=NumOfDegrees()), reducer= NoReducer()) - -# bs = BranchingStrategy(table_solver = TNContractionSolver(), selector = KNeighborSelector(1, 1), set_cover_solver = BooleanInference.OptimalBranchingCore.GreedyMerge(),measure=NumOfDegrees()) - -# solve_factoring(8, 8, 1019 * 1021; bsconfig = bs, reducer= NoReducer()) -# end \ No newline at end of file diff --git a/test/knn.jl b/test/knn.jl index c2b30fd..d08a61f 100644 --- a/test/knn.jl +++ b/test/knn.jl @@ -29,11 +29,11 @@ end doms = BooleanInference.init_doms(problem.static) region = k_neighboring(problem.static, doms, 1; max_tensors=100, k=1) @test region.tensors == [1, 3] - @test Set(union(region.inner_vars, region.boundary_vars)) == Set([1, 4]) + @test Set(region.vars) == Set([1, 4]) region = k_neighboring(problem.static, doms, 2; max_tensors=100, k=1) @test region.tensors == [2, 5, 6] - @test Set(union(region.inner_vars, region.boundary_vars)) == Set([2, 3, 5]) + @test Set(region.vars) == Set([2, 3, 5]) end @@ -45,11 +45,9 @@ end doms = BooleanInference.init_doms(problem.static) region = k_neighboring(problem.static, doms, 1; max_tensors=100, k=2) @test region.tensors == [1, 3, 4] - @test Set(union(region.inner_vars, region.boundary_vars)) == Set([1, 3, 4]) - @test region.boundary_vars == [3] + @test Set(region.vars) == Set([1, 3, 4]) region = k_neighboring(problem.static, doms, 2; max_tensors=100, k=2) @test region.tensors == [2, 4, 5, 6] - @test Set(union(region.inner_vars, region.boundary_vars)) == Set([2, 3, 4, 5]) - @test region.boundary_vars == [4] + @test Set(region.vars) == Set([2, 3, 4, 5]) end \ No newline at end of file diff --git a/test/problems.jl b/test/problems.jl index 3b7cdc1..7b62896 100644 --- a/test/problems.jl +++ b/test/problems.jl @@ -19,7 +19,6 @@ end @test length(problem.vars) == length(tn.problem.symbols) @test length(problem.tensors) > 0 @test length(problem.v2t) == length(problem.vars) - @test length(problem.t2v) == length(problem.tensors) @show problem end @@ -37,27 +36,24 @@ end [Tropical(0.0), Tropical(0.0), Tropical(0.0), Tropical(1.0)], # AND: [0,0,0,1] [Tropical(1.0), Tropical(0.0)] # NOT: [1,0] ] - + tn = setup_problem(var_num, tensors_to_vars, tensor_data) - + @test length(tn.vars) == 2 - @test all(v.dom_size == 2 for v in tn.vars) - + @test all(v.deg > 0 for v in tn.vars) + @test length(tn.tensors) == 2 @test length(tn.tensors[1].var_axes) == 2 @test length(tn.tensors[2].var_axes) == 1 - + @test length(tn.v2t) == 2 @test length(tn.v2t[1]) == 1 @test length(tn.v2t[2]) == 2 - - @test length(tn.t2v) == 2 - @test length(tn.t2v[1]) == 2 - @test length(tn.t2v[2]) == 1 - - @test haskey(tn.axis_of_t, (1, 1)) - @test haskey(tn.axis_of_t, (1, 2)) - @test haskey(tn.axis_of_t, (2, 2)) + + # Verify var_axes can replace t2v + @test length(tn.tensors[1].var_axes) == 2 + @test 1 in tn.tensors[1].var_axes + @test 2 in tn.tensors[1].var_axes end @testset "setup_from_tensor_network" begin diff --git a/test/propagate.jl b/test/propagate.jl index 08603d1..426f139 100644 --- a/test/propagate.jl +++ b/test/propagate.jl @@ -109,7 +109,7 @@ using GenericTensorNetworks # Propagation should detect contradiction propagated = BooleanInference.propagate(static, doms) - @test all(d -> d.bits == 0x00, propagated) + @test all(d -> d == BooleanInference.DM_NONE, propagated) end # Test 5: Chain propagation diff --git a/test/runtests.jl b/test/runtests.jl index 8991a84..f7ddea4 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -1,38 +1,38 @@ using BooleanInference using Test -@testset "branch.jl" begin - include("branch.jl") -end +# @testset "branch.jl" begin +# include("branch.jl") +# end -@testset "contraction.jl" begin - include("contraction.jl") -end +# @testset "contraction.jl" begin +# include("contraction.jl") +# end -@testset "interface.jl" begin - include("interface.jl") -end +# @testset "interface.jl" begin +# include("interface.jl") +# end -@testset "knn.jl" begin - include("knn.jl") -end +# # @testset "knn.jl" begin +# # include("knn.jl") +# # end -@testset "problems.jl" begin - include("problems.jl") -end +# @testset "problems.jl" begin +# include("problems.jl") +# end -@testset "propagate.jl" begin - include("propagate.jl") -end +# @testset "propagate.jl" begin +# include("propagate.jl") +# end -@testset "selector.jl" begin - include("selector.jl") -end +# @testset "greedymerge.jl" begin +# include("greedymerge.jl") +# end -@testset "stats.jl" begin - include("stats.jl") -end +# @testset "circuit_analysis.jl" begin +# include("circuit_analysis.jl") +# end -@testset "greedymerge.jl" begin - include("greedymerge.jl") -end +# @testset "branchtable.jl" begin +# include("branchtable.jl") +# end \ No newline at end of file diff --git a/test/selector.jl b/test/selector.jl deleted file mode 100644 index b23c9f1..0000000 --- a/test/selector.jl +++ /dev/null @@ -1,75 +0,0 @@ -using Test -using BooleanInference -using BooleanInference: TNProblem, MostOccurrenceSelector, MinGammaSelector, TNContractionSolver, NumUnfixedVars, setup_problem -using OptimalBranchingCore -using TropicalNumbers - -const dummy_tensors_to_vars = [[1, 2], [2, 3], [2]] -const dummy_tensor_data = [ - fill(Tropical(0.0), 4), - fill(Tropical(0.0), 4), - fill(Tropical(0.0), 2) -] - -function build_dummy_problem() - static = BooleanInference.setup_problem(3, dummy_tensors_to_vars, dummy_tensor_data) - return TNProblem(static) -end - -@testset "MostOccurrenceSelector" begin - problem = build_dummy_problem() - selector = MostOccurrenceSelector() - chosen = OptimalBranchingCore.select_variables(problem, NumUnfixedVars(), selector) - - # Variable 2 appears in all 3 tensors, so it should be selected - # Variable 1 appears in tensor 1, variable 3 appears in tensor 2 - @test chosen == 2 -end - -# Mock implementations for MinGammaSelector testing -struct MockTableSolver <: OptimalBranchingCore.AbstractTableSolver end -struct MockSetCoverSolver <: OptimalBranchingCore.AbstractSetCoverSolver end - -# Gamma values for testing: var 2 has lower gamma, var 3 has higher gamma -const gamma_values = Dict(2 => 0.25, 3 => 0.9) - -function OptimalBranchingCore.branching_table( - ::TNProblem, - ::MockTableSolver, - var::Int -)::Tuple{OptimalBranchingCore.BranchingTable, Vector{Int}} - # Return empty table for var 1 (UNSAT), valid tables for others - if var == 1 - return OptimalBranchingCore.BranchingTable(0, Vector{UInt64}[]), Int[] - else - # Return a simple valid branching table - return OptimalBranchingCore.BranchingTable(1, [[0x0, 0x1]]), [var] - end -end - -function OptimalBranchingCore.optimal_branching_rule( - ::OptimalBranchingCore.BranchingTable, - variables::Vector{Int}, - ::TNProblem, - ::OptimalBranchingCore.AbstractMeasure, - ::MockSetCoverSolver -) - var = first(variables) - gamma = get(gamma_values, var, Inf) - # Return a result with the gamma value - # The actual structure depends on OptimalBranchingCore, but we need γ field - return (γ=gamma, clauses=[[var]]) -end - -OptimalBranchingCore.get_clauses(result) = result.clauses - -@testset "MinGammaSelector" begin - problem = build_dummy_problem() - selector = MinGammaSelector(MockTableSolver(), MockSetCoverSolver()) - chosen = OptimalBranchingCore.select_variables(problem, NumUnfixedVars(), selector) - - # Variable 2 has gamma 0.25, variable 3 has gamma 0.9 - # Variable 1 should be skipped (empty table) - # So variable 2 should be selected - @test chosen == 2 -end diff --git a/test/singletensor.jl b/test/singletensor.jl new file mode 100644 index 0000000..c88e842 --- /dev/null +++ b/test/singletensor.jl @@ -0,0 +1,140 @@ +using Test +using BooleanInference +using OptimalBranchingCore + +@testset "SingleTensorSolver" begin + @testset "partition_tensor_variables" begin + # Test with mixed fixed and unfixed variables + doms = [DM_0, DM_BOTH, DM_1, DM_BOTH, DM_0] + tensor_vars = [1, 2, 3, 4, 5] + + fixed_pos, unfixed_pos, unfixed_ids = partition_tensor_variables(tensor_vars, doms) + + @test length(fixed_pos) == 3 + @test (1, false) in fixed_pos # var 1 fixed to 0 + @test (3, true) in fixed_pos # var 3 fixed to 1 + @test (5, false) in fixed_pos # var 5 fixed to 0 + + @test unfixed_pos == [2, 4] + @test unfixed_ids == [2, 4] + end + + @testset "SingleTensorSolver basic test" begin + # Create a problem with 3 variables and 2 tensors + # Tensor 1: v1 OR v2 (has multiple satisfying assignments) + # Tensor 2: v2 OR v3 (has multiple satisfying assignments) + using TropicalNumbers + + # Tensor 1: v1 OR v2 + tensor1_data = [ + Tropical(Inf), # (0,0) -> UNSAT + Tropical(0.0), # (0,1) -> SAT + Tropical(0.0), # (1,0) -> SAT + Tropical(0.0) # (1,1) -> SAT + ] + + # Tensor 2: v2 OR v3 + tensor2_data = [ + Tropical(Inf), # (0,0) -> UNSAT + Tropical(0.0), # (0,1) -> SAT + Tropical(0.0), # (1,0) -> SAT + Tropical(0.0) # (1,1) -> SAT + ] + + # Use setup_problem to create BipartiteGraph + static = setup_problem(3, [[1, 2], [2, 3]], [tensor1_data, tensor2_data]) + + # Create problem (all variables unfixed initially) + problem = TNProblem(static, verbose=false) + + # All variables should remain unfixed (multiple solutions possible) + @test problem.n_unfixed == 3 + + # Test with SingleTensorSolver on tensor 1 + solver = SingleTensorSolver() + table, variables = OptimalBranchingCore.branching_table(problem, solver, 1) + + @test !isempty(table.table) + @test length(variables) == 2 + @test variables == [1, 2] + + # Should have 3 valid configurations: (0,1), (1,0), (1,1) + @test length(table.table) == 1 + @test length(table.table[1]) == 3 + @test 0b01 in table.table[1] # v1=0, v2=1 + @test 0b10 in table.table[1] # v1=1, v2=0 + @test 0b11 in table.table[1] # v1=1, v2=1 + end + + @testset "SingleTensorSolver with fixed variables" begin + using TropicalNumbers + + # Create a problem with 3 variables and 2 tensors + # Tensor 1: v1 OR v2 + # Tensor 2: v2 OR v3 + tensor1_data = [ + Tropical(Inf), # (0,0) -> UNSAT + Tropical(0.0), # (0,1) -> SAT + Tropical(0.0), # (1,0) -> SAT + Tropical(0.0) # (1,1) -> SAT + ] + + tensor2_data = [ + Tropical(Inf), # (0,0) -> UNSAT + Tropical(0.0), # (0,1) -> SAT + Tropical(0.0), # (1,0) -> SAT + Tropical(0.0) # (1,1) -> SAT + ] + + static = setup_problem(3, [[1, 2], [2, 3]], [tensor1_data, tensor2_data]) + + # Manually fix v1 to 0 (without propagation) + doms = [DM_0, DM_BOTH, DM_BOTH] + problem = TNProblem(static, doms, 2, DynamicWorkspace(3, false)) + + solver = SingleTensorSolver() + table, variables = OptimalBranchingCore.branching_table(problem, solver, 1) + + # Tensor 1 has variables [1, 2], but v1 is fixed to 0 + @test length(variables) == 1 + @test variables == [2] + + # With v1=0, tensor 1 (v1 OR v2) requires v2=1 to be SAT + @test length(table.table) == 1 + @test length(table.table[1]) == 1 + @test table.table[1][1] == 0b1 # v2=1 + end + + @testset "SingleTensorSolver UNSAT case" begin + using TropicalNumbers + + # Create a tensor that's always UNSAT + tensor_data = [ + Tropical(Inf), # (0,0) -> UNSAT + Tropical(Inf), # (0,1) -> UNSAT + Tropical(Inf), # (1,0) -> UNSAT + Tropical(Inf) # (1,1) -> UNSAT + ] + + # Add a second tensor to prevent immediate UNSAT detection + tensor2_data = [ + Tropical(0.0), # (0,0) -> SAT + Tropical(0.0), # (0,1) -> SAT + Tropical(0.0), # (1,0) -> SAT + Tropical(0.0) # (1,1) -> SAT + ] + + static = setup_problem(3, [[1, 2], [2, 3]], [tensor_data, tensor2_data]) + + # Manually create problem without propagation + doms = [DM_BOTH, DM_BOTH, DM_BOTH] + problem = TNProblem(static, doms, 3, DynamicWorkspace(3, false)) + + solver = SingleTensorSolver() + table, variables = OptimalBranchingCore.branching_table(problem, solver, 1) + + # Tensor 1 is always UNSAT, should return empty table + @test isempty(table.table) + @test isempty(variables) + end +end diff --git a/test/stats.jl b/test/stats.jl deleted file mode 100644 index 409b71b..0000000 --- a/test/stats.jl +++ /dev/null @@ -1,92 +0,0 @@ -using Test -using BooleanInference -using BooleanInference: NumUnfixedVars - -@testset "BranchingStats detailed metrics" begin - stats = BranchingStats(true) - @test BooleanInference.needs_path_tracking(stats) - @test stats.avg_branching_factor == 0.0 - - record_branch!(stats, 3, 2) - record_branch!(stats, 2, 1) - - @test stats.total_branches == 2 - @test stats.total_subproblems == 5 - @test stats.max_depth == 2 - @test stats.avg_branching_factor ≈ 2.5 - - d = stats.detailed - @test d.branching_factors == [3, 2] - @test d.depth_distribution[3] == 1 - @test d.depth_distribution[2] == 1 - - record_propagation!(stats, 0.25) - record_propagation!(stats, 0.5) - @test d.propagation_calls == 2 - @test d.time_propagation ≈ 0.75 - - record_domain_reduction!(stats, 7) - record_early_unsat!(stats) - @test d.domain_reductions == 7 - @test d.early_unsat_detections == 1 - - record_branching_time!(stats, 0.1) - record_contraction_time!(stats, 0.2) - record_filtering_time!(stats, 0.3) - @test d.time_branching ≈ 0.1 - @test d.time_contraction ≈ 0.2 - @test d.time_filtering ≈ 0.3 - - record_cache_hit!(stats) - record_cache_hit!(stats) - record_cache_miss!(stats) - @test d.cache_hits == 2 - @test d.cache_misses == 1 - - record_variable_selection!(stats, 5, 10, 2) - record_variable_selection!(stats, 5, 6, 1) - record_variable_selection!(stats, 7, 4, 0) - @test d.variable_selection_counts[5] == 2 - @test d.variable_selection_counts[7] == 1 - @test d.remaining_vars_at_branch == [10, 6, 4] - @test d.depth_at_selection == [2, 1, 0] - @test d.variable_selection_sequence == [5, 5, 7] - - record_solved_leaf!(stats, 3, [1, 2, 3]) - @test !isempty(d.successful_paths) - @test d.successful_paths[1] == [1, 2, 3] - - record_unsat_leaf!(stats, 4) - @test stats.max_depth == 4 - - record_skipped_subproblem!(stats) - - buf = IOBuffer() - print_stats_summary(stats; io=buf) - summary_output = String(take!(buf)) - @test occursin("Branch decisions: 2", summary_output) - @test occursin("Successful paths", summary_output) - - copied = copy(stats) - @test copied !== stats - @test copied.detailed !== d - @test copied.detailed.successful_paths[1] == d.successful_paths[1] - copied.detailed.successful_paths[1][1] = 99 - @test d.successful_paths[1][1] == 1 - - reset!(stats) - @test stats.total_branches == 0 - @test stats.total_subproblems == 0 - @test stats.max_depth == 0 - @test stats.solved_leaves == 0 - @test stats.avg_branching_factor == 0.0 - @test isempty(d.branching_factors) - @test isempty(d.depth_distribution) - @test d.propagation_calls == 0 - @test d.time_propagation == 0.0 - @test isempty(d.variable_selection_counts) - @test isempty(d.successful_paths) - - plain_stats = BranchingStats() - @test !BooleanInference.needs_path_tracking(plain_stats) -end