From 02454ea5fb647a2c8b8a18feab1e79a1edd759bc Mon Sep 17 00:00:00 2001
From: c-allergic <xli445614@gmail.com>
Date: Thu, 1 Aug 2024 15:53:53 +0800
Subject: [PATCH 01/10] Build up the framework

---
 examples/dining.jl | 43 ++++++++++++++++++++-----------------------
 1 file changed, 20 insertions(+), 23 deletions(-)

diff --git a/examples/dining.jl b/examples/dining.jl
index d52895e..df2bb0e 100644
--- a/examples/dining.jl
+++ b/examples/dining.jl
@@ -1,30 +1,27 @@
 # # Dining with Friends(developing yet)
-# ## Invite your friends to a dinner party
+# ---
+# ## Inviting friends to dinner > cracking a bank encryption system
+# Using this package, we could showcase the problem how inviting friends to a dinner party is harder than cracking a bank encryption system.Let's introduce some background knowledge
+# ### Intor to RSA 
+# RSA is a public-key cryptosystem. It's widely used in 
 
-# Suppose you are hosting a dinner party and you have invited your friends.
-# The relation between your friends is represented by a graph.
-# To create a graph, we use the `smallgraph` function from the `Graphs` package.
-using ProblemReductions, Graphs
-graph = smallgraph(:petersen)
+# ### Intro to factoring problem
+# The factoring problem is to find the prime factors of a composite number. It's a pratically hard problem. 
+# ### Reduction path from _Factoring_ to _MaxCut_
+# explain how I could use the ProblemReductions.jl to reduce the factoring problem to the MaxCut problem
 
-# We could make it into a maxcut problem, where each vertex stands for a person and the weight of edges 
-# stand for the unfriendly level between them.
-mc = MaxCut(graph,[3,2,4,2,1,-1,2,3,1,1,4,3,2,2,1])
-# Then we use LuxorGraphPlot to visualize the graph.
-# OK, since we wants to find the best partition for our friends, we should find the maximum cut of the graph.
-# Then, we could reduce it into a spinglass problem,where we want to find the spins configuration with the lowest energy.
+# ---
+# ## Factoring -> MaxCut
+using ProblemReductions, Graphs, LuxorGraphPlot
 
-# ## Inviting friends to a dinner is harder than cracking the encryption system
-# Intro to RSA encryption system
-# Intro to factoring problem
+# ### Create a factoring problem
 # Example: how to solve $x \times y = 6$, by reducing to spin-glass
 # arr = ProblemReductions.compose_multiplier(2, 2)
-# ProblemReductions.set_output!(arr, [0, 1, 1, 0])  # ? x ? == 6
-
-
-# NOTE: the first/second argument is the bit-width of the first/second input.
-# TODO: visualize the spin-galss
-# https://queracomputing.github.io/UnitDiskMapping.jl/notebooks/tutorial.html
-# https://github.com/GiggleLiu/LuxorGraphPlot.jl
-# https://arxiv.org/abs/2209.03965
+# ProblemReductions.set_output!(arr, [0, 1, 1, 0]) ->? x ? == 6
 
+# ### reduce the factoring to the circuit Sat problem
+# could I visualize this circuit Sat?
+# ### reduce the circuit Sat problem to the SpinGlass problem
+# Visualize this SpinGlass problem
+# ### reduce the SpinGlass problem to the MaxCut problem
+# Visualize this MaxCut problem and explain how the maxcut problem represents inviting friends to a dinner party

From c3181c02de932d4992919864a533ca4fd5a5e79a Mon Sep 17 00:00:00 2001
From: c-allergic <xli445614@gmail.com>
Date: Fri, 2 Aug 2024 15:09:21 +0800
Subject: [PATCH 02/10] save

---
 examples/dining.jl | 29 ++++++++++++++++++-----------
 1 file changed, 18 insertions(+), 11 deletions(-)

diff --git a/examples/dining.jl b/examples/dining.jl
index df2bb0e..e31d3f2 100644
--- a/examples/dining.jl
+++ b/examples/dining.jl
@@ -1,25 +1,32 @@
 # # Dining with Friends(developing yet)
 # ---
 # ## Inviting friends to dinner > cracking a bank encryption system
-# Using this package, we could showcase the problem how inviting friends to a dinner party is harder than cracking a bank encryption system.Let's introduce some background knowledge
+# Using this package, we could showcase the problem how inviting friends to a dinner party is harder than cracking a bank encryption system.Let's introduce some background knowledge.
+
 # ### Intor to RSA 
