diff --git a/src/rules/sat_independentset.jl b/src/rules/sat_independentset.jl index 4176a06..72ec41d 100644 --- a/src/rules/sat_independentset.jl +++ b/src/rules/sat_independentset.jl @@ -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 @@ -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} } @@ -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) @@ -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 diff --git a/test/rules/rules.jl b/test/rules/rules.jl index 445b0ad..5a782c1 100644 --- a/test/rules/rules.jl +++ b/test/rules/rules.jl @@ -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)) diff --git a/test/rules/sat_independentset.jl b/test/rules/sat_independentset.jl index 920fc08..5af4a32 100644 --- a/test/rules/sat_independentset.jl +++ b/test/rules/sat_independentset.jl @@ -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 @@ -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] ) @@ -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] ) @@ -53,7 +79,16 @@ 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) @@ -61,6 +96,15 @@ using Test, ProblemReductions, Graphs 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]) ] ) ) @@ -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]) ] ) ) @@ -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 \ No newline at end of file