diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl
index c60bfd2..203fca3 100644
--- a/src/ProblemReductions.jl
+++ b/src/ProblemReductions.jl
@@ -10,11 +10,11 @@ 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
-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
@@ -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/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/Circuit.jl b/src/models/Circuit.jl
index 517465a..7cec756 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,15 +50,28 @@ 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))...)
+        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
@@ -148,7 +166,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 +175,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 +203,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/models/Factoring.jl b/src/models/Factoring.jl
new file mode 100644
index 0000000..e15c1e4
--- /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 = BitStr(config[1:f.m]).buf
+    input2 = BitStr(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 1eec979..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
 
@@ -114,3 +123,4 @@ include("VertexCovering.jl")
 include("SetPacking.jl")
 include("DominatingSet.jl")
 include("QUBO.jl")
+include("Factoring.jl")
diff --git a/src/rules/factoring_sat.jl b/src/rules/factoring_sat.jl
new file mode 100644
index 0000000..8e503ee
--- /dev/null
+++ b/src/rules/factoring_sat.jl
@@ -0,0 +1,75 @@
+"""
+$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.input
+    p = [BooleanExpr(Symbol("p$i")) for i in 1:n1]
+    q = [BooleanExpr(Symbol("q$i")) for i in 1:n2]
+    m = BooleanExpr[]
+    others = BooleanExpr[]
+    exprs = Assignment[]
+    spres = BooleanExpr.(falses(n2+1))
+    for i in 1:n1
+        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], spres[j+1], cpre)
+            append!(exprs, mul_exprs)
+            cpre = c
+            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
+    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)
+    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.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/rules.jl b/src/rules/rules.jl
index f2127c6..37ef27b 100644
--- a/src/rules/rules.jl
+++ b/src/rules/rules.jl
@@ -70,4 +70,5 @@ include("sat_3sat.jl")
 include("spinglass_qubo.jl")
 include("sat_coloring.jl")
 include("vertexcovering_setcovering.jl")
+include("factoring_sat.jl")
 include("sat_independentset.jl")
diff --git a/src/rules/spinglass_sat.jl b/src/rules/spinglass_sat.jl
index 03588b7..2659f70 100644
--- a/src/rules/spinglass_sat.jl
+++ b/src/rules/spinglass_sat.jl
@@ -21,7 +21,7 @@ target_problem(res::ReductionCircuitToSpinGlass) = res.spinglass
 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/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/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
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
diff --git a/test/rules/factoring_sat.jl b/test/rules/factoring_sat.jl
new file mode 100644
index 0000000..d56ed49
--- /dev/null
+++ b/test/rules/factoring_sat.jl
@@ -0,0 +1,40 @@
+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())
+    @test length(best_configs) == 1
+    best_config = best_configs[1]
+    assignment = Dict(zip(res.circuit.symbols, best_config))
+    @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
+end
\ No newline at end of file
diff --git a/test/rules/rules.jl b/test/rules/rules.jl
index 7943734..50ded9f 100644
--- a/test/rules/rules.jl
+++ b/test/rules/rules.jl
@@ -15,10 +15,14 @@ end
 @testset "vertexcovering_setcovering" begin
     include("vertexcovering_setcovering.jl")
 end
+
 @testset "sat_coloring.jl" begin
     include("sat_coloring.jl")
 end
 
+@testset "factoring_sat.jl" begin
+    include("factoring_sat.jl")
+end
 @testset "sat_3sat" begin
     include("sat_3sat.jl")
 end
diff --git a/test/rules/vertexcovering_setcovering.jl b/test/rules/vertexcovering_setcovering.jl
index e5ff9ef..fd078e9 100644
--- a/test/rules/vertexcovering_setcovering.jl
+++ b/test/rules/vertexcovering_setcovering.jl
@@ -1,5 +1,6 @@
 using Test, ProblemReductions, Graphs
 using ProblemReductions: vertexcovering2setcovering
+
 @testset "VertexCoveing_SetCovering" begin
     g = SimpleGraph(4)
     add_edge!(g, 1, 2) # no.1
@@ -14,7 +15,7 @@ using ProblemReductions: vertexcovering2setcovering
     @test reduction_complexity(SetCovering, vc) == 1
     @test target_problem(reduceto(SetCovering, vc)) == reduceto(SetCovering, vc).setcovering
     @test sc == SetCovering([[1,2],[1,3],[2,3,4],[4]], [1, 3, 1, 4])
-    @test sort(edgelabel) == sort(Dict([2, 3] => 3, [1, 3] => 2, [1, 2] => 1, [3, 4] => 4)) # in lexicographic order
+    @test edgelabel == Dict([2, 3] => 3, [1, 3] => 2, [1, 2] => 1, [3, 4] => 4) # in lexicographic order
     @test findbest(sc, BruteForce()) == [[1,0,1,0]]
     @test findbest(vc, BruteForce()) == [[1,0,1,0]]
     @test findbest(vc, BruteForce()) == findbest(sc, BruteForce())