-# RSA is a public-key cryptosystem. It's widely used in 
+# RSA is a public-key cryptosystem. It's widely used in encryption algorithm that helps secure bank transactions and communications. 
+# Here's the Introduction->[RSA encryption](https://en.wikipedia.org/wiki/RSA_(cryptosystem)). Easily explained, there are public key $(n,e)$ and private key$(n,d)$. 
+# The attacker needs to factorize the $n$, a product of two large prime numbers. So the security of RSA comes from factoring problem.
+# ### Factoring problem
+# The factoring problem is to find the prime factors of a composite number. It's a pratically hard problem. Generally, the input size in RSA is 2048 bits.
+# Consider two algorithms to solve it: General number field sieve(GNFS, a good algorithm in factoring) and  Brute force. 
+
+# | Algorithm | Time complexity | Operations | Time ($10^{12}$ ops/s)  |
+# | :--- | :--- | :--- | :--- | 
+# | GNFS | $O(e^{(\log n)^{1/3}(\log \log n)^{2/3}})$ | $2^{112}$ | $≈ 7 \times 10^{20}$ years |
+# | Brute force | $O(\sqrt{n})$ | $2^{1024}$|$≈5.7 \times 10^{228}$ years |
+# Both are way longer than the age of our universe.
 
-# ### Intro to factoring problem
-# The factoring problem is to find the prime factors of a composite number. It's a pratically hard problem. 
-# ### Reduction path from _Factoring_ to _MaxCut_
-# explain how I could use the ProblemReductions.jl to reduce the factoring problem to the MaxCut problem
+# So basically, RSA relies on factoring and if we could reduce factoring to maxcut problem, we could show that inviting friends to a dinner party is harder than cracking a bank encryption system.  
+# Next part, I'll reduce factoring to the maxcut by: Factoring -> Circuit Sat -> SpinGlass -> MaxCut.
 
 # ---
 # ## Factoring -> MaxCut
 using ProblemReductions, Graphs, LuxorGraphPlot
-
+# For a given number $n$, we could create a factoring problem.
 # ### Create a factoring problem
-# Example: how to solve $x \times y = 6$, by reducing to spin-glass
-# arr = ProblemReductions.compose_multiplier(2, 2)
-# ProblemReductions.set_output!(arr, [0, 1, 1, 0]) ->? x ? == 6
-
 # ### reduce the factoring to the circuit Sat problem
+
 # could I visualize this circuit Sat?
 # ### reduce the circuit Sat problem to the SpinGlass problem
 # Visualize this SpinGlass problem

From 85a5ad95fdc7f3b539f4c4525099d30507499bd8 Mon Sep 17 00:00:00 2001
From: GiggleLiu <cacate0129@gmail.com>
Date: Tue, 6 Aug 2024 15:27:51 +0800
Subject: [PATCH 03/10] new factoring

---
 src/ProblemReductions.jl |  1 +
 src/models/Factoring.jl  | 19 +++++++++++++++++++
 src/models/models.jl     |  1 +
 test/models/Factoring.jl | 19 +++++++++++++++++++
 test/models/models.jl    |  4 ++++
 5 files changed, 44 insertions(+)
 create mode 100644 src/models/Factoring.jl
 create mode 100644 test/models/Factoring.jl

diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl
index 33a1ec2..3c2136f 100644
--- a/src/ProblemReductions.jl
+++ b/src/ProblemReductions.jl
@@ -25,6 +25,7 @@ export VertexCovering, is_vertex_covering, vertex_covering_energy
 export SetPacking, is_set_packing
 export DominatingSet
 export QUBO
+export Factoring
 
 # rules
 export target_problem, AbstractProblem, AbstractReductionResult, reduceto, extract_solution, reduction_complexity
diff --git a/src/models/Factoring.jl b/src/models/Factoring.jl
new file mode 100644
index 0000000..e85c9e2
--- /dev/null
+++ b/src/models/Factoring.jl
@@ -0,0 +1,19 @@
+struct Factoring <: AbstractProblem
+    m::Int       # number of bits for the first number
+    n::Int       # number of bits for the second number
+    input::Int   # the number to factorize
+end
+
+# variables interface
+variables(f::Factoring) = collect(1:f.m+f.n)
+flavors(::Type{Factoring}) = [0, 1]
+
+# utilities
+function evaluate(f::Factoring, config)
+    @assert length(config) == num_variables(f)
+    input1 = bit_literal(config[1:f.m]...).buf
+    input2 = bit_literal(config[f.m+1:f.m+f.n]...).buf
+    return input1 * input2 == f.input ? 0 : 1
+end
+
+pack_bits(bits) = sum(i->isone(bits[i]) ? 2^(i-1) : 0, 1:length(bits))
\ No newline at end of file
diff --git a/src/models/models.jl b/src/models/models.jl
index 7030596..ec55e50 100644
--- a/src/models/models.jl
+++ b/src/models/models.jl
@@ -89,3 +89,4 @@ include("VertexCovering.jl")
 include("SetPacking.jl")
 include("DominatingSet.jl")
 include("QUBO.jl")
