Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix Bug: General SAT to Independent Set #71

Merged
merged 4 commits into from
Aug 14, 2024
Merged

Fix Bug: General SAT to Independent Set #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b641f55
Fix Bug: General SAT to Independent Set
SciCodePhy Aug 13, 2024
cf8596b
Update test/rules/rules.jl
SciCodePhy Aug 14, 2024
2ebee57
Fix test/rules/rules.jl
SciCodePhy Aug 14, 2024
b279101
Fix test/rules/rules.jl version-03
SciCodePhy Aug 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 53 additions & 69 deletions src/rules/sat_independentset.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,35 +23,13 @@ end
# ----Useful Functions----
function reduce_sat_to_independent_set(s::Satisfiability{T}) where T

var_list = Vector{BoolVar}()
var_missing_list = Vector{BoolVar}()
for clause_tmp in s.cnf.clauses
for var in clause_tmp.vars
if var in var_list
push!(var_list, var)
end
end
end
for literal in variables(s)
if ( BoolVar(literal, false) in var_list ) == false
push!(var_missing_list, BoolVar(literal, false) )
end
if ( BoolVar(literal, true) in var_list ) == false
push!(var_missing_list, BoolVar(literal, true) )
end
end

k = length(s.cnf.clauses)
num_nodes = length( var_missing_list ) + 3 * k
num_nodes = 3 * k
graph = SimpleGraph(num_nodes)

literal_to_nodes = Dict{BoolVar{T}, Vector{Int}}()
node_counter = 0

for var in var_missing_list
node_counter += 1
literal_to_nodes[var] = [node_counter]
end
for clause_tmp in s.cnf.clauses

clause_literals = clause_tmp.vars
Expand Down Expand Up @@ -94,6 +72,7 @@ end

function transform_is_to_sat_solution(sat_source::Satisfiability, sol, literal_to_nodes::Dict{BoolVar{Symbol}, Vector{Int}})

k = length(sat_source.cnf.clauses)
num_source_vars = num_variables(sat_source)

