diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 74d848da..d4385a2d 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -23,7 +23,7 @@ jobs:
       fail-fast: false
       matrix:
         version:
-          - '1.10'
+          - '1'
           - 'nightly'
         os:
           - ubuntu-latest
diff --git a/docs/src/index.md b/docs/src/index.md
index c9dfa8dc..14778b9b 100644
--- a/docs/src/index.md
+++ b/docs/src/index.md
@@ -51,21 +51,13 @@ A model problem is a subclass of [`AbstractProblem`](@ref) that defines the ener
 Facts affecting the computational complexity classification of the problem also include the topology of the problem and the domain of the variables.
 
 The required interfaces are:
-- [`variables`](@ref): The degrees of freedoms in the problem.
-    e.g. for the maximum independent set problems, they are the indices of vertices: 1, 2, 3...,
-    while for the max cut problem, they are the edges.
-- [`flavors`](@ref): A vector of integers as the flavors (or domain) of a degree of freedom.
-    e.g. for the maximum independent set problems, the flavors are [0, 1], where 0 means the vertex is not in the set and 1 means the vertex is in the set.
-- [`weights`](@ref): Energies associated with constraints.
-- [`energy`](@ref): Energy of a given configuration.
-- [`problem_size`](@ref): The size of the problem, which is the number of variables.
+- [`num_variables`](@ref): The number of variables in the problem, the variables are `1:num_variables`.
+- [`flavors`](@ref): A tuple of integers as the flavors (or domain) of a degree of freedom.
+    e.g. for the maximum independent set problems, the flavors are `(0, 1)`, where `0` means the vertex is not in the set and `1` means the vertex is in the set.
+- [`energy`](@ref): Energy of a given configuration, the smaller the better. If a configuration is invalid, the energy should be `Inf`.
 
 Optional functions include:
-- [`num_variables`](@ref): The number of variables in the problem.
-- [`num_flavors`](@ref): The number of flavors in the problem.
-- [`set_weights`](@ref): Change the weights for the `problem` and return a new problem instance.
-- [`weight_type`](@ref): The data type of weights.
-- [`findbest`](@ref): Find the best configurations in the computational problem.
+- [`problem_size`](@ref): The size of the problem, which is the number of variables.
 
 The following code lists all problems defined in ProblemReductions:
 ```@repl reduction_graph
@@ -97,7 +89,6 @@ A problem reduction rule is a function that reduces a problem to another problem
 
 Optional functions include:
 - [`extract_multiple_solutions`](@ref): Extract a set of solutions to the target problem back to the original problem. You may want to implement this when you want to make extracting multiple solutions faster.
-- [`reduce_size`](@ref): Infer the size of the target problem from the source problem size.
 
 The [`reduction_graph`](@ref) function returns the reduction graph of the problems that induced by the reduction rules defined in ProblemReductions:
 ```@repl reduction_graph
diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl
index 17c95be8..d249d368 100644
--- a/src/ProblemReductions.jl
+++ b/src/ProblemReductions.jl
@@ -11,18 +11,18 @@ 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, weights, set_weights, is_weighted, energy, weight_type, problem_size, configuration_space_size, constraints
+export num_variables, num_flavors, variables, flavors, weights, set_weights, is_weighted, energy, weight_type, problem_size, configuration_space_size
 export UnitWeight
 
 # models
 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
+export Coloring, is_vertex_coloring
+export SetCovering, is_set_covering
 export BoolVar, CNFClause, CNF, Satisfiability, is_kSAT, satisfiable, KSatisfiability
 export MaxCut
 export IndependentSet
-export VertexCovering, is_vertex_covering, vertex_covering_energy
+export VertexCovering, is_vertex_covering
 export SetPacking, is_set_packing
 export DominatingSet
 export QUBO
diff --git a/src/bruteforce.jl b/src/bruteforce.jl
index adcf597c..20f02121 100644
--- a/src/bruteforce.jl
+++ b/src/bruteforce.jl
@@ -6,17 +6,23 @@ A brute force method to find the best configuration of a problem.
 struct BruteForce end
 
 function findbest(problem::AbstractProblem, ::BruteForce; atol=eps(Float64), rtol=eps(Float64))
-    best_size = Inf
-    best_configs = Vector{Int}[]
-    configs = Iterators.product([flavors(problem) for i in 1:num_variables(problem)]...)
-    for (size, config) in energy_multi(problem, configs)
-        if isapprox(size, best_size; atol, rtol)
-            push!(best_configs, collect(config))
-        elseif size < best_size[1]
-            best_size = Float64(size)
-            empty!(best_configs)
-            push!(best_configs, collect(config))
+    flvs = flavors(problem)
+    best_ids = NTuple{num_variables(problem), Int}[]
+    configs = Iterators.product([1:length(flvs) for i in 1:num_variables(problem)]...)
+    energies = energy_eval_byid_multiple(problem, configs)
+    _findbest!(best_ids, configs, energies, atol, rtol)
+    return [collect(id_to_config(problem, id)) for id in best_ids]
+end
+
+function _findbest!(best_ids, configs, energies, atol, rtol)
+    best_energy = Inf
+    for (id, energy) in zip(configs, energies)
+        if isapprox(energy, best_energy; atol, rtol)
+            push!(best_ids, id)
+        elseif energy < best_energy
+            best_energy = energy
+            empty!(best_ids)
+            push!(best_ids, id)
         end
     end
-    return best_configs
 end
diff --git a/src/models/Circuit.jl b/src/models/Circuit.jl
index 363c9af9..d4022306 100644
--- a/src/models/Circuit.jl
+++ b/src/models/Circuit.jl
@@ -119,12 +119,6 @@ function print_statements(io::IO, exprs)
 end
 Base.show(io::IO, ::MIME"text/plain", x::Circuit) = show(io, x)
 
-function symbols(expr)
-    vars = Symbol[]
-    extract_symbols!(expr, vars)
-    return unique!(vars)
-end
-
 function extract_symbols!(c::Circuit, vars::Vector{Symbol})
     for ex in c.exprs
         extract_symbols!(ex, vars)
@@ -236,9 +230,7 @@ julia> sat.symbols
  :d
 
 julia> flavors(sat)
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(sat, [true, false, true, true, false, false, true])
 3
@@ -278,8 +270,8 @@ end
 Base.show(io::IO, ::MIME"text/plain", x::CircuitSAT) = show(io, x)
 
 # variables interface
-variables(c::CircuitSAT) = collect(1:length(c.symbols))
-flavors(::Type{<:CircuitSAT}) = [0, 1]
+num_variables(c::CircuitSAT) = length(c.symbols)
+flavors(::Type{<:CircuitSAT}) = (0, 1)
 problem_size(c::CircuitSAT) = (; num_exprs=length(c.circuit.exprs), num_variables=length(c.symbols))
 
 # weights interface
@@ -288,18 +280,24 @@ set_weights(c::CircuitSAT, weights) = CircuitSAT(c.circuit, weights, c.symbols)
 
 # constraints interface
 @nohard_constraints CircuitSAT
-function energy_terms(c::CircuitSAT)
+function soft_constraints(c::CircuitSAT)
     syms = symbols(c.circuit)
-    return [LocalConstraint([findfirst(==(s), c.symbols) for s in syms], syms=>expr) for expr in c.circuit.exprs]
+    return [SoftConstraint([findfirst(==(s), c.symbols) for s in syms], syms=>expr, w) for (w, expr) in zip(c.weights, c.circuit.exprs)]
 end
 
-function local_energy(::Type{<:CircuitSAT{T}}, spec::LocalConstraint, config) where {T}
+function local_energy(::Type{<:CircuitSAT{T}}, spec::SoftConstraint{WT}, config) where {T, WT}
     @assert length(config) == num_variables(spec)
     syms, ex = spec.specification
     dict = Dict(syms[i]=>Bool(c) for (i, c) in enumerate(config))
     for o in ex.outputs
         @assert haskey(dict, o) "The output variable `$o` is not in the configuration"
-        dict[o] != evaluate_expr(ex.expr, dict) && return 1  # this is the loss!
+        dict[o] != evaluate_expr(ex.expr, dict) && return spec.weight  # this is the loss!
     end
-    return 0
+    return zero(WT)
+end
+
+function symbols(expr::Union{Assignment, BooleanExpr, Circuit})
+    vars = Symbol[]
+    extract_symbols!(expr, vars)
+    return unique!(vars)
 end