+include("Factoring.jl")
diff --git a/test/models/Factoring.jl b/test/models/Factoring.jl
new file mode 100644
index 0000000..e969e7f
--- /dev/null
+++ b/test/models/Factoring.jl
@@ -0,0 +1,19 @@
+using Test, ProblemReductions, Graphs
+
+@testset "pack bits" begin
+    @test ProblemReductions.pack_bits([0, 1, 1]) == 6
+end
+
+@testset "factoring" begin
+    # construct a factoring problem
+    m = 2
+    n = 3
+    z = 15
+    f = Factoring(m, n, z)
+    @test variables(f) == [1, 2, 3, 4, 5]
+    @test flavors(Factoring) == [0, 1]
+    @test num_flavors(f) == 2
+    @test evaluate(f, [0, 1, 1, 1, 0]) == 1
+    @test evaluate(f, [1, 1, 1, 0, 1]) == 0
+    @test findbest(f, BruteForce()) == [[1, 1, 1, 0, 1]]
+end
\ No newline at end of file
diff --git a/test/models/models.jl b/test/models/models.jl
index 3c2e13e..bcf9eaf 100644
--- a/test/models/models.jl
+++ b/test/models/models.jl
@@ -42,4 +42,8 @@ end
 
 @testset "QUBO" begin
     include("QUBO.jl")
+end
+
+@testset "Factoring" begin
+    include("Factoring.jl")
 end
\ No newline at end of file

From 0e003e35909b9219280ca098c7847366994375f9 Mon Sep 17 00:00:00 2001
From: GiggleLiu <cacate0129@gmail.com>
Date: Tue, 6 Aug 2024 16:13:43 +0800
Subject: [PATCH 04/10] save

---
 src/rules/factoring_sat.jl  | 43 +++++++++++++++++++++++++++++++++++++
 src/rules/rules.jl          |  3 ++-
 test/rules/factoring_sat.jl |  5 +++++
 test/rules/rules.jl         |  4 ++++
 4 files changed, 54 insertions(+), 1 deletion(-)
 create mode 100644 src/rules/factoring_sat.jl
 create mode 100644 test/rules/factoring_sat.jl

diff --git a/src/rules/factoring_sat.jl b/src/rules/factoring_sat.jl
new file mode 100644
index 0000000..1285b06
--- /dev/null
+++ b/src/rules/factoring_sat.jl
@@ -0,0 +1,43 @@
+function reduceto(::Type{<:CircuitSAT}, f::Factoring)
+    # construct a circuit that multiplies two numbers
+    n1, n2, z = f.m, f.n, f.z
+    p = [BooleanExpr(Symbol("p$i")) for i in 1:n1]
+    q = [BooleanExpr(Symbol("q$i")) for i in 1:n2]
+    m = [BooleanExpr(Symbol("z$i")) for i in 1:n1+n2]
+    others = BooleanExpr[]
+    exprs = Assignment[]
+    s = [BooleanExpr(Symbol("s$i$j")) for i in 1:n1+1, j in 0:n2]
+    c = [BooleanExpr(Symbol("c$i$j")) for i in 0:n1, j in 1:n2]
+    # initialize s
+    for k = 1:size(s, 1)
+        push!(exprs, Assignment([s[k, 1]], BooleanExpr(:false)))
+    end
+    # initialize c
+    for k = 1:size(c, 2)
+        push!(exprs, Assignment([c[1, k]], BooleanExpr(:false)))
+    end
+    for i in 1:n1
+        for j in 1:n2
+            # s + 2c = p*q + s_pre + c_pre
+            mul_exprs, ancillas = multiplier(s[i, j+1], c[i+1, j], p[i], q[j], s[i+1, j], c[i, j])
+            append!(exprs, mul_exprs)
+            append!(others, ancillas)
+        end
+    end
+    return CircuitSAT(Circuit(exprs), vcat(pvars, qvars, outputs, vec(s), vec(c), others))
+end
+
+function multiplier(s::BooleanExpr, c::BooleanExpr, p::BooleanExpr, q::BooleanExpr, spre::BooleanExpr, cpre::BooleanExpr)
+    a = BooleanExpr(gensym("a"))
+    a_xor_s = BooleanExpr(gensym("a_xor_s"))
+    a_xor_s_and_c = BooleanExpr(gensym("a_xor_s_and_c"))
+    a_and_s = BooleanExpr(gensym("a_and_s"))
+    return [
+        Assignment([a], BooleanExpr(:and, [p, q])),
+        Assignment([a_xor_s], BooleanExpr(:xor, [a, spre])),
+        Assignment([s], BooleanExpr(:xor, [a_xor_s, cpre])),
+        Assignment([a_xor_s_and_c], BooleanExpr(:and, [a_xor_s, cpre])),
+        Assignment([a_and_s], BooleanExpr(:and, [a, spre])),
+        Assignment([c], BooleanExpr(:or, [a_xor_s_and_c, a_and_s]))
+    ], [a, a_xor_s, a_xor_s_and_c, a_and_s]
+end
\ No newline at end of file
diff --git a/src/rules/rules.jl b/src/rules/rules.jl
index 84fe6c3..a1e7b4a 100644
--- a/src/rules/rules.jl
+++ b/src/rules/rules.jl
@@ -49,4 +49,5 @@ function extract_solution end
 include("spinglass_sat.jl")
 include("spinglass_maxcut.jl")
 include("sat_coloring.jl")
