New Reduction: SAT to Circuit SAT (#89)

* New Reduction: SAT to Circuit SAT

* Fix typo

* Compactify and Fix typo

* Fix typo

* Fix tests

* FIx the test

* Delete with_complexity

* Delete the complexity test

src/ProblemReductions.jl

@@ -40,6 +40,7 @@ export findbest, BruteForce
 export CNF
 export ReductionSATToIndependentSet, ReductionSATToDominatingSet
 export ReductionIndependentSetToSetPacking
+export ReductionSATToCircuit
 
 # reduction path
 export ReductionGraph, reduction_graph, reduction_paths, implement_reduction_path, ConcatenatedReduction

src/rules/circuit_sat.jl

@@ -0,0 +1,71 @@
+"""
+$TYPEDEF
+
+The reduction result of an SAT problem o a Circuit SAT problem.
+
+### Fields
+- `target::CircuitSAT`: the target problem.
+$TYPEDFIELDS
+"""
+struct ReductionSATToCircuit{} <: AbstractReductionResult
+    target::CircuitSAT
+    sat_symbols::Vector{Symbol}
+end
+target_problem(res::ReductionSATToCircuit) = res.target
+
+function reduceto(::Type{<:CircuitSAT}, s::Satisfiability)
+    return ReductionSATToCircuit( cnf_to_circuit_sat(s.cnf), s.variables)
+end
+
+function clause_to_boolean_expr(clause::CNFClause{T}) where T
+    literal_exprs = map(var -> 
+        var.neg ? ¬( BooleanExpr(Symbol(var.name)) ) : BooleanExpr(Symbol(var.name)),
+        clause.vars
+    )
+    if length(literal_exprs) == 1
+        return literal_exprs[1]  
+    else
+        return BooleanExpr(:∨, literal_exprs)
+    end
+end
+
+function cnf_to_circuit_sat(cnf::CNF{T}) where T
+    exprs = Assignment[]  
+    clause_outputs = Symbol[] 
+    for clause in cnf.clauses
+        clause_output = gensym("clause")  
+        clause_expr = clause_to_boolean_expr(clause)  
+        push!(exprs, Assignment([clause_output], clause_expr))  
+        push!(clause_outputs, clause_output)  
+    end
+    final_output = gensym("out")  
+    push!(exprs, Assignment([final_output], BooleanExpr(:∧, map(var -> BooleanExpr(var), clause_outputs))))
+    circuit = Circuit(exprs)
+    return CircuitSAT(circuit)
+end
+
+function extract_solution(res::ReductionSATToCircuit, sol)
+    if sol[length(sol)] == false
+        return nothing
+    end
+    extract_sol = falses(length(res.sat_symbols))
+    for (i, var) in enumerate(res.sat_symbols)
+        extract_sol[i] = sol[findfirst(==(var), res.target.symbols)]
+    end
+    return extract_sol
+end
+
+function extract_multiple_solutions(res::ReductionSATToCircuit, sol_set)
+    all_assignments = Vector{Vector{Bool}}()
+    for sol_tmp in sol_set
+        if sol_tmp[length(sol_tmp)] == false
+            continue
+        end
+        assignment = falses(length(res.sat_symbols))
+        for (i, var) in enumerate(res.sat_symbols)
+            assignment[i] = sol_tmp[findfirst(==(var), res.target.symbols)]
+        end
+        push!(all_assignments, assignment)
+    end
+    return unique(filter(sol -> sol !== nothing, all_assignments))
+end

src/rules/rules.jl

@@ -76,3 +76,4 @@ include("factoring_sat.jl")
 include("sat_independentset.jl")
 include("sat_dominatingset.jl")
 include("independentset_setpacking.jl")
+include("circuit_sat.jl")

test/rules/circuit_sat.jl

@@ -0,0 +1,45 @@
+using Test, ProblemReductions
+
+@testset "circuit_sat" begin
+    function verify(sat)
+        reduction_results = reduceto(CircuitSAT, sat)
+        circuit_tmp = reduction_results.target
+        sol_circuit = findbest(circuit_tmp, BruteForce())
+        s1 = Set(findbest(sat, BruteForce()))
+        s2 = Set(unique(filter(sol -> sol !== nothing, extract_solution.(Ref(reduction_results), sol_circuit))))
+        s3 = Set(extract_multiple_solutions(reduction_results, sol_circuit))
+        return (s2 ⊆ s1) && (s3 == s1)
+    end
+
+    # Example 001: satisfiable 3-SAT
+    x1 = BoolVar(:x1, false)
+    nx1 = BoolVar(:x1, true)
+    x2 = BoolVar(:x2, false)
+    nx2 = BoolVar(:x2, true)
+    x3 = BoolVar(:x3, false)
+    nx3 = BoolVar(:x3, true)
+
+    clause1 = CNFClause([x1, nx2, x3])
+    clause2 = CNFClause([nx1, x2, nx3])
+    clause3 = CNFClause([x1, nx2, nx3])
+    clause4 = CNFClause([nx1, x2, x3])
+
+    clause_lst = [clause1, clause2, clause3, clause4]
+    sat01 = Satisfiability(CNF(clause_lst))
+
+    @test verify(sat01)
+
+    # Example 002: satisfiable 3-SAT
+    clause5 = CNFClause([nx1, x2, x3])
+    clause6 = CNFClause([x1, nx2, x3])
+    clause7 = CNFClause([x1, x2, nx3])
+    sat02 = Satisfiability(CNF([clause5, clause6, clause7]))
+    @test verify(sat02)
+
+    # Example 003: satisfiable 3-SAT
+    clause8 = CNFClause([x1, x2, x3])
+    clause9 = CNFClause([nx1, nx2, nx3])
+    sat03 = Satisfiability(CNF([clause8, clause9]))
+    @test verify(sat03)
+
+end

test/rules/rules.jl

@@ -39,6 +39,10 @@ end
     include("independentset_setpacking.jl")
 end
 
+@testset "circuit_sat" begin
+    include("circuit_sat.jl")
+end
+
 @testset "rules" begin
     circuit = CircuitSAT(@circuit begin
         x = a ∨ ¬b