\ No newline at end of file
diff --git a/src/models/Coloring.jl b/src/models/Coloring.jl
index 23552962..a983a1b5 100644
--- a/src/models/Coloring.jl
+++ b/src/models/Coloring.jl
@@ -22,23 +22,10 @@ julia> coloring = Coloring{3}(g)  # 3 colors
 Coloring{3, Int64, UnitWeight}(SimpleGraph{Int64}(15, [[2, 5, 6], [1, 3, 7], [2, 4, 8], [3, 5, 9], [1, 4, 10], [1, 8, 9], [2, 9, 10], [3, 6, 10], [4, 6, 7], [5, 7, 8]]), [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 
 julia> variables(coloring)
-10-element Vector{Int64}:
-  1
-  2
-  3
-  4
-  5
-  6
-  7
-  8
-  9
- 10
+1:10
 
 julia> flavors(coloring)
-3-element Vector{Int64}:
- 0
- 1
- 2
+(0, 1, 2)
 
 julia> is_vertex_coloring(coloring.graph,[1,2,3,1,3,2,1,2,3,1]) #random assignment
 false
@@ -56,8 +43,8 @@ Base.:(==)(a::Coloring, b::Coloring) = a.graph == b.graph && a.weights == b.weig
 problem_size(c::Coloring) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 
 # variables interface
-variables(gp::Coloring{K}) where K = collect(1:nv(gp.graph))
-flavors(::Type{<:Coloring{K}}) where K = collect(0:K-1) # colors
+num_variables(gp::Coloring{K}) where K = nv(gp.graph)
+flavors(::Type{<:Coloring{K}}) where K = ntuple(i->i-1, K) # colors
 num_flavors(::Type{<:Coloring{K}}) where K = K # number of colors
 
 # weights interface
@@ -66,15 +53,15 @@ set_weights(c::Coloring{K}, weights) where K = Coloring{K}(c.graph, weights)
 
 # constraints interface
 @nohard_constraints Coloring
-function energy_terms(c::Coloring)
+function soft_constraints(c::Coloring)
     # constraints on edges
-    return [LocalConstraint(_vec(e), :coloring) for e in edges(c.graph)]
+    return [SoftConstraint(_vec(e), :coloring, w) for (w, e) in zip(weights(c), edges(c.graph))]
 end
 
-function local_energy(::Type{<:Coloring{K, T}}, spec::LocalConstraint, config) where {K, T}
+function local_energy(::Type{<:Coloring{K, T}}, spec::SoftConstraint{WT}, config) where {K, T, WT}
     @assert length(config) == num_variables(spec)
     a, b = config
-    return a == b ? one(T) : zero(T)
+    return a == b ? spec.weight : zero(WT)
 end
 
 """
diff --git a/src/models/DominatingSet.jl b/src/models/DominatingSet.jl
index 9d026ef5..1b1019e1 100644
--- a/src/models/DominatingSet.jl
+++ b/src/models/DominatingSet.jl
@@ -25,17 +25,10 @@ julia> DS = DominatingSet(graph)
 DominatingSet{SimpleGraph{Int64}, Int64, UnitWeight}(SimpleGraph{Int64}(4, [[2], [1, 3], [2, 4], [3, 5], [4]]), [1, 1, 1, 1, 1])
 
 julia> variables(DS)  # degrees of freedom
-5-element Vector{Int64}:
- 1
- 2
- 3
- 4
- 5
+1:5
 
 julia> flavors(DS)  # flavors of the vertices
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(DS, [0, 1, 0, 1, 0]) # Positive sample: (size) of a dominating set
 2
@@ -60,8 +53,8 @@ end
 Base.:(==)(a::DominatingSet, b::DominatingSet) = ( a.graph == b.graph )
 
 # Variables Interface
-variables(gp::DominatingSet) = [1:nv(gp.graph)...]
-flavors(::Type{<:DominatingSet}) = [0, 1]
+num_variables(gp::DominatingSet) = nv(gp.graph)
+flavors(::Type{<:DominatingSet}) = (0, 1)
 problem_size(c::DominatingSet) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 
 # Weights Interface
@@ -69,14 +62,20 @@ weights(c::DominatingSet) = c.weights
 set_weights(c::DominatingSet, weights) = DominatingSet(c.graph, weights)
 
 # Constraints Interface
-@nohard_constraints DominatingSet
-function energy_terms(c::DominatingSet)
+function hard_constraints(c::DominatingSet)
+    return [HardConstraint(vcat(v, neighbors(c.graph, v)), :dominance) for v in vertices(c.graph)]
+end
+function is_satisfied(::Type{<:DominatingSet}, spec::HardConstraint, config)
+    @assert length(config) == num_variables(spec)
+    return count(isone, config) >= 1
+end
+
+function soft_constraints(c::DominatingSet)
     # constraints on vertex and its neighbours
-    return [LocalConstraint(vcat(v, neighbors(c.graph, v)), :dominating) for v in vertices(c.graph)]
+    return [SoftConstraint([v], :num_vertex, w) for (w, v) in zip(weights(c), vertices(c.graph))]
 end
 
-function local_energy(::Type{<:DominatingSet{GT, T}}, spec::LocalConstraint, config) where {GT, T}
-    @assert length(config) == num_variables(spec)
-    nselect = count(isone, config)
-    return nselect < 1 ? energy_max(T) : T(first(config))
+function local_energy(::Type{<:DominatingSet{GT, T}}, spec::SoftConstraint{WT}, config) where {GT, T, WT}
+    @assert length(config) == num_variables(spec) == 1
+    return WT(first(config)) * spec.weight
 end
diff --git a/src/models/Factoring.jl b/src/models/Factoring.jl
index ef9dd496..193b16be 100644
--- a/src/models/Factoring.jl
+++ b/src/models/Factoring.jl
@@ -19,16 +19,10 @@ julia> factoring = Factoring(2,2,6)
 Factoring(2, 2, 6)
 
 julia> variables(factoring) # return the sum of factors' bit size
-4-element Vector{Int64}:
- 1
- 2
- 3
- 4
+1:4
 
 julia> flavors(factoring)
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(factoring,[0,1,1,1]) # 01 -> 2, 11 -> 3
 0
@@ -41,17 +35,17 @@ struct Factoring <: AbstractProblem
 end
 
 # variables interface
-variables(f::Factoring) = collect(1:f.m+f.n)
-flavors(::Type{Factoring}) = [0, 1]
+num_variables(f::Factoring) = f.m+f.n
+flavors(::Type{Factoring}) = (0, 1)
 problem_size(f::Factoring) = (; num_bits_first=f.m, num_bits_second=f.n)
 
 # utilities
-function energy_multi(f::Factoring, configs)
-    @assert all(config->length(config) == num_variables(f), configs)
-    return Iterators.map(configs) do config
-        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, config)
+function energy_eval_byid_multiple(f::Factoring, config_ids)
+    @assert all(id->length(id) == num_variables(f), config_ids)
+    return Iterators.map(config_ids) do id
+        input1 = BitStr(id[1:f.m] .- 1).buf
+        input2 = BitStr(id[f.m+1:f.m+f.n] .- 1).buf
+        return (input1 * input2 == f.input ? 0 : 1)
     end
 end
 
diff --git a/src/models/IndependentSet.jl b/src/models/IndependentSet.jl
index bd4ccdc0..5c2e2b71 100644
--- a/src/models/IndependentSet.jl
+++ b/src/models/IndependentSet.jl
@@ -24,23 +24,17 @@ julia> graph = SimpleGraph(Graphs.SimpleEdge.([(1, 2), (1, 3), (3, 4), (2, 3)]))
 julia> IS = IndependentSet(graph)
 IndependentSet{SimpleGraph{Int64}, Int64, UnitWeight}(SimpleGraph{Int64}(4, [[2, 3], [1, 3], [1, 2, 4], [3]]), [1, 1, 1, 1])
 
-julia> variables(IS)  # degrees of freedom
-4-element Vector{Int64}:
- 1
- 2
- 3
- 4
+julia> num_variables(IS)  # degrees of freedom
+4
 
 julia> flavors(IS)  # flavors of the vertices
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(IS, [1, 0, 0, 1]) # Positive sample: -(size) of an independent set
 -2
 
 julia> energy(IS, [0, 1, 1, 0]) # Negative sample: 0
-3037000500
+3037000498
 
 julia> findbest(IS, BruteForce())  # solve the problem with brute force
 2-element Vector{Vector{Int64}}:
@@ -58,8 +52,8 @@ end
 Base.:(==)(a::IndependentSet, b::IndependentSet) = a.graph == b.graph && a.weights == b.weights
 
 # Variables Interface
-variables(gp::IndependentSet) = [1:nv(gp.graph)...]
-flavors(::Type{<:IndependentSet}) = [0, 1]
+num_variables(gp::IndependentSet) = nv(gp.graph)
+flavors(::Type{<:IndependentSet}) = (0, 1)
 problem_size(c::IndependentSet) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 
 # weights interface
@@ -68,18 +62,18 @@ set_weights(c::IndependentSet, weights) = IndependentSet(c.graph, weights)
 
 # constraints interface
 function hard_constraints(c::IndependentSet)
-    return [LocalConstraint(_vec(e), nothing) for e in edges(c.graph)]
+    return [HardConstraint(_vec(e), :independence) for e in edges(c.graph)]
 end
-function is_satisfied(::Type{<:IndependentSet}, spec::LocalConstraint, config)
+function is_satisfied(::Type{<:IndependentSet}, spec::HardConstraint, config)
     @assert length(config) == num_variables(spec)
     return count(!iszero, config) <= 1
 end
 
-function energy_terms(c::IndependentSet)
-    return [LocalConstraint([i], nothing) for i in 1:nv(c.graph)]
+function soft_constraints(c::IndependentSet)
+    return [SoftConstraint([i], :num_vertex, w) for (w, i) in zip(weights(c), 1:nv(c.graph))]
 end
 
-function local_energy(::Type{<:IndependentSet{GT, T}}, spec::LocalConstraint, config) where {GT, T}
+function local_energy(::Type{<:IndependentSet{GT, T}}, spec::SoftConstraint{WT}, config) where {GT, T, WT}
     @assert length(config) == num_variables(spec) == 1
-    return T(-first(config))
+    return WT(-first(config)) * spec.weight
 end
\ No newline at end of file
diff --git a/src/models/Matching.jl b/src/models/Matching.jl
index e6a608ba..64ff078b 100644
--- a/src/models/Matching.jl
+++ b/src/models/Matching.jl
@@ -18,8 +18,7 @@ struct Matching{T, WT<:AbstractVector{T}} <: ConstraintSatisfactionProblem{T}
 end
 Base.:(==)(a::Matching, b::Matching) = a.graph == b.graph && a.weights == b.weights
 
-flavors(::Type{<:Matching}) = [0, 1]
-variables(gp::Matching) = collect(1:ne(gp.graph))
+flavors(::Type{<:Matching}) = (0, 1)
 num_variables(gp::Matching) = ne(gp.graph)
 problem_size(c::Matching) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 
@@ -30,22 +29,22 @@ set_weights(c::Matching, weights) = Matching(c.graph, weights)
 # constraints interface
 function hard_constraints(c::Matching)
     # edges sharing a vertex cannot be both in the matching
-    return [LocalConstraint([i for (i, e) in enumerate(edges(c.graph)) if contains(e, v)], :noshare) for v in vertices(c.graph)]
+    return [HardConstraint([i for (i, e) in enumerate(edges(c.graph)) if contains(e, v)], :noshare) for v in vertices(c.graph)]
 end
 
-function is_satisfied(::Type{<:Matching}, spec::LocalConstraint, config)
+function is_satisfied(::Type{<:Matching}, spec::HardConstraint, config)
     @assert length(config) == num_variables(spec)
     return count(isone, config) <= 1
 end
 
-function energy_terms(c::Matching)
+function soft_constraints(c::Matching)
     # as many edges as possible
-    return [LocalConstraint([e], :edge) for e in variables(c)]
+    return [SoftConstraint([e], :num_edges, w) for (w, e) in zip(weights(c), variables(c))]
 end
 
-function local_energy(::Type{<:Matching{T}}, spec::LocalConstraint, config) where {T}
+function local_energy(::Type{<:Matching{T}}, spec::SoftConstraint{WT}, config) where {T, WT}
     @assert length(config) == num_variables(spec) == 1
-    return T(first(config))
+    return WT(first(config)) * spec.weight
 end
 
 """
diff --git a/src/models/MaxCut.jl b/src/models/MaxCut.jl
index c5312efb..b3dafe4a 100644
--- a/src/models/MaxCut.jl
+++ b/src/models/MaxCut.jl
@@ -28,9 +28,7 @@ julia> num_variables(maxcut) # return the number of vertices
 3
 
 julia> flavors(maxcut) # return the flavors of the vertices
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(maxcut, [0,1,0]) # return the energy of the configuration
 -4
@@ -52,9 +50,8 @@ end
 Base.:(==)(a::MaxCut, b::MaxCut) = a.graph == b.graph && a.weights == b.weights
 
 # varibles interface 
-variables(gp::MaxCut) = [1:nv(gp.graph)...]
 num_variables(gp::MaxCut) = nv(gp.graph)
-flavors(::Type{<:MaxCut}) = [0, 1] #choose it or not
+flavors(::Type{<:MaxCut}) = (0, 1) #choose it or not
 problem_size(c::MaxCut) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
                             
 # weights interface
@@ -62,13 +59,13 @@ weights(c::MaxCut) = c.weights
 set_weights(c::MaxCut, weights) = MaxCut(c.graph, weights)
 
 # constraints interface
-function energy_terms(c::MaxCut)
-    return [LocalConstraint(_vec(e), :cut) for e in edges(c.graph)]
+function soft_constraints(c::MaxCut)
+    return [SoftConstraint(_vec(e), :cut, w) for (w, e) in zip(weights(c), edges(c.graph))]
 end
-function local_energy(::Type{<:MaxCut{T}}, spec::LocalConstraint, config) where {T}
+function local_energy(::Type{<:MaxCut{T}}, spec::SoftConstraint{WT}, config) where {T, WT}
     @assert length(config) == num_variables(spec)
     a, b = config
-    return (a != b) ? -one(T) : zero(T)
+    return (a != b) ? -spec.weight : zero(WT)
 end
 @nohard_constraints MaxCut
 
diff --git a/src/models/MaximalIS.jl b/src/models/MaximalIS.jl
index 52d418e8..6a6c0fc6 100644
--- a/src/models/MaximalIS.jl
+++ b/src/models/MaximalIS.jl
@@ -23,20 +23,14 @@ julia> graph = SimpleGraph(Graphs.SimpleEdge.([(1, 2), (1, 3), (3, 4), (2, 3), (
 julia> problem = MaximalIS(graph)
 MaximalIS{Int64, UnitWeight}(SimpleGraph{Int64}(5, [[2, 3, 4], [1, 3], [1, 2, 4], [1, 3]]), [1, 1, 1, 1])
 
-julia> variables(problem)  # degrees of freedom
-4-element Vector{Int64}:
- 1
- 2
- 3
- 4
+julia> num_variables(problem)  # degrees of freedom
+4
 
 julia> flavors(problem)
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(problem, [0, 1, 0, 0])  # unlike the independent set, this configuration is not a valid solution
-3037000500
+3037000499
 
 julia> findbest(problem, BruteForce())
 1-element Vector{Vector{Int64}}:
@@ -54,9 +48,8 @@ end
 Base.:(==)(a::MaximalIS, b::MaximalIS) = a.graph == b.graph && a.weights == b.weights
 
 # variables interface
-variables(gp::MaximalIS) = [1:nv(gp.graph)...]
 num_variables(gp::MaximalIS) = nv(gp.graph)
-flavors(::Type{<:MaximalIS}) = [0, 1]
+flavors(::Type{<:MaximalIS}) = (0, 1)
 problem_size(c::MaximalIS) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 
 # weights interface
@@ -64,20 +57,20 @@ weights(c::MaximalIS) = c.weights
 set_weights(c::MaximalIS, weights) = MaximalIS(c.graph, weights)
 
 function hard_constraints(c::MaximalIS)
-    return [LocalConstraint(vcat(v, neighbors(c.graph, v)), :maximal_independent) for v in vertices(c.graph)]
+    return [HardConstraint(vcat(v, neighbors(c.graph, v)), :maximal_independence) for v in vertices(c.graph)]
 end
-function is_satisfied(::Type{<:MaximalIS}, spec::LocalConstraint, config)
+function is_satisfied(::Type{<:MaximalIS}, spec::HardConstraint, config)
     @assert length(config) == num_variables(spec)
     nselect = count(!iszero, config)
     return !(nselect == 0 || (nselect > 1 && !iszero(first(config))))
 end
 # constraints interface
-function energy_terms(c::MaximalIS)
-    return [LocalConstraint([v], :vertex) for v in vertices(c.graph)]
+function soft_constraints(c::MaximalIS)
+    return [SoftConstraint([v], :vertex, w) for (w, v) in zip(weights(c), vertices(c.graph))]
 end
-function local_energy(::Type{<:MaximalIS{T}}, spec::LocalConstraint, config) where {T}
+function local_energy(::Type{<:MaximalIS{T}}, spec::SoftConstraint{WT}, config) where {T, WT}
     @assert length(config) == num_variables(spec)
-    return T(-first(config))
+    return WT(-first(config)) * spec.weight
 end
 
 """
diff --git a/src/models/Paintshop.jl b/src/models/Paintshop.jl
index da07779c..55df91f0 100644
--- a/src/models/Paintshop.jl
+++ b/src/models/Paintshop.jl
@@ -20,16 +20,11 @@ julia> using ProblemReductions
 julia> problem = PaintShop(["a","b","a","c","c","b"])
 PaintShop{String}(["a", "b", "a", "c", "c", "b"], Bool[1, 1, 0, 1, 0, 0])
 
-julia> variables(problem)
-3-element Vector{String}:
- "a"
- "b"
- "c"
+julia> num_variables(problem)
+3
 
 julia> flavors(problem)
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(problem, [0, 1, 0])
 4
@@ -51,23 +46,24 @@ struct PaintShop{LT} <: ConstraintSatisfactionProblem{Int}
     end
 end
 
-variables(gp::PaintShop) = unique(gp.sequence)
-flavors(::Type{<:PaintShop}) = [0, 1]
+num_variables(gp::PaintShop) = length(gp.sequence) ÷ 2
+symbols(gp::PaintShop) = unique(gp.sequence)
+flavors(::Type{<:PaintShop}) = (0, 1)
 problem_size(c::PaintShop) = (; sequence_length=length(c.sequence))
 Base.:(==)(a::PaintShop, b::PaintShop) = a.sequence == b.sequence && a.isfirst == b.isfirst
 
 # constraints interface
-function energy_terms(c::PaintShop)
+function soft_constraints(c::PaintShop)
     # constraints on alphabets with the same color
-    vars = variables(c)
-    return [LocalConstraint([findfirst(==(c.sequence[i]), vars), findfirst(==(c.sequence[i+1]), vars)], (c.isfirst[i], c.isfirst[i+1])) for i=1:length(c.sequence)-1]
+    syms = symbols(c)
+    return [SoftConstraint([findfirst(==(c.sequence[i]), syms), findfirst(==(c.sequence[i+1]), syms)], (c.isfirst[i], c.isfirst[i+1]), 1) for i=1:length(c.sequence)-1]
 end
 
-function local_energy(::Type{<:PaintShop}, spec::LocalConstraint, config)
+function local_energy(::Type{<:PaintShop}, spec::SoftConstraint{WT}, config) where {WT}
     @assert length(config) == num_variables(spec)
     isfirst1, isfirst2 = spec.specification
     c1, c2 = config
-    return (c1 == c2) == (isfirst1 == isfirst2) ? 0 : 1
+    return (c1 == c2) == (isfirst1 == isfirst2) ? zero(WT) : spec.weight
 end
 
 @nohard_constraints PaintShop
@@ -80,7 +76,7 @@ The `config` is a sequence of 0 and 1, where 0 means painting the first appearen
 and 1 means painting the first appearence of a car in blue.
 """
 function paint_shop_coloring_from_config(p::PaintShop{LT}, config) where {LT}
-    d = Dict{LT,Bool}(zip(variables(p), config))
+    d = Dict{LT,Bool}(zip(symbols(p), config))
     return map(1:length(p.sequence)) do i
         p.isfirst[i] ? d[p.sequence[i]] : ~d[p.sequence[i]]
     end
diff --git a/src/models/QUBO.jl b/src/models/QUBO.jl
index c0220483..8586f872 100644
--- a/src/models/QUBO.jl
+++ b/src/models/QUBO.jl
@@ -30,22 +30,11 @@ julia> graph = SimpleGraph(3)
 julia> QUBO02 = QUBO(graph, Float64[], [1., 1., 1.])
 QUBO{Float64}([1.0 0.0 0.0; 0.0 1.0 0.0; 0.0 0.0 1.0])
 
-julia> variables(QUBO01)  # degrees of freedom
-3-element Vector{Int64}:
- 1
- 2
- 3
-
-julia> variables(QUBO02)
-3-element Vector{Int64}:
- 1
- 2
- 3
+julia> num_variables(QUBO01)  # degrees of freedom
+3
 
 julia> flavors(QUBO01)  # flavors of the vertices
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(QUBO01, [0, 1, 0])
 1.0
@@ -83,8 +72,8 @@ function QUBO(graph::SimpleGraph, edge_weights::Vector{T}, vertex_weights::Vecto
 end
 
 # variables interface
-variables(c::QUBO) = collect(1:size(c.matrix, 1))
-flavors(::Type{<:QUBO}) = [0, 1]
+num_variables(c::QUBO) = size(c.matrix, 1)
+flavors(::Type{<:QUBO}) = (0, 1)
 problem_size(c::QUBO) = (; num_variables=size(c.matrix, 1))
 
 function weights(c::QUBO)
@@ -95,19 +84,19 @@ function weights(c::QUBO)
 end
 
 # constraints interface
-function energy_terms(c::QUBO)
+function soft_constraints(c::QUBO)
     vcat(
-        [LocalConstraint([i, j], :offdiagonal) for i in variables(c), j in variables(c) if i < j && (c.matrix[i, j] != 0 || c.matrix[j, i] != 0)],
-        [LocalConstraint([i], :diagonal) for i in variables(c) if c.matrix[i, i] != 0]
+        [SoftConstraint([i, j], :offdiagonal, c.matrix[i, j] + c.matrix[j, i]) for i in variables(c), j in variables(c) if i < j && (c.matrix[i, j] != 0 || c.matrix[j, i] != 0)],
+        [SoftConstraint([i], :diagonal, c.matrix[i, i]) for i in variables(c) if c.matrix[i, i] != 0]
     )
 end
 @nohard_constraints QUBO
-function local_energy(::Type{<:QUBO}, spec::LocalConstraint, config)
+function local_energy(::Type{<:QUBO}, spec::SoftConstraint, config)
     @assert length(config) == num_variables(spec)
     if spec.specification == :offdiagonal
         a, b = config
-        return a * b
+        return a * b * spec.weight
     else
-        return first(config)
+        return first(config) * spec.weight
     end
 end
diff --git a/src/models/Satisfiability.jl b/src/models/Satisfiability.jl
index 62903a87..b5c0d0e7 100644
--- a/src/models/Satisfiability.jl
+++ b/src/models/Satisfiability.jl
@@ -28,7 +28,7 @@ function Base.show(io::IO, b::CNFClause)
 end
 Base.:(==)(x::CNFClause, y::CNFClause) = x.vars == y.vars
 Base.length(x::CNFClause) = length(x.vars)
-variables(clause::CNFClause) = unique([var.name for var in clause.vars])
+symbols(clause::CNFClause) = unique([var.name for var in clause.vars])
 
 """
     CNF{T}
@@ -93,7 +93,7 @@ macro bools(syms::Symbol...)
     esc(Expr(:block, [:($s = $BoolVar($(QuoteNode(s)))) for s in syms]..., nothing))
 end
 
-function variables(cnf::CNF{T}) where T
+function symbols(cnf::CNF{T}) where T
     unique([var.name for clause in cnf.clauses for var in clause.vars])
 end
 
@@ -141,23 +141,24 @@ Satisfiability{String, Int64, UnitWeight}(["x", "y", "z", "w"], [1, 1], (x ∨ y
 ```
 """
 struct Satisfiability{S, T, WT<:AbstractArray{T}} <:AbstractSatisfiabilityProblem{S, T}
-    variables::Vector{S}
+    symbols::Vector{S}
     weights::WT
     cnf::CNF{S}
-    function Satisfiability(variables::Vector{S}, cnf::CNF{S}, weights::WT) where {S, T, WT<:AbstractArray{T}}
+    function Satisfiability(symbols::Vector{S}, cnf::CNF{S}, weights::WT) where {S, T, WT<:AbstractArray{T}}
         @assert length(weights) == length(cnf.clauses) "length of weights must be equal to the number of clauses $(length(cnf.clauses)), got: $(length(weights))"
-        new{S, T, WT}(variables, weights, cnf)
+        new{S, T, WT}(symbols, weights, cnf)
     end
 end
 function Satisfiability(cnf::CNF{S}, weights::AbstractVector=UnitWeight(length(cnf.clauses))) where {S}
-    Satisfiability(variables(cnf), cnf, weights)
+    Satisfiability(symbols(cnf), cnf, weights)
 end
 clauses(c::Satisfiability) = c.cnf.clauses
-variables(c::Satisfiability) = c.variables
-Base.:(==)(x::Satisfiability, y::Satisfiability) = x.cnf == y.cnf && x.weights == y.weights && x.variables == y.variables
+num_variables(c::Satisfiability) = length(c.symbols)
+symbols(c::Satisfiability) = c.symbols
+Base.:(==)(x::Satisfiability, y::Satisfiability) = x.cnf == y.cnf && x.weights == y.weights && x.symbols == y.symbols
 
 weights(c::Satisfiability) = c.weights
-set_weights(c::Satisfiability, weights::AbstractVector) = Satisfiability(c.variables, c.cnf, weights)
+set_weights(c::Satisfiability, weights::AbstractVector) = Satisfiability(c.symbols, c.cnf, weights)
 
 """
 $TYPEDEF
@@ -165,45 +166,50 @@ $TYPEDEF
 The satisfiability problem for k-SAT, where the goal is to find an assignment that satisfies the CNF.
 
 ### Fields
-- `variables::Vector{T}`: The variables in the CNF.
+- `symbols::Vector{T}`: The symbols in the CNF.
 - `cnf::CNF{T}`: The CNF expression.
+- `weights`: the weights associated with clauses.
+- `allow_less::Bool`: whether to allow less than `k` literals in a clause.
 """
 struct KSatisfiability{K, S, T, WT<:AbstractArray{T}} <:AbstractSatisfiabilityProblem{S, T}
-    variables::Vector{S}
+    symbols::Vector{S}
     cnf::CNF{S}
     weights::WT
-    function KSatisfiability{K}(variables::Vector{S}, cnf::CNF{S}, weights::WT) where {K, S, T, WT<:AbstractVector{T}}
-        @assert is_kSAT(cnf, K) "The CNF is not a $K-SAT problem"
-        new{K, S, T, WT}(variables, cnf, weights)
+    allow_less::Bool
+    function KSatisfiability{K}(symbols::Vector{S}, cnf::CNF{S}, weights::WT, allow_less::Bool) where {K, S, T, WT<:AbstractVector{T}}
+        @assert is_kSAT(cnf, K; allow_less) "The CNF is not a $K-SAT problem"
+        new{K, S, T, WT}(symbols, cnf, weights, allow_less)
     end
 end
-function KSatisfiability{K}(cnf::CNF{S}, weights::WT=UnitWeight(length(cnf.clauses))) where {K, S, WT<:AbstractVector}
-    KSatisfiability{K}(variables(cnf), cnf, weights)
+function KSatisfiability{K}(cnf::CNF{S}, weights::WT=UnitWeight(length(cnf.clauses)); allow_less::Bool=false) where {K, S, WT<:AbstractVector}
+    KSatisfiability{K}(symbols(cnf), cnf, weights, allow_less)
 end
-Base.:(==)(x::KSatisfiability, y::KSatisfiability) = x.cnf == y.cnf
-is_kSAT(cnf::CNF, k::Int) = all(c -> k == length(c.vars), cnf.clauses)
+get_k(::Type{<:KSatisfiability{K}}) where K = K
+Base.:(==)(x::KSatisfiability, y::KSatisfiability) = x.cnf == y.cnf && x.weights == y.weights && x.allow_less == y.allow_less
+is_kSAT(cnf::CNF, k::Int; allow_less::Bool=false) = all(c -> k == length(c.vars) || (allow_less && k > length(c.vars)), cnf.clauses)
 clauses(c::KSatisfiability) = c.cnf.clauses
-variables(c::KSatisfiability) = c.variables
+num_variables(c::KSatisfiability) = length(c.symbols)
+symbols(c::KSatisfiability) = c.symbols
 
-problem_size(c::AbstractSatisfiabilityProblem) = (; num_claues = length(clauses(c)), num_variables = length(variables(c)))
-flavors(::Type{<:AbstractSatisfiabilityProblem}) = [0, 1]  # false, true
+problem_size(c::AbstractSatisfiabilityProblem) = (; num_claues = length(clauses(c)), num_variables = num_variables(c))
+flavors(::Type{<:AbstractSatisfiabilityProblem}) = (0, 1)  # false, true
 
 weights(c::KSatisfiability) = c.weights
-set_weights(c::KSatisfiability, weights::Vector{WT}) where {WT} = KSatisfiability(c.variables, c.cnf, weights)
+set_weights(c::KSatisfiability{K}, weights::AbstractVector{WT}) where {K, WT} = KSatisfiability{K}(c.symbols, c.cnf, weights, c.allow_less)
 
 # constraints interface
-function energy_terms(c::AbstractSatisfiabilityProblem)
-    vars = variables(c)
-    return map(clauses(c)) do cl
-        idx = [findfirst(==(v), vars) for v in variables(cl)]
-        LocalConstraint(idx, vars[idx] => cl)
+function soft_constraints(c::AbstractSatisfiabilityProblem)
+    vars = symbols(c)
+    return map(zip(clauses(c), weights(c))) do (cl, w)
+        idx = [findfirst(==(v), vars) for v in symbols(cl)]
+        SoftConstraint(idx, vars[idx] => cl, w)
     end
 end
-function local_energy(::Type{<:AbstractSatisfiabilityProblem{S, T}}, spec::LocalConstraint, config) where {S, T}
+function local_energy(::Type{<:AbstractSatisfiabilityProblem{S, T}}, spec::SoftConstraint{WT}, config) where {S, T, WT}
     @assert length(config) == num_variables(spec)
     vars, expr = spec.specification
     assignment = Dict(zip(vars, config))
-    return !satisfiable(expr, assignment) ? one(T) : zero(T)
+    return !satisfiable(expr, assignment) ? spec.weight : zero(WT)
 end
 
 @nohard_constraints AbstractSatisfiabilityProblem
diff --git a/src/models/SetCovering.jl b/src/models/SetCovering.jl
index d5be2f14..919c5754 100644
--- a/src/models/SetCovering.jl
+++ b/src/models/SetCovering.jl
@@ -31,17 +31,14 @@ julia> weights = [1, 2, 3]
 julia> setcovering = SetCovering(subsets, weights)
 SetCovering{Int64, Int64, Vector{Int64}}([1, 2, 3, 4], [[1, 2, 3], [2, 4], [1, 4]], [1, 2, 3])
 
-julia> variables(setcovering)  # degrees of freedom
-3-element Vector{Int64}:
- 1
- 2
- 3
+julia> num_variables(setcovering)  # degrees of freedom
+3
 
 julia> energy(setcovering, [1, 0, 1])  # cost of a configuration
 4
 
 julia> energy(setcovering, [0, 1, 1])
-3037000500
+3037000505
 
 julia> sc = set_weights(setcovering, [1, 2, 3])  # set the weights of the subsets
 SetCovering{Int64, Int64, Vector{Int64}}([1, 2, 3, 4], [[1, 2, 3], [2, 4], [1, 4]], [1, 2, 3])
@@ -65,8 +62,8 @@ Defined as the number of sets.
 problem_size(c::SetCovering) = (; num_sets=length(c.sets), num_elements=length(c.elements))
 
 # variables interface
-variables(gp::SetCovering) = [1:length(gp.sets)...]
-flavors(::Type{<:SetCovering}) = [0, 1] # whether the set is selected (1) or not (0)
+num_variables(gp::SetCovering) = length(gp.sets)
+flavors(::Type{<:SetCovering}) = (0, 1) # whether the set is selected (1) or not (0)
 
 # weights interface
 weights(c::SetCovering) = c.weights
@@ -74,19 +71,19 @@ set_weights(c::SetCovering, weights) = SetCovering(c.sets, weights)
 
 # constraints interface
 function hard_constraints(c::SetCovering)
-    return [LocalConstraint(findall(s->v in s, c.sets), :cover) for v in c.elements]
+    return [HardConstraint(findall(s->v in s, c.sets), :cover) for v in c.elements]
 end
-function is_satisfied(::Type{<:SetCovering{T}}, spec::LocalConstraint, config) where {T}
+function is_satisfied(::Type{<:SetCovering{T}}, spec::HardConstraint, config) where {T}
     @assert length(config) == num_variables(spec)
     return count(isone, config) > 0
 end
 
-function energy_terms(c::SetCovering)
-    return [LocalConstraint([i], :set) for i in variables(c)]
+function soft_constraints(c::SetCovering)
+    return [SoftConstraint([i], :set, w) for (i, w) in zip(variables(c), weights(c))]
 end
-function local_energy(::Type{<:SetCovering{ET, T}}, spec::LocalConstraint, config) where {ET, T}
+function local_energy(::Type{<:SetCovering{ET, T}}, spec::SoftConstraint{WT}, config) where {ET, T, WT}
     @assert length(config) == num_variables(spec)
-    return T(first(config))
+    return WT(first(config)) * spec.weight
 end
 
 """
diff --git a/src/models/SetPacking.jl b/src/models/SetPacking.jl
index 1955295f..7444f7ab 100644
--- a/src/models/SetPacking.jl
+++ b/src/models/SetPacking.jl
@@ -30,24 +30,17 @@ julia> sets = [[1, 2, 5], [1, 3], [2, 4], [3, 6], [2, 3, 6]]
 julia> SP = SetPacking(sets)
 SetPacking{Int64, Int64, UnitWeight}([1, 2, 5, 3, 4, 6], [[1, 2, 5], [1, 3], [2, 4], [3, 6], [2, 3, 6]], [1, 1, 1, 1, 1])
 
-julia> variables(SP)  # degrees of freedom
-5-element Vector{Int64}:
- 1
- 2
- 3
- 4
- 5
+julia> num_variables(SP)  # degrees of freedom
+5
 
 julia> flavors(SP)  # flavors of the subsets
-2-element Vector{Int64}:
- 0
- 1
+(0, 1)
 
 julia> energy(SP, [1, 0, 0, 1, 0]) # Positive sample: -(size) of a packing
 -2
 
 julia> energy(SP, [1, 0, 1, 1, 0]) # Negative sample: 0
-3037000500
+3037000497
 
 julia> findbest(SP, BruteForce())  # solve the problem with brute force
 3-element Vector{Vector{Int64}}:
@@ -69,8 +62,8 @@ Base.:(==)(a::SetPacking, b::SetPacking) = ( a.sets == b.sets && a.weights == b.
 problem_size(c::SetPacking) = (; num_elements = length(c.elements), num_sets = length(c.sets))
 
 # Variables Interface
-variables(c::SetPacking) = [1:length(c.sets)...]
-flavors(::Type{<:SetPacking}) = [0, 1]
+num_variables(c::SetPacking) = length(c.sets)
+flavors(::Type{<:SetPacking}) = (0, 1)
 
 weights(c::SetPacking) = c.weights
 set_weights(c::SetPacking, weights::Vector{T}) where {T} = SetPacking(c.sets, weights)
@@ -83,20 +76,20 @@ function hard_constraints(c::SetPacking)  # sets sharing the same element
             push!(get!(()->Int[], d, e), i)
         end
     end
-    return [LocalConstraint(v, :independent) for v in values(d)]
+    return [HardConstraint(v, :independence) for v in values(d)]
 end
-function is_satisfied(::Type{<:SetPacking}, spec::LocalConstraint, config)
+function is_satisfied(::Type{<:SetPacking}, spec::HardConstraint, config)
     @assert length(config) == num_variables(spec)
     return count(isone, config) <= 1
 end
 
-function energy_terms(c::SetPacking)  # sets sharing the same element
-    return [LocalConstraint([s], :set) for s in 1:length(c.sets)]
+function soft_constraints(c::SetPacking)  # sets sharing the same element
+    return [SoftConstraint([s], :set, w) for (w, s) in zip(weights(c), 1:length(c.sets))]
 end
 
-function local_energy(::Type{<:SetPacking}, spec::LocalConstraint, config)
+function local_energy(::Type{<:SetPacking}, spec::SoftConstraint{WT}, config) where {WT}
     @assert length(config) == num_variables(spec) == 1
-    return -first(config)
+    return WT(-first(config)) * spec.weight
 end
 
 """
diff --git a/src/models/SpinGlass.jl b/src/models/SpinGlass.jl
index 94a88bd4..bf9a82f4 100644
--- a/src/models/SpinGlass.jl
+++ b/src/models/SpinGlass.jl
@@ -47,17 +47,11 @@ julia> h = [1, -1, -1, 1]  # external field
 julia> spinglass = SpinGlass(graph, J, h)  # Define a spin glass problem
 SpinGlass{SimpleGraph{Int64}, Int64, Vector{Int64}}(SimpleGraph{Int64}(4, [[2, 3], [1, 3], [1, 2, 4], [3]]), [1, -1, 1, -1], [1, -1, -1, 1])
 
-julia> variables(spinglass)  # degrees of freedom
-4-element Vector{Int64}:
- 1
- 2
- 3
- 4
+julia> num_variables(spinglass)  # degrees of freedom
+4
 
 julia> flavors(spinglass)  # flavors of the spins
-2-element Vector{Int64}:
-  1
- -1
+(1, -1)
 
 julia> energy(spinglass, [-1, 1, 1, -1])  # energy of a configuration
 -2
@@ -85,8 +79,8 @@ function spin_glass_from_matrix(M::AbstractMatrix, h::AbstractVector)
 end
 
 # variables interface
-variables(gp::SpinGlass) = collect(1:nv(gp.graph))
-flavors(::Type{<:SpinGlass}) = [1, -1]
+num_variables(gp::SpinGlass) = nv(gp.graph)
+flavors(::Type{<:SpinGlass}) = (1, -1)
 problem_size(c::SpinGlass) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 
 # weights interface
@@ -94,12 +88,12 @@ weights(gp::SpinGlass) = vcat(gp.J, gp.h)
 set_weights(c::SpinGlass, weights) = SpinGlass(c.graph, weights[1:ne(c.graph)], weights[ne(c.graph)+1:end])
 
 # constraints interface
-function energy_terms(sg::SpinGlass)
-    return vcat([LocalConstraint(_vec(e), :edge) for e in edges(sg.graph)], [LocalConstraint([v], :vertex) for v in vertices(sg.graph)])
+function soft_constraints(sg::SpinGlass)
+    return vcat([SoftConstraint(_vec(e), :edge, w) for (w, e) in zip(sg.J, edges(sg.graph))], [SoftConstraint([v], :vertex, w) for (w, v) in zip(sg.h, vertices(sg.graph))])
 end
 @nohard_constraints SpinGlass
 
-function local_energy(::Type{<:SpinGlass}, spec::LocalConstraint, config)
+function local_energy(::Type{<:SpinGlass}, spec::SoftConstraint{WT}, config) where {WT}
     @assert length(config) == num_variables(spec)
-    spec.specification == :edge ? prod(config) : first(config)
+    return WT(spec.specification == :edge ? prod(config) : first(config)) * spec.weight
 end
diff --git a/src/models/VertexCovering.jl b/src/models/VertexCovering.jl
index a78eff6b..b1435873 100644
--- a/src/models/VertexCovering.jl
+++ b/src/models/VertexCovering.jl
@@ -29,18 +29,14 @@ julia> weights = [1, 3, 1, 4]
 julia> VC= VertexCovering(graph, weights)
 VertexCovering{Int64, Vector{Int64}}(SimpleGraph{Int64}(5, [[2, 3, 4], [1, 3], [1, 2, 4], [1, 3]]), [1, 3, 1, 4])
 
-julia> variables(VC)  # degrees of freedom
-4-element Vector{Int64}:
- 1
- 2
- 3
- 4
+julia> num_variables(VC)  # degrees of freedom
+4
 
 julia> energy(VC, [1, 0, 0, 1]) # Negative sample
-3037000500
+3037000505
 
 julia> energy(VC, [0, 1, 1, 0]) # Positive sample
-3037000500
+3037000504
 
 julia> findbest(VC, BruteForce())  # solve the problem with brute force
 1-element Vector{Vector{Int64}}:
@@ -61,9 +57,8 @@ end
 Base.:(==)(a::VertexCovering, b::VertexCovering) = a.graph == b.graph && a.weights == b.weights
 
 # variables interface
-variables(gp::VertexCovering) = collect(1:nv(gp.graph))
 num_variables(gp::VertexCovering) = nv(gp.graph)
-flavors(::Type{<:VertexCovering}) = [0, 1] # whether the vertex is selected (1) or not (0)
+flavors(::Type{<:VertexCovering}) = (0, 1) # whether the vertex is selected (1) or not (0)
 problem_size(c::VertexCovering) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 
 #weights interface 
@@ -72,18 +67,18 @@ set_weights(c::VertexCovering, weights) = VertexCovering(c.graph, weights)
 
 # constraints interface
 function hard_constraints(c::VertexCovering)
-    return [LocalConstraint(_vec(e), :cover) for e in edges(c.graph)]
+    return [HardConstraint(_vec(e), :cover) for e in edges(c.graph)]
 end
-function is_satisfied(::Type{<:VertexCovering}, spec::LocalConstraint, config)
+function is_satisfied(::Type{<:VertexCovering}, spec::HardConstraint, config)
     @assert length(config) == num_variables(spec)
     return any(!iszero, config)
 end
-function energy_terms(c::VertexCovering)
-    return [LocalConstraint([v], :vertex) for v in vertices(c.graph)]
+function soft_constraints(c::VertexCovering)
+    return [SoftConstraint([v], :vertex, w) for (w, v) in zip(weights(c), vertices(c.graph))]
 end
-function local_energy(::Type{<:VertexCovering{T}}, spec::LocalConstraint, config) where T
+function local_energy(::Type{<:VertexCovering{T}}, spec::SoftConstraint{WT}, config) where {T, WT}
     @assert length(config) == num_variables(spec)
-    return T(first(config))
+    return WT(first(config)) * spec.weight
 end
 
 """
diff --git a/src/models/models.jl b/src/models/models.jl
index 52fdc807..ac48c9df 100644
--- a/src/models/models.jl
+++ b/src/models/models.jl
@@ -22,26 +22,47 @@ abstract type AbstractProblem end
 The abstract base type of constraint satisfaction problems. `T` is the type of the local energy of the constraints.
 
 ### Required interfaces
-- [`energy_terms`](@ref), the specification of the energy terms, it is associated with weights.
 - [`hard_constraints`](@ref), the specification of the hard constraints. Once the hard constraints are violated, the energy goes to infinity.
+- [`is_satisfied`](@ref), check if the hard constraints are satisfied.
+
+- [`soft_constraints`](@ref), the specification of the energy terms as soft constraints, which is associated with weights.
 - [`local_energy`](@ref), the local energy for the constraints.
+- [`weights`](@ref): The weights of the soft constraints.
+- [`set_weights`](@ref): Change the weights for the `problem` and return a new problem instance.
 """
 abstract type ConstraintSatisfactionProblem{T} <: AbstractProblem end
 
 """
 $TYPEDEF
 
-The local constraint of the problem.
+A hard constraint on a [`ConstraintSatisfactionProblem`](@ref).
 
 ### Fields
 - `variables`: the indices of the variables involved in the constraint.
 - `specification`: the specification of the constraint.
 """
-struct LocalConstraint{ST}
+struct HardConstraint{ST}
     variables::Vector{Int}
     specification::ST
 end
-num_variables(spec::LocalConstraint) = length(spec.variables)
+num_variables(spec::HardConstraint) = length(spec.variables)
+
+"""
+$TYPEDEF
+
+A soft constraint on a [`ConstraintSatisfactionProblem`](@ref).
+
+### Fields
+- `variables`: the indices of the variables involved in the constraint.
+- `specification`: the specification of the constraint.
+- `weight`:  the weight of the constraint.
+"""
+struct SoftConstraint{WT, ST}
+    variables::Vector{Int}
+    specification::ST
+    weight::WT
+end
+num_variables(spec::SoftConstraint) = length(spec.variables)
 
 ######## Interfaces for computational problems ##########
 """
@@ -80,14 +101,14 @@ function problem_size end
 The degrees of freedoms in the computational problem. e.g. for the maximum independent set problems, they are the indices of vertices: 1, 2, 3...,
 while for the max cut problem, they are the edges.
 """
-function variables end
+variables(c::AbstractProblem) = 1:num_variables(c)
 
 """
     num_variables(problem::AbstractProblem) -> Int
 
 The number of variables in the computational problem.
 """
-num_variables(c::AbstractProblem) = length(variables(c))
+function num_variables end
 
 """
     weight_type(problem::AbstractProblem) -> Type
@@ -137,41 +158,74 @@ The lower the energy, the better the configuration.
 function energy end
 
 # energy interface
-energy(problem::AbstractProblem, config) = first(energy_multi(problem, [config]))[1]
-struct EnergyMultiConfig{T, PT<:ConstraintSatisfactionProblem{T}, ST, ST2, VT, WT <: AbstractVector{T}}
-    problem::PT
-    configs::VT  # iterator of configurations
-    hard_specs::Vector{LocalConstraint{ST}}
-    energy_terms::Vector{LocalConstraint{ST2}}
-    weights::WT
-end
-
-function energy_multi(problem::ConstraintSatisfactionProblem{T}, configs) where T
-    @assert all(config -> length(config) == num_variables(problem), configs) "All configurations must have the same length as the number of variables, got: $(length.(configs)), which should be $(num_variables(problem))"
-    hard_specs = hard_constraints(problem)
+energy(problem::AbstractProblem, config) = first(energy_eval_byid_multiple(problem, (config_to_id(problem, config),)))
+function energy_eval_byid_multiple(problem::ConstraintSatisfactionProblem{T}, ids) where T
     terms = energy_terms(problem)
-    ws = is_weighted(problem) ? weights(problem) : UnitWeight(length(terms))
-    return EnergyMultiConfig(problem, configs, hard_specs, terms, ws)
+    return Iterators.map(ids) do id
+        energy_eval_byid(terms, id)
+    end
+end
+function config_to_id(problem::AbstractProblem, config)
+    flvs = flavors(problem)
+    map(c -> findfirst(==(c), flvs), config)
+end
+function id_to_config(problem::AbstractProblem, id)
+    flvs = flavors(problem)
+    map(i -> flvs[i], id)
 end
 
-function Base.iterate(emc::EnergyMultiConfig{T}, args...) where T
-    config_spec = iterate(emc.configs, args...)
-    if config_spec === nothing
-        return nothing
+struct EnergyTerm{LT, N, F, T}
+    variables::Vector{LT}
+    flavors::NTuple{N, F}
+    strides::Vector{Int}
+    energies::Vector{T}
+end
+function Base.show(io::IO, term::EnergyTerm)
+    println(io, """EnergyTerm""")
+    entries = []
+    sizes = repeat([length(term.flavors)], length(term.variables))
+    for (idx, energy) in zip(CartesianIndices(Tuple(sizes)), term.energies)
+        push!(entries, [getindex.(Ref(term.flavors), idx.I)..., energy])
     end
-    config, state = config_spec
-    if !all(spec -> is_satisfied(typeof(emc.problem), spec, _get(config, spec.variables)), emc.hard_specs)
-        return (energy_max(T), config), state
+	pretty_table(io, transpose(hcat(entries...)); header=[string.(term.variables)..., "energy"])
+	return nothing
+end
+Base.show(io::IO, ::MIME"text/plain", term::EnergyTerm) = show(io, term)
+
+energy_terms(problem::ConstraintSatisfactionProblem{T}) where T = energy_terms(T, problem)
+function energy_terms(::Type{T}, problem::ConstraintSatisfactionProblem) where T
+    vars = variables(problem)
+    flvs = flavors(problem)
+    nflv = length(flvs)
+    terms = EnergyTerm{eltype(vars), length(flvs), eltype(flvs), T}[]
+    for constraint in hard_constraints(problem)
+        sizes = [nflv for _ in constraint.variables]
+        energies = map(CartesianIndices(Tuple(sizes))) do idx
+            is_satisfied(typeof(problem), constraint, getindex.(Ref(flvs), idx.I)) ? zero(T) : energy_max(T)
+        end
+        strides = [nflv^i for i in 0:length(constraint.variables)-1]
+        push!(terms, EnergyTerm(constraint.variables, flvs, strides, vec(energies)))
     end
-    energy = zero(T)
-    for (i, spec) in enumerate(emc.energy_terms)
-        subconfig = _get(config, spec.variables)
-        energy += local_energy(typeof(emc.problem), spec, subconfig) * emc.weights[i]
+    for (i, constraint) in enumerate(soft_constraints(problem))
+        sizes = [nflv for _ in constraint.variables]
+        energies = map(CartesianIndices(Tuple(sizes))) do idx
+            T(local_energy(typeof(problem), constraint, getindex.(Ref(flvs), idx.I)))
+        end
+        strides = [nflv^i for i in 0:length(constraint.variables)-1]
+        push!(terms, EnergyTerm(constraint.variables, flvs, strides, vec(energies)))
+    end
+    return terms
+end
+
+Base.@propagate_inbounds function energy_eval_byid(terms::AbstractVector{EnergyTerm{LT, N, F, T}}, config_id) where {LT, N, F, T}
+    sum(terms) do term
+        k = 1
+        for (stride, var) in zip(term.strides, term.variables)
+            k += stride * (config_id[var]-1)
+        end
+        term.energies[k]
     end
-    return (energy, config), state
 end
-_get(config::AbstractVector, indices) = view(config, indices)
-_get(config::Tuple, indices) = Iterators.map(i -> config[i], indices)
 
 """
 $TYPEDSIGNATURES
@@ -201,14 +255,14 @@ Base.getindex(::UnitWeight, i) = 1
 Base.size(w::UnitWeight) = (w.n,)
 
 """
-    energy_terms(problem::AbstractProblem) -> Vector{LocalConstraint}
+    soft_constraints(problem::AbstractProblem) -> Vector{SoftConstraint}
 
 The energy terms of the problem. Each term is associated with weights.
 """
-function energy_terms end
+function soft_constraints end
 
 """
-    hard_constraints(problem::AbstractProblem) -> Vector{LocalConstraint}
+    hard_constraints(problem::AbstractProblem) -> Vector{HardConstraint}
 
 The hard constraints of the problem. Once the hard constraints are violated, the energy goes to infinity.
 """
@@ -217,13 +271,20 @@ function hard_constraints end
 macro nohard_constraints(problem)
     esc(quote
         function $ProblemReductions.hard_constraints(problem::$(problem))
-            return LocalConstraint{Nothing}[]
+            return HardConstraint{Nothing}[]
         end
     end)
 end
 
 """
-    local_energy(::Type{<:ConstraintSatisfactionProblem{T}}, constraint::LocalConstraint, config) -> T
+    is_satisfied(::Type{<:ConstraintSatisfactionProblem}, constraint::HardConstraint, config) -> Bool
+
+Check if the `constraint` is satisfied by the configuration `config`.
+"""
+function is_satisfied end
+
+"""
+    local_energy(::Type{<:ConstraintSatisfactionProblem{T}}, constraint::SoftConstraint, config) -> T
 
 The local energy of the `constraint` given the configuration `config`.
 """
diff --git a/src/reduction_path.jl b/src/reduction_path.jl
index 6bbc7bc5..7935165f 100644
--- a/src/reduction_path.jl
+++ b/src/reduction_path.jl
@@ -93,7 +93,13 @@ identity_reduction(::Type{<:AbstractProblem}, source) = IdentityReductionResult(
 Returns a [`ReductionGraph`](@ref) instance from the reduction rules defined with method `reduceto`.
 """
 function reduction_graph()
-    ms = filter(m->m.sig.types[2] <: Type{<:AbstractProblem}, methods(reduceto))
+    ms = filter(methods(reduceto)) do m
+        if !hasproperty(m.sig, :types)
+            @warn "Illegal type signature as the first argument of `reduceto`, got $(m.sig). Note the `where` syntax is not supported yet. Skip this method."
+            return false
+        end
+        m.sig.types[2] <: Type{<:AbstractProblem}
+    end
     rules = extract_types.(getfield.(ms, :sig))
     nodes = unique!(vcat(concrete_subtypes(AbstractProblem), first.(rules), last.(rules)))
     graph = SimpleDiGraph(length(nodes))
diff --git a/src/rules/circuit_sat.jl b/src/rules/circuit_sat.jl
index 9f6ee7aa..9c669252 100644
--- a/src/rules/circuit_sat.jl
+++ b/src/rules/circuit_sat.jl
@@ -14,7 +14,7 @@ end
 target_problem(res::ReductionSATToCircuit) = res.target
 
 function reduceto(::Type{<:CircuitSAT}, s::Satisfiability)
-    return ReductionSATToCircuit( cnf_to_circuit_sat(s.cnf), s.variables)
+    return ReductionSATToCircuit( cnf_to_circuit_sat(s.cnf), s.symbols)
 end
 
 function clause_to_boolean_expr(clause::CNFClause{T}) where T
diff --git a/src/rules/sat_3sat.jl b/src/rules/sat_3sat.jl
index def50577..2cc18975 100644
--- a/src/rules/sat_3sat.jl
+++ b/src/rules/sat_3sat.jl
@@ -1,144 +1,55 @@
 """
 The reduction result of a general SAT problem to a 3-SAT problem.
-
-### Fields
-- `sat_source::Satisfiability{GT, T}`: the source general SAT problem.
 """
-struct ReductionSATTo3SAT{T} <: AbstractReductionResult
+struct ReductionSATToKSAT{K, T} <: AbstractReductionResult
     sat_source::Satisfiability{T}
-    sat_target::KSatisfiability{3, T}
-    new_var_map::Dict{Symbol, Symbol}
-    inverse_new_var_map::Dict{Symbol, Symbol}
-end
-target_problem(res::ReductionSATTo3SAT) = res.sat_target
-
-function reduceto(::Type{<:KSatisfiability}, sat_source::Satisfiability)
-    sat_source_renamed, new_var_map, inverse_new_var_map = rename_variables(sat_source)
-    sat_target = transform_to_3_literal_cnf(sat_source_renamed)
-    return ReductionSATTo3SAT(sat_source, sat_target, new_var_map, inverse_new_var_map )
-end
-
-function extract_solution(res::ReductionSATTo3SAT, sol)
-    num_source_vars = num_variables(res.sat_source)
-    target_vars = variables( res.sat_target )
-
-    @assert length(sol) == length(target_vars)
-    original_solution = fill(-1, num_source_vars) 
-    for (i, new_var) in enumerate(target_vars)
-        new_var_str = string(new_var)
-        if startswith(new_var_str, "x_")
-            original_index = parse(Int, new_var_str[3:end])
-            original_solution[original_index] = sol[i]
-        end
-    end
-
-    return original_solution
-end
-
-function extract_multiple_solutions(res::ReductionSATTo3SAT, sol_set)
-    num_source_vars = num_variables(res.sat_source)
-    target_vars = variables( res.sat_target )
-
-    @assert length(sol_set[1]) == length(target_vars)
-    all_original_solutions = Vector{Vector{Int64}}()
-    for sol_tmp in sol_set
-        original_solution = fill(-1, num_source_vars) 
-        for (i, new_var) in enumerate(target_vars)
-            new_var_str = string(new_var)
-            if startswith(new_var_str, "x_")
-                original_index = parse(Int, new_var_str[3:end])
-                original_solution[original_index] = sol_tmp[i]
-            end
-        end
-        push!(all_original_solutions, original_solution)
-    end
-
-    return unique( all_original_solutions )
+    sat_target::KSatisfiability{K, T}
 end
+target_problem(res::ReductionSATToKSAT) = res.sat_target
 
-# ----Useful functions----
-# 001: Function to rename variables in the CNF
-function rename_variables(sat::Satisfiability)
-    
-    original_vars = variables(sat)
-    
-    new_var_map = Dict{Symbol, Symbol}()
-    inverse_new_var_map = Dict{Symbol, Symbol}()
-
-    for (i, var_name) in enumerate(original_vars)
-        new_var_map[var_name] = Symbol("x_$(i)")
-        inverse_new_var_map[Symbol("x_$(i)")] = var_name
+function reduceto(target_type::Type{<:KSatisfiability}, sat_source::Satisfiability; allow_less::Bool=false)
+    K = get_k(target_type)
+    cnf = CNF(CNFClause{Symbol}[])
+    for clause in sat_source.cnf.clauses
+        add_clause!(K, cnf, clause; allow_less)
     end
-    
-    renamed_clauses = [
-        CNFClause([BoolVar(new_var_map[var.name], var.neg) for var in clause.vars])
-        for clause in sat.cnf.clauses
-    ]
-    
-    new_cnf = CNF(renamed_clauses)
-    
-    return Satisfiability(new_cnf), new_var_map, inverse_new_var_map
+    return ReductionSATToKSAT(sat_source, KSatisfiability{K}(cnf; allow_less))
 end
 
-# 002: Function to generate unique dummy variables
-function generate_dummy_var(dummy_var_counter::Int)
-    dummy_var_counter += 1
-    return BoolVar(Symbol("z_$(dummy_var_counter)"), false), dummy_var_counter
+function extract_solution(res::ReductionSATToKSAT, sol)
+    symbols_source = symbols(res.sat_source)
+    symbols_target = symbols(res.sat_target)
+    @assert length(sol) == length(symbols_target)
+    d = Dict(zip(symbols_target, sol))
+    return [d[s] for s in symbols_source]
 end
 
-# 003: Transform an arbitrary-length clause to 3-literal CNF
-function transform_to_3_literal_clause(literals::Vector{BoolVar{Symbol}}, dummy_var_counter::Int)
-    n = length(literals)
-    transformed_clauses = Vector{CNFClause{Symbol}}() 
-
-    if n == 1
-        
-        z1, dummy_var_counter = generate_dummy_var(dummy_var_counter)
-        z2, dummy_var_counter = generate_dummy_var(dummy_var_counter)
-        push!(transformed_clauses, CNFClause([literals[1], z1, z2]))
-        push!(transformed_clauses, CNFClause([literals[1], BoolVar(z1.name, true), z2]))
-        push!(transformed_clauses, CNFClause([literals[1], z1, BoolVar(z2.name, true)]))
-        push!(transformed_clauses, CNFClause([literals[1], BoolVar(z1.name, true), BoolVar(z2.name, true)]))
-        
-    elseif n == 2
-       
-        z1, dummy_var_counter = generate_dummy_var(dummy_var_counter)
-        push!(transformed_clauses, CNFClause([literals[1], literals[2], z1]))
-        push!(transformed_clauses, CNFClause([literals[1], literals[2], BoolVar(z1.name, true)]))
-    
-    elseif n == 3
-        
-        push!(transformed_clauses, CNFClause([literals[1], literals[2], literals[3]]))
-
+function add_clause!(K::Int, cnf::CNF, clause::CNFClause; allow_less::Bool)
+    if length(clause.vars) == K
+        push!(cnf.clauses, clause)
+    elseif length(clause.vars) < K
+        if allow_less
+            push!(cnf.clauses, clause)
+        else
+            anc = gensym("ancilla")
+            trueliteral, falseliteral = BoolVar(anc, false), BoolVar(anc, true)
+            add_clause!(K, cnf, CNFClause([clause.vars..., trueliteral]); allow_less)
+            add_clause!(K, cnf, CNFClause([clause.vars..., falseliteral]); allow_less)
+        end
     else
-        
-        z1, dummy_var_counter = generate_dummy_var(dummy_var_counter)
-        push!(transformed_clauses, CNFClause([literals[1], literals[2], z1]))
-
-        for i in 3:n-2
-            z_next, dummy_var_counter = generate_dummy_var(dummy_var_counter)
-            push!(transformed_clauses, CNFClause([literals[i], BoolVar(z1.name, true), z_next]))
-            z1 = z_next
+        clauses = cut_or_clause(K, clause)
+        for c in clauses
+            add_clause!(K, cnf, c; allow_less)
         end
-
-        push!(transformed_clauses, CNFClause([literals[n-1], literals[n], BoolVar(z1.name, true)]))
     end
-
-    return transformed_clauses, dummy_var_counter
 end
-
-# 004: Function to transform CNF to 3-literal CNF
-function transform_to_3_literal_cnf(sat::Satisfiability)
-    transformed_clauses = Vector{CNFClause{Symbol}}() 
-    dummy_var_counter = 0 
-
-    for clause in sat.cnf.clauses
-
-        transformed, dummy_var_counter = transform_to_3_literal_clause(clause.vars, dummy_var_counter)
-        transformed_clauses = vcat(transformed_clauses, transformed)
-    end
-    
-    return KSatisfiability{3}(CNF(transformed_clauses))
+# cut the clause into k-or-less-literal clauses
+function cut_or_clause(k::Int, clause::CNFClause)
+    @assert k >= 3
+    length(clause.vars) <= k && return [clause]
+    anc = gensym("ancilla")
+    c1 = CNFClause([clause.vars[1:k-1]..., BoolVar(anc, false)])
+    return [c1, cut_or_clause(k, CNFClause([clause.vars[k:end]..., BoolVar(anc, true)]))...]
 end
 
 # ----KSatisfiability to General Satisfiability----
diff --git a/src/rules/sat_coloring.jl b/src/rules/sat_coloring.jl
index 809f373b..ff20ce8e 100644
--- a/src/rules/sat_coloring.jl
+++ b/src/rules/sat_coloring.jl
@@ -4,31 +4,33 @@ The reduction result of a Sat problem to a Coloring problem.
 
 ### Fields
 - `Coloring{K, T, WT<:AbstractVector{T}}`: the coloring problem, where K is the number of colors and WT is the weights type. 
-- `varlabel`, used to filter extra variables
+- `posvertices`, a map from literal to vertex index
+- `negvertices`, a map from negative literal to vertex index
 
 Note: The coloring problem is a 3 coloring problem, in which a auxiliary color is used Auxiliary color => 2.
 """
-struct ReductionSatToColoring{K,S,T,WT<:AbstractVector{T}} <: AbstractReductionResult
+struct ReductionSatToColoring{K,T,WT<:AbstractVector{T}} <: AbstractReductionResult
     coloring::Coloring{K, T, WT}
-    varlabel::Dict{S, Int}
+    posvertices::Vector{Int}
+    negvertices::Vector{Int}
 end
 
 target_problem(res::ReductionSatToColoring) = res.coloring
 
 function reduceto(::Type{<:Coloring{3}}, sat::Satisfiability) #ensure the Sat problem is a Sat problem
-    sc = SATColoringConstructor(BoolVar.(variables(sat)))
+    sc = SATColoringConstructor(symbols(sat))
     for e in sat.cnf.clauses
         add_clause!(sc, e)
     end
     prob = Coloring{3}(sc.g, UnitWeight(ne(sc.g)))
-    return ReductionSatToColoring(prob, sc.varlabel)
+    return ReductionSatToColoring(prob, sc.posvertices, sc.negvertices)
 end
 
 function extract_solution(res::ReductionSatToColoring, sol)
-    out = zeros(eltype(sol),Int(length(res.varlabel)/2))
+    out = zeros(eltype(sol),length(res.posvertices))
     t, f, a = sol[1:3]
     @assert t != f && t != a "Invalid solution!"
-    for i in 4:3+Int(length(res.varlabel)/2)
+    for i in 4:3+length(res.posvertices)
         @assert sol[i] != a "Invalid solution, got auxiliary color: $a"
         out[i-3] = sol[i] == t
     end
@@ -36,24 +38,28 @@ function extract_solution(res::ReductionSatToColoring, sol)
 end
 
 # Construct the graph for the SAT problem and needed information
-struct SATColoringConstructor{T}
+struct SATColoringConstructor
     g::SimpleGraph{Int}    # the graph
-    varlabel::Dict{T,Int}  # a map from variable name to vertex index
+    posvertices::Vector{Int}  # a map from literal to vertex index
+    negvertices::Vector{Int}  # a map from negative literal to vertex index
+    vmap::Dict{BoolVar, Int}  # a map from literal to vertex index
 end
-function SATColoringConstructor(variables::Vector{T}) where T<:BoolVar
-    nv = length(variables)
-    g = SimpleGraph(2*nv+3)
+function SATColoringConstructor(symbols::Vector{Symbol})
+    nvar = length(symbols)
+    g = SimpleGraph(2*nvar+3)
     for (i, j) in [(1, 2), (1, 3), (2, 3)]
         add_edge!(g, i, j)
     end
-    for i in 1:nv
-        a, nota = 3 + i, 3 + i + nv
+    for i in 1:nvar
+        a, nota = 3 + i, 3 + i + nvar
         add_edge!(g, a, 3)   # attach_to_ancilla
         add_edge!(g, nota, 3)   # attach_to_ancilla
         add_edge!(g, a, nota)  # connect the variable and its negation
     end
-    varlabel = merge!(Dict(zip(variables, 4:3+nv)), Dict(zip((¬).(variables), 4+nv:2*nv+3)))
-    return SATColoringConstructor(g, varlabel)
+    posvertices = collect(4:3+nvar)
+    negvertices = 4+nvar:2*nvar+3
+    vmap = merge(Dict(zip(BoolVar.(symbols, false), posvertices)), Dict(zip(BoolVar.(symbols, true), negvertices)))
+    return SATColoringConstructor(g, posvertices, negvertices, vmap)
 end
 
 true_vertex(sc::SATColoringConstructor) = 1
@@ -66,15 +72,15 @@ end
 attach_to_ancilla!(sc::SATColoringConstructor, idx::Int) = _attach_to_idx!(sc, idx, ancilla_vertex(sc))
 attach_to_false!(sc::SATColoringConstructor, idx::Int) = _attach_to_idx!(sc, idx, false_vertex(sc))
 attach_to_true!(sc::SATColoringConstructor, idx::Int) = _attach_to_idx!(sc, idx, true_vertex(sc))
-function _attach_to_idx!(sc::SATColoringConstructor{T}, idx::Int, kth::Int) where T
+function _attach_to_idx!(sc::SATColoringConstructor, idx::Int, kth::Int)
     add_edge!(sc.g, idx, kth)
 end
 
-function add_clause!(sc::SATColoringConstructor{T}, c::CNFClause) where T
+function add_clause!(sc::SATColoringConstructor, c::CNFClause)
     @assert length(c.vars) > 0 "The clause must have at least 1 variables"
-    output_node = sc.varlabel[c.vars[1]] # get the first variable
+    output_node = sc.vmap[c.vars[1]] # get the first variable
     for i in c.vars[2:end]
-       output_node = add_coloring_or_gadget!(sc, output_node, sc.varlabel[i])
+       output_node = add_coloring_or_gadget!(sc, output_node, sc.vmap[i])
     end
     set_true!(sc, output_node)
 end
@@ -83,7 +89,7 @@ end
 # `input1`: the vertex index in `g` as the first input
 # `input2`: the vertex index in `g` as the second input
 # returns an output vertex number
-function add_coloring_or_gadget!(sc::SATColoringConstructor{T}, input1::Int, input2::Int) where T
+function add_coloring_or_gadget!(sc::SATColoringConstructor, input1::Int, input2::Int)
     add_vertices!(sc.g, 5) # add 5 nodes to the graph and track their index
     ancilla1, ancilla2, entrance1, entrance2, output = nv(sc.g)-4:nv(sc.g)
 
diff --git a/src/rules/sat_dominatingset.jl b/src/rules/sat_dominatingset.jl
index 5e6ddd51..4e993af2 100644
--- a/src/rules/sat_dominatingset.jl
+++ b/src/rules/sat_dominatingset.jl
@@ -26,7 +26,7 @@ function reduceto(::Type{DominatingSet{<:SimpleGraph}}, s::AbstractSatisfiabilit
     end
     for (i, clause_tmp) in enumerate(s.cnf.clauses)
         for literal in clause_tmp.vars
-            literal_node = 3 * (findfirst(==(literal.name), variables(s))-1) + (literal.neg ? 2 : 1)
+            literal_node = 3 * (findfirst(==(literal.name), symbols(s))-1) + (literal.neg ? 2 : 1)
             add_edge!(g, literal_node, 3 * num_variables(s)+i)
         end
     end
diff --git a/src/rules/sat_independentset.jl b/src/rules/sat_independentset.jl
index e7b015f2..97052462 100644
--- a/src/rules/sat_independentset.jl
+++ b/src/rules/sat_independentset.jl
@@ -15,7 +15,7 @@ end
 target_problem(res::ReductionSATToIndependentSet) = res.target
 
 function reduceto(::Type{IndependentSet{<:SimpleGraph}}, s::AbstractSatisfiabilityProblem)
-    literals = BoolVar{eltype(variables(s))}[]
+    literals = BoolVar{eltype(symbols(s))}[]
     g = SimpleGraph(0)
     for c in clauses(s)  # add edges between literals in the same clause
         add_vertices!(g, length(c.vars))
@@ -29,7 +29,7 @@ function reduceto(::Type{IndependentSet{<:SimpleGraph}}, s::AbstractSatisfiabili
             literals[i] == ¬(literals[j]) && add_edge!(g, i, j)
         end
     end
-    return ReductionSATToIndependentSet(IndependentSet(g), literals, variables(s), length(clauses(s)))
+    return ReductionSATToIndependentSet(IndependentSet(g), literals, symbols(s), length(clauses(s)))
 end
 
 function extract_solution(res::ReductionSATToIndependentSet{ST}, sol) where ST
diff --git a/test/models/Coloring.jl b/test/models/Coloring.jl
index 35c700ac..404c618b 100644
--- a/test/models/Coloring.jl
+++ b/test/models/Coloring.jl
@@ -4,7 +4,7 @@ using Test, ProblemReductions, Graphs
 
 @testset "coloring" begin
     # constructor function
-    @test flavors(Coloring{3}) == [0,1,2]
+    @test flavors(Coloring{3}) == (0, 1, 2)
     @test num_flavors(Coloring{3}) == 3
     
     g = SimpleGraph(4)
diff --git a/test/models/DominatingSet.jl b/test/models/DominatingSet.jl
index e09d88ec..c9e39b6f 100644
--- a/test/models/DominatingSet.jl
+++ b/test/models/DominatingSet.jl
@@ -23,7 +23,7 @@ using Test, ProblemReductions, Graphs
     # variables
     @test variables(DS_01) == [1, 2, 3, 4, 5]
     @test num_variables(DS_01) == 5
-    @test flavors(DominatingSet) == [0, 1]
+    @test flavors(DominatingSet) == (0, 1)
     @test problem_size(DS_01) == (; num_vertices = 5, num_edges = 4)
 
     # energy
diff --git a/test/models/Factoring.jl b/test/models/Factoring.jl
index c8953e6e..62b8db15 100644
--- a/test/models/Factoring.jl
+++ b/test/models/Factoring.jl
@@ -11,7 +11,7 @@ end
     z = 15
     f = Factoring(m, n, z)
     @test variables(f) == [1, 2, 3, 4, 5]
-    @test flavors(Factoring) == [0, 1]
+    @test flavors(Factoring) == (0, 1)
     @test problem_size(f) == (; num_bits_first = 2, num_bits_second = 3)
     @test num_flavors(f) == 2
     @test energy(f, [0, 1, 1, 1, 0]) == 1
diff --git a/test/models/IndependentSet.jl b/test/models/IndependentSet.jl
index 1d9e512d..8677a510 100644
--- a/test/models/IndependentSet.jl
+++ b/test/models/IndependentSet.jl
@@ -28,7 +28,7 @@ using Test, ProblemReductions, Graphs
     # variables
     @test variables(IS_01) == [1, 2, 3, 4]
     @test num_variables(IS_01) == 4
-    @test flavors(IndependentSet) == [0, 1]
+    @test flavors(IndependentSet) == (0, 1)
 
     # energy
     # Positive examples
@@ -41,4 +41,16 @@ using Test, ProblemReductions, Graphs
     @test findbest(IS_01, BruteForce()) == [[1, 0, 0, 1], [0, 1, 0, 1]] # "1" is superior to "0"
     @test Set( findbest(IS_03, BruteForce()) ) == Set( [[1, 0, 1, 0, 1], [1, 0, 0, 1, 1]] )
     @test configuration_space_size(IS_01) ≈ 4
+end
+
+@testset "energyterms" begin
+    g01 = smallgraph(:diamond)
+    IS_01 = IndependentSet(g01)
+    terms = ProblemReductions.energy_terms(IS_01)
+    @test length(terms) == 9
+    for cfg in [[0, 1, 1, 0], [1, 0, 0, 1]]
+        e1 = ProblemReductions.energy_eval_byid(terms, cfg .+ 1)
+        e2 = ProblemReductions.energy(IS_01, cfg)
+        @test (e1 == e2) || (e1 > 1e4 && e2 > 1e4)
+    end
 end
\ No newline at end of file
diff --git a/test/models/Matching.jl b/test/models/Matching.jl
index 652b58d1..e32b10f0 100644
--- a/test/models/Matching.jl
+++ b/test/models/Matching.jl
@@ -8,7 +8,7 @@ using ProblemReductions: is_matching
     @test m1 isa Matching
     @test variables(m1) == [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
     @test num_variables(m1) == 15
-    @test flavors(m1) == [0, 1]
+    @test flavors(m1) == (0, 1)
     @test problem_size(m1) == (; num_vertices = 10, num_edges = 15)
 
     #test2 
@@ -21,7 +21,7 @@ using ProblemReductions: is_matching
     @test set_weights(m2, [1, 1, 0, 0]) == Matching(g2, [1, 1, 0, 0])
     @test variables(m2) == [1, 2, 3, 4]
     @test num_variables(m2) == 4
-    @test flavors(m2) == [0, 1]
+    @test flavors(m2) == (0, 1)
     @test ProblemReductions.weights(m2) == [1, 0, 0, 1]
     @test ProblemReductions.set_weights(m2, [1, 1, 0, 0]) == Matching(g2, [1, 1, 0, 0])
     @test is_matching(m2.graph, [1, 0, 0, 1]) == true
diff --git a/test/models/MaxCut.jl b/test/models/MaxCut.jl
index a12bf820..0ee8accd 100644
--- a/test/models/MaxCut.jl
+++ b/test/models/MaxCut.jl
@@ -16,8 +16,8 @@ using Test, ProblemReductions, Graphs
     # variables
     @test variables(mc) == [1, 2, 3, 4]
     @test num_variables(mc) == 4
-    @test flavors(MaxCut) == [0, 1]
-    @test flavors(mc) == [0, 1]
+    @test flavors(MaxCut) == (0, 1)
+    @test flavors(mc) == (0, 1)
     @test num_flavors(mc) == 2
     # weights
     @test ProblemReductions.weights(mc) == [1, 3, 1, 4]
diff --git a/test/models/MaximalIS.jl b/test/models/MaximalIS.jl
index 50e45a7e..9dc9bdf8 100644
--- a/test/models/MaximalIS.jl
+++ b/test/models/MaximalIS.jl
@@ -9,7 +9,7 @@ using ProblemReductions:  is_maximal_independent_set
     @test mis1 isa MaximalIS
     @test variables(mis1) == [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
     @test num_variables(mis1) == 10
-    @test flavors(mis1) == [0, 1]
+    @test flavors(mis1) == (0, 1)
     @test num_flavors(mis1) == 2
     @test ProblemReductions.weights(mis1) == [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
     @test ProblemReductions.set_weights(mis1, [1, 5, 1, 4, 1, 3, 1, 2, 1, 2]) == MaximalIS(g,[1, 5, 1, 4, 1, 3, 1, 2, 1, 2])
@@ -25,7 +25,7 @@ using ProblemReductions:  is_maximal_independent_set
     @test mis2 isa MaximalIS
     @test variables(mis2) == [1, 2, 3, 4]
     @test num_variables(mis2) == 4
-    @test flavors(MaximalIS) == [0, 1]
+    @test flavors(MaximalIS) == (0, 1)
     @test ProblemReductions.weights(mis2) == [1, 1, 1, 1]
     mis2 =  set_weights(mis2, [1, 2, 1, 2]) 
     @test mis2 == MaximalIS(g,[1, 2, 1, 2])
diff --git a/test/models/Paintshop.jl b/test/models/Paintshop.jl
index 01d7d7c1..0971b431 100644
--- a/test/models/Paintshop.jl
+++ b/test/models/Paintshop.jl
@@ -6,9 +6,9 @@ using ProblemReductions:paint_shop_coloring_from_config
     ps1 = PaintShop(["a","b","a","c","c","b"])
     @test ps1 isa PaintShop
     @test ps1.isfirst == [1,1,0,1,0,0]
-    @test variables(ps1) == ["a","b","c"]
+    @test variables(ps1) == 1:3
     @test num_variables(ps1) == 3
-    @test flavors(ps1) == [0, 1]
+    @test flavors(ps1) == (0, 1)
     @test problem_size(ps1) == (; sequence_length = 6)
 
     #test2 We could use number for the variables for our convenience
diff --git a/test/models/QUBO.jl b/test/models/QUBO.jl
index 9f014489..34d7a4f6 100644
--- a/test/models/QUBO.jl
+++ b/test/models/QUBO.jl
@@ -15,7 +15,7 @@ using ProblemReductions, Test, Graphs
     # variables
     @test variables(q01) == [1, 2, 3]
     @test num_variables(q01) == 3
-    @test flavors(q01) == [0, 1]
+    @test flavors(q01) == (0, 1)
     @test num_flavors(q01) == 2
 
     # energy
diff --git a/test/models/Satisfiability.jl b/test/models/Satisfiability.jl
index b493d634..a913cf00 100644
--- a/test/models/Satisfiability.jl
+++ b/test/models/Satisfiability.jl
@@ -7,6 +7,7 @@ using ProblemReductions: KSatisfiability,clauses
 
     clause1 = CNFClause([bv1, bv2, bv3])
     clause2 = CNFClause([BoolVar("w"), bv1, BoolVar("x", true)])
+    clause3 = CNFClause([bv1, bv2])
 
     cnf_test = CNF([clause1, clause2])
     sat_test = Satisfiability(cnf_test)
@@ -17,7 +18,7 @@ using ProblemReductions: KSatisfiability,clauses
     
     @test is_kSAT(sat_test.cnf, 3)
     vars = ["x", "y", "z", "w"]
-    @test variables(sat_test) == vars
+    @test ProblemReductions.symbols(sat_test) == vars
     @test num_variables(sat_test) == 4
     @test problem_size(sat_test) == (; num_claues = 2, num_variables = 4)
 
@@ -36,9 +37,15 @@ using ProblemReductions: KSatisfiability,clauses
 
     # Tests for KSatisfiability
     ksat_test = KSatisfiability{3}(cnf_test)
+    @test_throws AssertionError KSatisfiability{3}(CNF([clause1, clause3]); allow_less=false)
+    @test KSatisfiability{3}(CNF([clause1, clause3]); allow_less=true) isa KSatisfiability
+    copied = set_weights(deepcopy(ksat_test), randn(length(ProblemReductions.weights(ksat_test))))
+    @test ksat_test != copied
+    @test ksat_test == ProblemReductions.set_weights(copied, ProblemReductions.weights(ksat_test))
+    @show ProblemReductions.energy_terms(ksat_test)
     @test clauses(ksat_test) == cnf_test.clauses
     @test ksat_test isa KSatisfiability
-    @test variables(ksat_test) == vars
+    @test ProblemReductions.symbols(ksat_test) == vars
     @test num_variables(ksat_test) == 4
 
     cfg = [0, 1, 0, 1]
diff --git a/test/models/SetCovering.jl b/test/models/SetCovering.jl
index 5e29672b..1f8c1d95 100644
--- a/test/models/SetCovering.jl
+++ b/test/models/SetCovering.jl
@@ -6,7 +6,7 @@ using Test, ProblemReductions, Graphs
     @test c.elements == [1, 2, 3, 4]
     @test variables(c)==[1, 2, 3]
     @test num_variables(c) == 3
-    @test flavors(SetCovering) == [0, 1]
+    @test flavors(SetCovering) == (0, 1)
     @test problem_size(c) == (; num_sets=3, num_elements=4)
     
     # weights interface
diff --git a/test/models/SetPacking.jl b/test/models/SetPacking.jl
index e10aa9a5..a50c224b 100644
--- a/test/models/SetPacking.jl
+++ b/test/models/SetPacking.jl
@@ -17,7 +17,7 @@ using Test, ProblemReductions
     # variables
     @test variables(SP_01) == [1, 2, 3, 4, 5]
     @test num_variables(SP_01) == 5
-    @test flavors(SetPacking) == [0, 1]
+    @test flavors(SetPacking) == (0, 1)
 
     # energy
     # a Positive examples
diff --git a/test/models/SpinGlass.jl b/test/models/SpinGlass.jl
index 2966fc98..6d69232f 100644
--- a/test/models/SpinGlass.jl
+++ b/test/models/SpinGlass.jl
@@ -12,7 +12,7 @@ using ProblemReductions, Test, Graphs
     # variables
     @test variables(sg) == [1, 2, 3]
     @test num_variables(sg) == 3
-    @test flavors(sg) == [1, -1]
+    @test flavors(sg) == (1, -1)
     @test num_flavors(sg) == 2
 
     # weights
@@ -25,3 +25,13 @@ using ProblemReductions, Test, Graphs
         @test cfg[3] == cfg[1] & cfg[2]
     end
 end
+
+
+@testset "energyterms - spinglass" begin
+    g01 = smallgraph(:diamond)
+    sg = SpinGlass(g01, [1, -2, -2, 1, 2], [1, 1, -2, -2])
+    terms = ProblemReductions.energy_terms(sg)
+    for cfg in [[-1, 1, 1, -1], [1, -1, -1, 1]]
+        @test ProblemReductions.energy_eval_byid(terms, (1 .- cfg) .÷ 2 .+ 1) == ProblemReductions.energy(sg, cfg)
+    end
+end
\ No newline at end of file
diff --git a/test/models/VertexCovering.jl b/test/models/VertexCovering.jl
index 355c5d84..f7977d08 100644
--- a/test/models/VertexCovering.jl
+++ b/test/models/VertexCovering.jl
@@ -12,7 +12,7 @@ using Test, ProblemReductions, Graphs
     @test problem_size(vc) == (; num_vertices = 4, num_edges = 4)
     @test variables(vc) == [1, 2, 3, 4]
     @test num_variables(vc) == 4
-    @test flavors(VertexCovering) == [0, 1]
+    @test flavors(VertexCovering) == (0, 1)
     @test ProblemReductions.weights(vc) == [1, 3, 1, 4]
     @test set_weights(vc, [1, 3, 4, 4]) == VertexCovering(g, [1, 3, 4, 4])
 
diff --git a/test/rules/rules.jl b/test/rules/rules.jl
index d56d119f..eed09048 100644
--- a/test/rules/rules.jl
+++ b/test/rules/rules.jl
@@ -70,7 +70,7 @@ end
             spinglass => MaxCut,
             qubo => SpinGlass{<:SimpleGraph},
             spinglass => QUBO,
-            sat => KSatisfiability,
+            sat => KSatisfiability{3},
             ksat => Satisfiability,
             sat => IndependentSet{<:SimpleGraph},
             sat => DominatingSet{<:SimpleGraph},
diff --git a/test/rules/sat_3sat.jl b/test/rules/sat_3sat.jl
index cc52c61c..d8754430 100644
--- a/test/rules/sat_3sat.jl
+++ b/test/rules/sat_3sat.jl
@@ -1,8 +1,6 @@
 using Test, ProblemReductions
-using ProblemReductions: generate_dummy_var, rename_variables, transform_to_3_literal_clause, transform_to_3_literal_cnf
 
 @testset "sat_3sat" begin
-
     # Example 001 (Satisfiability => 3-Satisfiability)
     bv1 = BoolVar(:x, false)
     bv2 = BoolVar(:y, true)
@@ -16,29 +14,7 @@ using ProblemReductions: generate_dummy_var, rename_variables, transform_to_3_li
     cnf01 = CNF([clause1, clause2, clause3])
     sat01 = Satisfiability(cnf01)
 
-    @test variables( rename_variables(sat01)[1] ) == [Symbol("x_1"), Symbol("x_2"), Symbol("x_3"), Symbol("x_4")]
-    @test generate_dummy_var(5)[1] == BoolVar(Symbol("z_$(6)"), false)
-    @test CNF( transform_to_3_literal_clause(clause2.vars, 0)[1] ) == ( bv2 ∨ bv3 ∨ BoolVar(Symbol("z_$(1)"), false) ) ∧ ( bv2 ∨ bv3 ∨ BoolVar(Symbol("z_$(1)"), true) )
-
-    expected_transformed_cnf = CNF([
-    CNFClause([bv1, BoolVar(Symbol("z_1"), false), BoolVar(Symbol("z_2"), false)]),
-    CNFClause([bv1, BoolVar(Symbol("z_1"), true), BoolVar(Symbol("z_2"), false)]),
-    CNFClause([bv1, BoolVar(Symbol("z_1"), false), BoolVar(Symbol("z_2"), true)]),
-    CNFClause([bv1, BoolVar(Symbol("z_1"), true), BoolVar(Symbol("z_2"), true)]),
-
-    CNFClause([bv2, bv3, BoolVar(Symbol("z_3"), false)]),
-    CNFClause([bv2, bv3, BoolVar(Symbol("z_3"), true)]),
-
-    CNFClause([bv1, bv2, BoolVar(Symbol("z_4"), false)]),
-    CNFClause([bv3, bv4, BoolVar(Symbol("z_4"), true)])
-    ])
-    transformed_cnf = transform_to_3_literal_cnf(sat01).cnf
-    @test transformed_cnf == expected_transformed_cnf
-
-    reduction_result = reduceto(KSatisfiability, sat01)
-    @test reduction_result.sat_target == KSatisfiability{3}( transform_to_3_literal_cnf( rename_variables(sat01)[1] ).cnf )
-    @test target_problem( reduction_result ) == KSatisfiability{3}( transform_to_3_literal_cnf( rename_variables(sat01)[1] ).cnf )
-
+    reduction_result = reduceto(KSatisfiability{3}, sat01)
     original_sol = findbest(sat01, BruteForce() )
     new_sol = findbest(reduction_result.sat_target, BruteForce() )
     @test original_sol == extract_multiple_solutions(reduction_result, new_sol)
@@ -60,10 +36,7 @@ using ProblemReductions: generate_dummy_var, rename_variables, transform_to_3_li
     cnf02 = CNF([clause5, clause6])
     sat02 = Satisfiability(cnf02)
 
-    reduction_result_03 = reduceto(KSatisfiability, sat02)
+    reduction_result_03 = reduceto(KSatisfiability{3}, sat02)
     @test Set( findbest(sat02, BruteForce() ) ) == Set( extract_multiple_solutions( reduction_result_03, findbest(reduction_result_03.sat_target, BruteForce() ) ) )
     @test issubset( Set( findbest(sat02, BruteForce() ) ), Set( unique( extract_solution.( Ref(reduction_result_03), findbest(reduction_result_03.sat_target, BruteForce() ) ) ) ) )
-end
-    
-
-    
+end
\ No newline at end of file
diff --git a/test/rules/sat_coloring.jl b/test/rules/sat_coloring.jl
index ad6f7d19..854833c3 100644
--- a/test/rules/sat_coloring.jl
+++ b/test/rules/sat_coloring.jl
@@ -5,11 +5,15 @@ using ProblemReductions: SATColoringConstructor, add_clause!, Satisfiability, CN
     bool1 = BoolVar(:X)
     bool2 = BoolVar(:Y)
     clause1 = CNFClause([bool1, bool2])
-    CNF1 = CNF([clause1])
+    clause2 = CNFClause([bool1, ¬bool2])
+    CNF1 = CNF([clause1, clause2])
     Sat1 = Satisfiability(CNF1)
     @test Sat1 isa Satisfiability
     result = reduceto(Coloring{3}, Sat1)
-    expected_varlabel = Dict{BoolVar{Symbol}, Int64}(¬bool1 => 6, ¬bool2 => 7,bool2 => 5, bool1 => 4) 
-    @test result.varlabel == expected_varlabel
+    @test result.posvertices == [4, 5]
+    @test result.negvertices == [6, 7]
     @test target_problem(result) isa Coloring
+    res = findbest(target_problem(result), BruteForce())
+    backres = extract_solution.(Ref(result), res)
+    @test unique(backres) == [[1, 0], [1, 1]]
 end