-include("vertexcovering_setcovering.jl")
\ No newline at end of file
+include("vertexcovering_setcovering.jl")
+include("factoring_sat.jl")
\ No newline at end of file
diff --git a/test/rules/factoring_sat.jl b/test/rules/factoring_sat.jl
new file mode 100644
index 0000000..c7f96ed
--- /dev/null
+++ b/test/rules/factoring_sat.jl
@@ -0,0 +1,5 @@
+using Test, ProblemReductions
+
+
+@testset "multiplier" begin
+end
\ No newline at end of file
diff --git a/test/rules/rules.jl b/test/rules/rules.jl
index 55dd7a4..379ba34 100644
--- a/test/rules/rules.jl
+++ b/test/rules/rules.jl
@@ -14,6 +14,10 @@ end
     include("sat_coloring.jl")
 end
 
+@testset "factoring_sat.jl" begin
+    include("factoring_sat.jl")
+end
+
 @testset "rules" begin
     circuit = CircuitSAT(@circuit begin
         x = a ∨ ¬b

From d85227b92daf2ce3f32c1189ac2ed0f50d662a8c Mon Sep 17 00:00:00 2001
From: GiggleLiu <cacate0129@gmail.com>
Date: Tue, 6 Aug 2024 16:20:32 +0800
Subject: [PATCH 05/10] update

---
 src/rules/factoring_sat.jl | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/rules/factoring_sat.jl b/src/rules/factoring_sat.jl
index 1285b06..5b5a5a9 100644
--- a/src/rules/factoring_sat.jl
+++ b/src/rules/factoring_sat.jl
@@ -3,28 +3,28 @@ function reduceto(::Type{<:CircuitSAT}, f::Factoring)
     n1, n2, z = f.m, f.n, f.z
     p = [BooleanExpr(Symbol("p$i")) for i in 1:n1]
     q = [BooleanExpr(Symbol("q$i")) for i in 1:n2]
-    m = [BooleanExpr(Symbol("z$i")) for i in 1:n1+n2]
+    m = [BooleanExpr(Symbol("m$i")) for i in 1:n1+n2]
     others = BooleanExpr[]
     exprs = Assignment[]
-    s = [BooleanExpr(Symbol("s$i$j")) for i in 1:n1+1, j in 0:n2]
-    c = [BooleanExpr(Symbol("c$i$j")) for i in 0:n1, j in 1:n2]
-    # initialize s
-    for k = 1:size(s, 1)
-        push!(exprs, Assignment([s[k, 1]], BooleanExpr(:false)))
-    end
-    # initialize c
-    for k = 1:size(c, 2)
-        push!(exprs, Assignment([c[1, k]], BooleanExpr(:false)))
-    end
     for i in 1:n1
+        spres = BooleanExpr[]
+        cpre = BooleanExpr(:false)
         for j in 1:n2
+            # spre: the signal from the previous cycle
+            # cpre: the signal from the previous computational step
             # s + 2c = p*q + s_pre + c_pre
-            mul_exprs, ancillas = multiplier(s[i, j+1], c[i+1, j], p[i], q[j], s[i+1, j], c[i, j])
+            c = BooleanExpr(Symbol("c$i$j"))
+            s = BooleanExpr(Symbol("s$i$j"))
+            mul_exprs, ancillas = multiplier(s, c, p[i], q[j], j == n2 ? BooleanExpr(:false) : spres[j+1], cpre)
             append!(exprs, mul_exprs)
             append!(others, ancillas)
+            cpre = c
+            push!(spres, s)
+            push!(others, c)
+            push!(others, s)
         end
     end
-    return CircuitSAT(Circuit(exprs), vcat(pvars, qvars, outputs, vec(s), vec(c), others))
+    return CircuitSAT(Circuit(exprs), vcat(pvars, qvars, outputs, others))
 end
 
 function multiplier(s::BooleanExpr, c::BooleanExpr, p::BooleanExpr, q::BooleanExpr, spre::BooleanExpr, cpre::BooleanExpr)

From 6af0a258b8eb0de80a986726c4c1d4200473c8c7 Mon Sep 17 00:00:00 2001
From: c-allergic <xli445614@gmail.com>
Date: Wed, 7 Aug 2024 17:23:08 +0800
Subject: [PATCH 06/10] save

---
 src/ProblemReductions.jl    |  2 +-
 src/models/Circuit.jl       | 18 +++++++++--
 src/rules/factoring_sat.jl  | 60 ++++++++++++++++++++++++++++---------
 src/rules/spinglass_sat.jl  | 16 +++++++++-
 test/models/Circuit.jl      |  2 +-
 test/rules/factoring_sat.jl | 24 ++++++++++++++-
 6 files changed, 101 insertions(+), 21 deletions(-)

diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl
index 3c2136f..10897f2 100644
--- a/src/ProblemReductions.jl
+++ b/src/ProblemReductions.jl
@@ -14,7 +14,7 @@ export num_variables, num_flavors, variables, flavors, parameters, set_parameter
 export UnitWeight
 
 # models
-export BooleanExpr, Circuit, Assignment, ssa_form, CircuitSAT, @circuit, booleans, ¬, ∨, ∧, ⊻, is_literal, is_cnf, is_dnf
+export BooleanExpr, Circuit, Assignment, simple_form, CircuitSAT, @circuit, booleans, ¬, ∨, ∧, ⊻, is_literal, is_cnf, is_dnf
 export SpinGlass, spinglass_gadget
 export Coloring, coloring_energy, is_vertex_coloring
 export SetCovering, is_set_covering, set_covering_energy
diff --git a/src/models/Circuit.jl b/src/models/Circuit.jl
index 517465a..b2df95e 100644
--- a/src/models/Circuit.jl
+++ b/src/models/Circuit.jl
@@ -5,12 +5,17 @@ struct BooleanExpr
     function BooleanExpr(i::Symbol)
         new(:var, BooleanExpr[], i)
     end
+    function BooleanExpr(b::Bool)
+        new(:var, BooleanExpr[], b ? Symbol("true") : Symbol("false"))
+    end
     function BooleanExpr(head::Symbol, args::Vector{BooleanExpr})
+        @assert head != :var
         new(head, args)
     end
 end
 function extract_symbols!(ex::BooleanExpr, vars::Vector{Symbol})
     if ex.head == :var
+        (ex.var == Symbol("true") || ex.var == Symbol("false")) && return
         push!(vars, ex.var)
     else
         map(v->extract_symbols!(v, vars), ex.args)
@@ -45,7 +50,13 @@ function evaluate(ex::BooleanExpr, dict::Dict{BooleanExpr, Bool})
 end
 function evaluate(ex::BooleanExpr, dict::Dict{Symbol, Bool})
     if ex.head == :var
-        return dict[ex.var]
+        if ex.var == Symbol("true")
+            return true
+        elseif ex.var == Symbol("false")
+            return false
+        else
+            return dict[ex.var]
+        end
     else
         _eval(Val(ex.head), dict, evaluate.(ex.args, Ref(dict))...)
     end
@@ -148,7 +159,7 @@ function analyse_expr(bex)
     end
 end
 
-function ssa_form(c::Circuit)
+function simple_form(c::Circuit)
     new_exprs = Assignment[]
     for ex in c.exprs
         handle_assign!(new_exprs, ex)
@@ -157,6 +168,7 @@ function ssa_form(c::Circuit)
 end
 
 function handle_assign!(new_exprs, ex::Assignment)
+    ex.expr.head == :var && return push!(new_exprs, ex)
     newargs = map(ex.expr.args) do arg
         if arg.head == :var
             arg.var
@@ -184,7 +196,7 @@ struct CircuitSAT <: AbstractProblem
     symbols::Vector{Symbol}
 end
 function CircuitSAT(circuit::Circuit)
-    ssa = ssa_form(circuit)
+    ssa = simple_form(circuit)
     vars = symbols(ssa)
     CircuitSAT(ssa, vars)
 end
diff --git a/src/rules/factoring_sat.jl b/src/rules/factoring_sat.jl
index 5b5a5a9..8e503ee 100644
--- a/src/rules/factoring_sat.jl
+++ b/src/rules/factoring_sat.jl
@@ -1,30 +1,62 @@
+"""
+$TYPEDEF
+The reduction result of a  factoring problem to a CircuitSAT problem.
+
+### Fields
+- `circuit::CircuitSAT`: the CircuitSAT problem.
+- `p::Vector{Int}`: the first number to multiply (store bit locations)
+- `q::Vector{Int}`: the second number to multiply.
+- `m::Vector{Int}`: the result of the multiplication.
+"""
+struct ReductionFactoringToSat <: AbstractReductionResult
+    circuit::CircuitSAT
+    p::Vector{Int}
+    q::Vector{Int}
+    m::Vector{Int}
+end
+
+target_problem(res::ReductionFactoringToSat) = res.circuit
+
 function reduceto(::Type{<:CircuitSAT}, f::Factoring)
     # construct a circuit that multiplies two numbers
-    n1, n2, z = f.m, f.n, f.z
+    n1, n2, z = f.m, f.n, f.input
     p = [BooleanExpr(Symbol("p$i")) for i in 1:n1]
     q = [BooleanExpr(Symbol("q$i")) for i in 1:n2]
-    m = [BooleanExpr(Symbol("m$i")) for i in 1:n1+n2]
+    m = BooleanExpr[]
     others = BooleanExpr[]
     exprs = Assignment[]
+    spres = BooleanExpr.(falses(n2+1))
     for i in 1:n1
-        spres = BooleanExpr[]
-        cpre = BooleanExpr(:false)
+        cpre = BooleanExpr(false)
         for j in 1:n2
             # spre: the signal from the previous cycle
             # cpre: the signal from the previous computational step
             # s + 2c = p*q + s_pre + c_pre
             c = BooleanExpr(Symbol("c$i$j"))
             s = BooleanExpr(Symbol("s$i$j"))
-            mul_exprs, ancillas = multiplier(s, c, p[i], q[j], j == n2 ? BooleanExpr(:false) : spres[j+1], cpre)
+            mul_exprs, ancillas = multiplier(s, c, p[i], q[j], spres[j+1], cpre)
             append!(exprs, mul_exprs)
-            append!(others, ancillas)
             cpre = c
-            push!(spres, s)
+            spres[j] = s
             push!(others, c)
             push!(others, s)
+            append!(others, ancillas)
         end
+        spres[end] = cpre
+        push!(m, spres[1])
+    end
+    append!(m, spres[2:end])
+    # set the target integer
+    for i in 1:n1+n2
+        push!(exprs, Assignment([m[i].var], BooleanExpr(Bool(readbit(z, i)))))
     end
-    return CircuitSAT(Circuit(exprs), vcat(pvars, qvars, outputs, others))
+    sat = CircuitSAT(Circuit(exprs))
+    findvars(vars) = map(v->findfirst(==(v), sat.symbols), getfield.(vars, :var))
+    return ReductionFactoringToSat(sat, findvars(p), findvars(q), findvars(m))
+end
+
+function extract_solution(res::ReductionFactoringToSat, sol)
+    return vcat(sol[res.p], sol[res.q])
 end
 
 function multiplier(s::BooleanExpr, c::BooleanExpr, p::BooleanExpr, q::BooleanExpr, spre::BooleanExpr, cpre::BooleanExpr)
@@ -33,11 +65,11 @@ function multiplier(s::BooleanExpr, c::BooleanExpr, p::BooleanExpr, q::BooleanEx
     a_xor_s_and_c = BooleanExpr(gensym("a_xor_s_and_c"))
     a_and_s = BooleanExpr(gensym("a_and_s"))
     return [
-        Assignment([a], BooleanExpr(:and, [p, q])),
-        Assignment([a_xor_s], BooleanExpr(:xor, [a, spre])),
-        Assignment([s], BooleanExpr(:xor, [a_xor_s, cpre])),
-        Assignment([a_xor_s_and_c], BooleanExpr(:and, [a_xor_s, cpre])),
-        Assignment([a_and_s], BooleanExpr(:and, [a, spre])),
-        Assignment([c], BooleanExpr(:or, [a_xor_s_and_c, a_and_s]))
+        Assignment([a.var], BooleanExpr(:∧, [p, q])),    # a = p & q
+        Assignment([a_xor_s.var], BooleanExpr(:⊻, [a, spre])),  # a_xor_s = a ⊻ s_pre
+        Assignment([s.var], BooleanExpr(:⊻, [a_xor_s, cpre])),  # s = a_xor_s ⊻ c_pre
+        Assignment([a_xor_s_and_c.var], BooleanExpr(:∧, [a_xor_s, cpre])),  # a_xor_s_and_c = a_xor_s & c_pre
+        Assignment([a_and_s.var], BooleanExpr(:∧, [a, spre])),  # a_and_s = a & s_pre
+        Assignment([c.var], BooleanExpr(:∨, [a_xor_s_and_c, a_and_s]))  # c = a_xor_s_and_c | a_and_s
     ], [a, a_xor_s, a_xor_s_and_c, a_and_s]
 end
\ No newline at end of file
diff --git a/src/rules/spinglass_sat.jl b/src/rules/spinglass_sat.jl
index f08f490..9193e8f 100644
--- a/src/rules/spinglass_sat.jl
+++ b/src/rules/spinglass_sat.jl
@@ -21,7 +21,7 @@ function reduceto(::Type{<:SpinGlass}, sat::CircuitSAT)
 end
 
 function circuit2spinglass(c::Circuit)
-    ssa = ssa_form(c)
+    ssa = simple_form(c)
     all_variables = Symbol[]
     modules = []
     for assignment in ssa.exprs
@@ -106,6 +106,20 @@ function spinglass_gadget(::Val{:∨})
     LogicGadget(sg, [1, 2], [3])
 end
 
+function spinglass_gadget(::Val{:⊻})
+    g = SimpleGraph(4)
+    add_edge!(g, 1, 2)
+    add_edge!(g, 1, 3)
+    add_edge!(g, 2, 3)
+    add_edge!(g, 1, 4)
+    add_edge!(g, 2, 4)
+    add_edge!(g, 3, 4)
+    h = [1, 1, 1, 4]
+    J = [2,-2,-4,-2,-4,4]
+    sg = SpinGlass(g, J, h)
+    LogicGadget(sg, [1, 2], [3])
+end
+
 function expr_to_spinglass_gadget(expr::BooleanExpr)
     modules = []
     inputs = Symbol[]
diff --git a/test/models/Circuit.jl b/test/models/Circuit.jl
index 56c645a..dcf92ed 100644
--- a/test/models/Circuit.jl
+++ b/test/models/Circuit.jl
@@ -45,7 +45,7 @@ end
     end
     println(circuit)
     @test ProblemReductions.evaluate(circuit, Dict(:x => true, :y => false, :z => false)) == Dict(:x => true, :y => false, :z => false, :c => false, :d => true)
-    ssa = ProblemReductions.ssa_form(circuit)
+    ssa = ProblemReductions.simple_form(circuit)
     res = ProblemReductions.evaluate(ssa, Dict(:x => true, :y => false, :z => false))
     @test res[:x] && !res[:y] && !res[:z] && !res[:c] && res[:d]
 end
diff --git a/test/rules/factoring_sat.jl b/test/rules/factoring_sat.jl
index c7f96ed..75650f7 100644
--- a/test/rules/factoring_sat.jl
+++ b/test/rules/factoring_sat.jl
@@ -1,5 +1,27 @@
 using Test, ProblemReductions
 
-
 @testset "multiplier" begin
+    s, c, p, q, spre, cpre = BooleanExpr.([:s, :c, :p, :q, :spre, :cpre])
+    exprs, ancillas = ProblemReductions.multiplier(s, c, p, q, spre, cpre)
+    @test length(ancillas) == 4
+    @test length(exprs) == 6
+    circ = Circuit(exprs)
+    for p in [true, false], q in [true, false], spre in [true, false], cpre in [true, false]
+        assignment = Dict(:p => p, :q => q, :spre => spre, :cpre => cpre)
+        res = evaluate(circ, assignment)
+        @test res[:s] + 2 * res[:c] == (p * q) + spre + cpre
+    end
+end
+
+@testset "reduction" begin
+    fact = Factoring(1, 1, 1)
+    res = reduceto(CircuitSAT, fact)
+    best_configs = findbest(target_problem(res), BruteForce())
+    @show best_configs
+    @test length(best_configs) == 1
+    best_config = best_configs[1]
+    assignment = Dict(zip(res.circuit.symbols, best_config))
+    @show assignment
+    @show assignment[:p1], assignment[:q1]
+    @test assignment[:p1] * assignment[:q1] ==1
 end
\ No newline at end of file

From 8d3f13c2d66da48842fbeff11d73afcee9cf89ce Mon Sep 17 00:00:00 2001
From: c-allergic <xli445614@gmail.com>
Date: Thu, 8 Aug 2024 15:51:35 +0800
Subject: [PATCH 07/10] Add some test(a unit test TLE)

---
 test/rules/factoring_sat.jl | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/test/rules/factoring_sat.jl b/test/rules/factoring_sat.jl
index 75650f7..ed718df 100644
--- a/test/rules/factoring_sat.jl
+++ b/test/rules/factoring_sat.jl
@@ -17,11 +17,30 @@ end
     fact = Factoring(1, 1, 1)
     res = reduceto(CircuitSAT, fact)
     best_configs = findbest(target_problem(res), BruteForce())
-    @show best_configs
     @test length(best_configs) == 1
     best_config = best_configs[1]
     assignment = Dict(zip(res.circuit.symbols, best_config))
-    @show assignment
-    @show assignment[:p1], assignment[:q1]
     @test assignment[:p1] * assignment[:q1] ==1
+
+    fact2 = Factoring(2, 1, 2)
+    res2 = reduceto(CircuitSAT, fact2)
+    best_configs2 = findbest(target_problem(res2), BruteForce())
+    @test length(best_configs2) == 1
+    best_config2 = best_configs2[1]
+    assignment2 = Dict(zip(res2.circuit.symbols, best_config2))
+    @test (2* assignment2[:p2]+ assignment2[:p1]) * assignment2[:q1] == 2
+
+    fact3 = Factoring(2, 1, 3)
+    res3 = reduceto(CircuitSAT, fact3)
+    best_configs3 = findbest(target_problem(res3), BruteForce())
+    @test length(best_configs3) == 1
+    best_config3 = best_configs3[1]
+    assignment3 = Dict(zip(res3.circuit.symbols, best_config3))
+    @test (2* assignment3[:p2]+ assignment3[:p1]) * assignment3[:q1] == 3
+
+    # fact4 = Factoring(2, 2, 6)
+    # res4 = reduceto(CircuitSAT, fact4)
+    # best_configs4 = findbest(target_problem(res4), BruteForce()) <- this step is slow and we can't get the result ,stucked. maybe improve it
+    # @test length(best_configs4) == 2
+    
 end
\ No newline at end of file

From 5a30d187621f9bf6e3db41b061a8ec5f739ba258 Mon Sep 17 00:00:00 2001
From: c-allergic <xli445614@gmail.com>
Date: Tue, 13 Aug 2024 12:53:23 +0800
Subject: [PATCH 08/10] fix rules.jl

---
 test/rules/factoring_sat.jl | 6 ------
 test/rules/rules.jl         | 1 +
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/test/rules/factoring_sat.jl b/test/rules/factoring_sat.jl
index a6ca386..d56ed49 100644
--- a/test/rules/factoring_sat.jl
+++ b/test/rules/factoring_sat.jl
@@ -37,10 +37,4 @@ end
     best_config3 = best_configs3[1]
     assignment3 = Dict(zip(res3.circuit.symbols, best_config3))
     @test (2* assignment3[:p2]+ assignment3[:p1]) * assignment3[:q1] == 3
-
-    fact4 = Factoring(2, 2, 6)
-    res4 = reduceto(CircuitSAT, fact4)
-    best_configs4 = findbest(target_problem(res4), BruteForce()) 
-    @test length(best_configs4) == 2
-    
 end
\ No newline at end of file
diff --git a/test/rules/rules.jl b/test/rules/rules.jl
index 92bf2fd..79dc50a 100644
--- a/test/rules/rules.jl
+++ b/test/rules/rules.jl
@@ -21,6 +21,7 @@ end
 
 @testset "factoring_sat.jl" begin
     include("factoring_sat.jl")
+end
 @testset "sat_3sat" begin
     include("sat_3sat.jl")
 end

From 8d9bfec08358fcee638b8ea054c8e2e4c12bc3a0 Mon Sep 17 00:00:00 2001
From: GiggleLiu <cacate0129@gmail.com>
Date: Tue, 13 Aug 2024 12:55:34 +0800
Subject: [PATCH 09/10] add configuration space size

---
 src/ProblemReductions.jl      | 2 +-
 src/bruteforce.jl             | 2 +-
 src/models/models.jl          | 9 +++++++++
 test/models/IndependentSet.jl | 1 +
 4 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl
index 7f88ca9..203fca3 100644
--- a/src/ProblemReductions.jl
+++ b/src/ProblemReductions.jl
@@ -10,7 +10,7 @@ export @bit_str
 export TruthTable
 export HyperGraph, UnitDiskGraph, GridGraph, PlanarGraph, SimpleGraph
 export @bv_str, StaticElementVector, StaticBitVector, statictrues, staticfalses, onehotv
-export num_variables, num_flavors, variables, flavors, parameters, set_parameters, evaluate, parameter_type, problem_size
+export num_variables, num_flavors, variables, flavors, parameters, set_parameters, evaluate, parameter_type, problem_size, configuration_space_size
 export UnitWeight
 
 # models
diff --git a/src/bruteforce.jl b/src/bruteforce.jl
index df9c6ff..3d1e507 100644
--- a/src/bruteforce.jl
+++ b/src/bruteforce.jl
@@ -1,5 +1,5 @@
 """
-    BruteForce
+$TYPEDEF
 
 A brute force method to find the best configuration of a problem.
 """
diff --git a/src/models/models.jl b/src/models/models.jl
index 3bfbf8f..187bf4b 100644
--- a/src/models/models.jl
+++ b/src/models/models.jl
@@ -89,6 +89,15 @@ The lower the energy, the better the configuration.
 """
 function evaluate end
 
+"""
+$TYPEDSIGNATURES
+
+Return the log2 size of the configuration space of the problem.
+"""
+function configuration_space_size(problem::AbstractProblem)
+    return log2(num_flavors(problem)) * num_variables(problem)
+end
+
 """
     findbest(problem::AbstractProblem, method) -> Vector
 
diff --git a/test/models/IndependentSet.jl b/test/models/IndependentSet.jl
index 567cf41..d73472d 100644
--- a/test/models/IndependentSet.jl
+++ b/test/models/IndependentSet.jl
@@ -33,4 +33,5 @@ using Test, ProblemReductions, Graphs
 
     # test findbest function
     @test findbest(IS_01, BruteForce()) == [[1, 0, 0, 1], [0, 1, 0, 1]] # "1" is superior to "0"
+    @test configuration_space_size(IS_01) ≈ 4
 end
\ No newline at end of file

From 26bdeb9b452a39f890f5ef05bdfe5bc8fbf56894 Mon Sep 17 00:00:00 2001
From: GiggleLiu <cacate0129@gmail.com>
Date: Tue, 13 Aug 2024 13:22:11 +0800
Subject: [PATCH 10/10] speed up

---
 src/models/Circuit.jl | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/models/Circuit.jl b/src/models/Circuit.jl
index b2df95e..7cec756 100644
--- a/src/models/Circuit.jl
+++ b/src/models/Circuit.jl
@@ -58,13 +58,20 @@ function evaluate(ex::BooleanExpr, dict::Dict{Symbol, Bool})
             return dict[ex.var]
         end
     else
-        _eval(Val(ex.head), dict, evaluate.(ex.args, Ref(dict))...)
+        fmap = arg->evaluate(arg, dict)
+        if ex.head == :¬
+            return !evaluate(ex.args[1], dict)
+        elseif ex.head == :∨
+            return any(fmap, ex.args)
+        elseif ex.head == :∧
+            return all(fmap, ex.args)
+        elseif ex.head == :⊻
+            return mapreduce(fmap, xor, ex.args)
+        else
+            _eval(Val(ex.head), dict, evaluate.(ex.args, Ref(dict))...)
+        end
     end
 end
-_eval(::Val{:¬}, dict, x) = !x
-_eval(::Val{:∨}, dict, xs...) = any(xs)
-_eval(::Val{:∧}, dict, xs...) = all(xs)
-_eval(::Val{:⊻}, dict, xs...) = reduce(xor, xs)
 
 # --------- Assignment --------------
 struct Assignment