if sol isa Vector{ Vector{Int64} }
Expand All @@ -120,14 +99,15 @@ function transform_is_to_sat_solution(sat_source::Satisfiability, sol, literal_t
end

if length(assignments) == num_source_vars

original_solution = fill(-1, num_source_vars)
for (var_i, var) in enumerate( variables( sat_source ) )
original_solution[var_i] = assignments[var]
end
push!(all_original_solutions, original_solution)

else
elseif ( length( assignments ) != num_source_vars )

literals_missed = []
for literal in variables(sat_source)
if !haskey(assignments, literal)
Expand All @@ -150,67 +130,71 @@ function transform_is_to_sat_solution(sat_source::Satisfiability, sol, literal_t

push!(all_original_solutions, original_solution)
end

end

end

return unique(all_original_solutions)

elseif sol isa Vector{Int64}

assignments = Dict{Symbol, Int64}()
for (vertex, vertex_true) in enumerate( sol )

if vertex_true == 1
for (literal, nodes) in literal_to_nodes
if vertex in nodes

if literal.neg
assignments[literal.name] = 0
else
assignments[literal.name] = 1
end

break
for (vertex, vertex_true) in enumerate( sol )

if vertex_true == 1
for (literal, nodes) in literal_to_nodes
if vertex in nodes

if literal.neg
assignments[literal.name] = 0
else
assignments[literal.name] = 1
end

break
end
end
end
end

if length(assignments) == num_source_vars

if length(assignments) == num_source_vars

original_solution = fill(-1, num_source_vars)
for (var_i, var) in enumerate( variables( sat_source ) )
original_solution[var_i] = assignments[var]
original_solution = fill(-1, num_source_vars)
for (var_i, var) in enumerate( variables( sat_source ) )
original_solution[var_i] = assignments[var]
end
return original_solution

elseif ( length( assignments ) != num_source_vars )

all_original_solutions = Vector{Vector{Int64}}()
literals_missed = []
for literal in variables(sat_source)
if !haskey(assignments, literal)
push!(literals_missed, literal)
end
end
@warn "return $(2^( length(literals_missed) )) degenerate solutions for single input"

for each_case in 0:( 2^( length(literals_missed) ) - 1 )
complete_assignments = copy( assignments )
case_number = each_case
for literal in literals_missed
complete_assignments[literal] = rem(case_number, 2)
case_number = div(case_number, 2)
end
return original_solution

else
all_original_solutions = Vector{Vector{Int64}}()
literals_missed = []
for literal in variables(sat_source)
if !haskey(assignments, literal)
push!(literals_missed, literal)
end
original_solution = fill(-1, num_source_vars)
for (var_i, var) in enumerate( variables( sat_source ) )
original_solution[var_i] = complete_assignments[var]
end

for each_case in 0:( 2^( length(literals_missed) ) - 1 )
complete_assignments = copy( assignments )
case_number = each_case
for literal in literals_missed
complete_assignments[literal] = rem(case_number, 2)
case_number = div(case_number, 2)
end
push!(all_original_solutions, original_solution)
end
return unique(all_original_solutions)

original_solution = fill(-1, num_source_vars)
for (var_i, var) in enumerate( variables( sat_source ) )
original_solution[var_i] = complete_assignments[var]
end

push!(all_original_solutions, original_solution)
end
end

return unique(all_original_solutions)
end
end
end
9 changes: 8 additions & 1 deletion test/rules/rules.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,14 @@ end
best_target = findbest(target, BruteForce())

# extract the solution
best_source_extracted = extract_solution.(Ref(result), best_target)
best_source_extracted = Vector{Any}()
for sol_tmp in extract_solution.(Ref(result), best_target)
if sol_tmp[1] != sol_tmp[1][1]
best_source_extracted = vcat(best_source_extracted, sol_tmp)
else
best_source_extracted = push!(best_source_extracted, sol_tmp)
end
end

# check if the solutions are the same
@test unique!(sort(best_source)) == unique!(sort(best_source_extracted))
Expand Down
66 changes: 64 additions & 2 deletions test/rules/sat_independentset.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,15 @@ using Test, ProblemReductions, Graphs
IS01 = reduction_results.is_target
sol_IS = findbest( IS01, BruteForce() )
@test Set( findbest(sat01, BruteForce()) ) == Set( extract_solution(reduction_results, sol_IS) )

sol_single_input_01 = Vector{Vector{Int}}()
for sol_tmp in extract_solution.(Ref(reduction_results), sol_IS)
if sol_tmp isa Vector{Vector{Int}}
sol_single_input_01 = vcat(sol_single_input_01, sol_tmp)
elseif sol_tmp isa Vector{Int}
sol_single_input_01 = vcat(sol_single_input_01, [sol_tmp])
end
end
@test Set( findbest(sat01, BruteForce()) ) == Set( unique(sol_single_input_01) )
@test target_problem( reduction_results ) == IS01

# Example 002: satisfiable 3-SAT
Expand All @@ -34,6 +42,15 @@ using Test, ProblemReductions, Graphs
IS02 = reduction_results_02.is_target
sol_IS_02 = findbest( IS02, BruteForce() )
@test Set( findbest( sat02, BruteForce() ) ) == Set( extract_solution(reduction_results_02, sol_IS_02) )
sol_single_input_02 = Vector{Vector{Int}}()
for sol_tmp in extract_solution.(Ref(reduction_results_02), sol_IS_02)
if sol_tmp isa Vector{Vector{Int}}
sol_single_input_02 = vcat(sol_single_input_02, sol_tmp)
elseif sol_tmp isa Vector{Int}
sol_single_input_02 = vcat(sol_single_input_02, [sol_tmp])
end
end
@test Set( findbest(sat02, BruteForce()) ) == Set( unique(sol_single_input_02) )

# Example 003: satisfiable 3-SAT
clause8 = CNFClause( [x1, x2, x3] )
Expand All @@ -43,6 +60,15 @@ using Test, ProblemReductions, Graphs
IS03 = reduction_results_03.is_target
sol_IS_03 = findbest( IS03, BruteForce() )
@test Set( findbest( sat03, BruteForce() ) ) == Set( extract_solution(reduction_results_03, sol_IS_03) )
sol_single_input_03 = Vector{Vector{Int}}()
for sol_tmp in extract_solution.(Ref(reduction_results_03), sol_IS_03)
if sol_tmp isa Vector{Vector{Int}}
sol_single_input_03 = vcat(sol_single_input_03, sol_tmp)
elseif sol_tmp isa Vector{Int}
sol_single_input_03 = vcat(sol_single_input_03, [sol_tmp])
end
end
@test Set( findbest(sat03, BruteForce()) ) == Set( unique(sol_single_input_03) )

# Example 004: unsatisfiable 3-SAT (trivial example)
clause10 = CNFClause( [x1, x1, x1] )
Expand All @@ -53,14 +79,32 @@ using Test, ProblemReductions, Graphs
IS04 = reduction_results_04.is_target
sol_IS_04 = findbest( IS04, BruteForce() )
@test Set( findbest( sat04, BruteForce() ) ) == Set( extract_solution(reduction_results_04, sol_IS_04) )

sol_single_input_04 = Vector{Vector{Int}}()
for sol_tmp in extract_solution.(Ref(reduction_results_04), sol_IS_04)
if sol_tmp isa Vector{Vector{Int}}
sol_single_input_04 = vcat(sol_single_input_04, sol_tmp)
elseif sol_tmp isa Vector{Int}
sol_single_input_04 = vcat(sol_single_input_04, [sol_tmp])
end
end
@test Set( findbest(sat04, BruteForce()) ) == Set( unique(sol_single_input_04) )

# Example 005: unsatisfiable 1-SAT (equivalent with example 004)
sat05 = Satisfiability( CNF( [ CNFClause([x1]), CNFClause([nx1]) ] ) )
reduction_results_05 = reduceto(IndependentSet, sat05)
@test reduction_complexity(IndependentSet, sat05) == 1
IS05 = reduction_results_05.is_target
sol_IS_05 = findbest( IS05, BruteForce() )
@test Set( findbest( sat05, BruteForce() ) ) == Set( extract_solution(reduction_results_05, sol_IS_05) )
sol_single_input_05 = Vector{Vector{Int}}()
for sol_tmp in extract_solution.(Ref(reduction_results_05), sol_IS_05)
if sol_tmp isa Vector{Vector{Int}}
sol_single_input_05 = vcat(sol_single_input_05, sol_tmp)
elseif sol_tmp isa Vector{Int}
sol_single_input_05 = vcat(sol_single_input_05, [sol_tmp])
end
end
@test Set( findbest(sat05, BruteForce()) ) == Set( unique(sol_single_input_05) )

# Example 006: unsatisfiable 2-SAT
sat06 = Satisfiability( CNF( [ CNFClause([x1, x2]), CNFClause([x1, nx2]), CNFClause([nx1, x2]), CNFClause([nx1, nx2]) ] ) )
Expand All @@ -69,6 +113,15 @@ using Test, ProblemReductions, Graphs
IS06 = reduction_results_06.is_target
sol_IS_06 = findbest( IS06, BruteForce() )
@test Set( findbest( sat06, BruteForce() ) ) == Set( extract_solution(reduction_results_06, sol_IS_06) )
sol_single_input_06 = Vector{Vector{Int}}()
for sol_tmp in extract_solution.(Ref(reduction_results_06), sol_IS_06)
if sol_tmp isa Vector{Vector{Int}}
sol_single_input_06 = vcat(sol_single_input_06, sol_tmp)
elseif sol_tmp isa Vector{Int}
sol_single_input_06 = vcat(sol_single_input_06, [sol_tmp])
end
end
@test Set( findbest(sat06, BruteForce()) ) == Set( unique(sol_single_input_06) )

# Example 007: satisfiable 2-SAT
sat07 = Satisfiability( CNF( [ CNFClause([x1, x2]), CNFClause([x1, nx2]), CNFClause([nx1, x2]) ] ) )
Expand All @@ -77,4 +130,13 @@ using Test, ProblemReductions, Graphs
IS07 = reduction_results_07.is_target
sol_IS_07 = findbest( IS07, BruteForce() )
@test Set( findbest( sat07, BruteForce() ) ) == Set( extract_solution(reduction_results_07, sol_IS_07) )
sol_single_input_07 = Vector{Vector{Int}}()
for sol_tmp in extract_solution.(Ref(reduction_results_07), sol_IS_07)
if sol_tmp isa Vector{Vector{Int}}
sol_single_input_07 = vcat(sol_single_input_07, sol_tmp)
elseif sol_tmp isa Vector{Int}
sol_single_input_07 = vcat(sol_single_input_07, [sol_tmp])
end
end
@test Set( findbest(sat07, BruteForce()) ) == Set( unique(sol_single_input_07) )
end