From 0345fa0efeabdb64374d9151b6137e3e96877ddc Mon Sep 17 00:00:00 2001 From: SciCodePhy Date: Wed, 21 Aug 2024 08:51:20 -0400 Subject: [PATCH 1/6] New Reduction: SAT to Dominating Set --- src/ProblemReductions.jl | 2 +- src/rules/sat_dominatingset.jl | 84 +++++++++++++++++++++++++++++++++ test/rules/rules.jl | 7 ++- test/rules/sat_dominatingset.jl | 70 +++++++++++++++++++++++++++ 4 files changed, 161 insertions(+), 2 deletions(-) create mode 100644 src/rules/sat_dominatingset.jl create mode 100644 test/rules/sat_dominatingset.jl diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl index ee2849d..3672d50 100644 --- a/src/ProblemReductions.jl +++ b/src/ProblemReductions.jl @@ -39,7 +39,7 @@ export ReductionCircuitToSpinGlass, ReductionMaxCutToSpinGlass, ReductionSpinGla ReductionSpinGlassToQUBO, ReductionQUBOToSpinGlass export findbest, BruteForce export CNF -export Reduction3SATToIndependentSet +export ReductionSATToIndependentSet, ReductionSATTODominatingSet # reduction path export ReductionGraph, reduction_graph, reduction_paths, implement_reduction_path diff --git a/src/rules/sat_dominatingset.jl b/src/rules/sat_dominatingset.jl new file mode 100644 index 0000000..1d55491 --- /dev/null +++ b/src/rules/sat_dominatingset.jl @@ -0,0 +1,84 @@ +struct ReductionSATToDominatingSet{T, GT<:AbstractGraph} <: AbstractReductionResult + target::DominatingSet{GT} # the target problem + num_literals::Int # number of literals in the SAT problem + num_clauses::Int # number of clauses in the SAT problem +end +target_problem(res::ReductionSATToDominatingSet) = res.target + +@with_complexity 1 function reduceto(::Type{<:DominatingSet}, s::AbstractSatisfiabilityProblem) + num_clauses = length(s.cnf.clauses) + num_vertices = 3 * num_variables(s) + num_clauses + g = SimpleGraph(num_vertices) + for i in 1:num_variables(s) + for m in 3*(i-1)+1:3*i + for n in m:3*i + add_edge!(g, m, n) + end + end + 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) + add_edge!(g, literal_node, 3 * num_variables(s)+i) + end + end + return ReductionSATToDominatingSet(DominatingSet(g), num_variables(s), num_clauses) +end + +function extract_solution(res::ReductionSATToDominatingSet, sol) + if count(value -> value == 1, sol) > res.num_literals + return nothing + end + assignment = fill(0, res.num_literals) + for (i, value) in enumerate(sol) + if value == 1 + if value == 1 + if rem(i, 3) == 1 + assignment[div(i, 3)+1] = 1 + elseif rem(i, 3) == 2 + assignment[div(i, 3)+1] = 0 + elseif rem(i, 3) == 0 + assignment[div(i, 3)] = rand([0,1]) + end + end + end + end + return assignment +end + +function extract_multiple_solutions(res::ReductionSATToDominatingSet, sol) + if count(value -> value == 1, sol[1]) > res.num_literals + return [] + end + all_assignments = Vector{Vector{Int}}() + for sol_tmp in sol + assignment = fill(0, res.num_literals) + dummy_vars = Vector{Int}() + for (i, value) in enumerate(sol_tmp) + if value == 1 + if rem(i, 3) == 1 + assignment[div(i, 3)+1] = 1 + elseif rem(i, 3) == 2 + assignment[div(i, 3)+1] = 0 + elseif rem(i, 3) == 0 + push!(dummy_vars, div(i, 3)) + end + end + end + if length(dummy_vars) > 0 + for each_case in 0:( 2^( length(dummy_vars) ) - 1 ) + copied_assignment = copy(assignment) + case_number = each_case + for var in dummy_vars + copied_assignment[var] = rem(case_number, 2) + case_number = div(case_number, 2) + end + push!(all_assignments, copied_assignment) + end + else + push!(all_assignments, assignment) + end + end + return unique(all_assignments) +end + diff --git a/test/rules/rules.jl b/test/rules/rules.jl index 506b2c2..dd90c0d 100644 --- a/test/rules/rules.jl +++ b/test/rules/rules.jl @@ -31,6 +31,10 @@ end include("sat_independentset.jl") end +@testset "sat_dominatingset" begin + include("sat_dominatingset.jl") +end + @testset "rules" begin circuit = CircuitSAT(@circuit begin x = a ∨ ¬b @@ -58,7 +62,8 @@ end spinglass2 => QUBO, sat => KSatisfiability, ksat => Satisfiability, - sat => IndependentSet + sat => IndependentSet, + sat => DominatingSet ] @info "Testing reduction from $(typeof(source)) to $(target_type)" # directly solve diff --git a/test/rules/sat_dominatingset.jl b/test/rules/sat_dominatingset.jl new file mode 100644 index 0000000..ac2cef3 --- /dev/null +++ b/test/rules/sat_dominatingset.jl @@ -0,0 +1,70 @@ +@testset "sat_dominatingset" begin + function verify(sat) + reduction_results = reduceto(DominatingSet, sat) + DS_tmp = reduction_results |> target_problem + sol_DS = findbest(DS_tmp, BruteForce()) + s1 = Set(findbest(sat, BruteForce())) + s2 = Set( unique( extract_solution.(Ref(reduction_results), sol_DS) ) ) + s3 = Set(extract_multiple_solutions(reduction_results, sol_DS)) + return (s2 ⊆ s1) && (s3 == s1) + end + + function verify_unsatisfiable(sat) + reduction_results = reduceto(DominatingSet, sat) + DS_tmp = reduction_results |> target_problem + sol_DS = findbest(DS_tmp, BruteForce()) + s2 = Set( unique( extract_solution.(Ref(reduction_results), sol_DS) ) ) + s3 = Set(extract_multiple_solutions(reduction_results, sol_DS)) + return (s2 == Set([nothing])) && (s3 == Set([])) + end + + # Example 001: satisfiable 3-SAT + x1 = BoolVar(:x1, false) + nx1 = BoolVar(:x1, true) + x2 = BoolVar(:x2, false) + nx2 = BoolVar(:x2, true) + x3 = BoolVar(:x3, false) + nx3 = BoolVar(:x3, true) + + clause1 = CNFClause([x1, nx2, x3]) + clause2 = CNFClause([nx1, x2, nx3]) + clause3 = CNFClause([x1, nx2, nx3]) + clause4 = CNFClause([nx1, x2, x3]) + + clause_lst = [clause1, clause2, clause3, clause4] + sat01 = Satisfiability(CNF(clause_lst)) + + @test reduction_complexity(DominatingSet, sat01) == 1 + @test verify(sat01) + + # Example 002: satisfiable 3-SAT + clause5 = CNFClause([nx1, x2, x3]) + clause6 = CNFClause([x1, nx2, x3]) + clause7 = CNFClause([x1, x2, nx3]) + sat02 = Satisfiability(CNF([clause5, clause6, clause7])) + @test verify(sat02) + + # Example 003: satisfiable 3-SAT + clause8 = CNFClause([x1, x2, x3]) + clause9 = CNFClause([nx1, nx2, nx3]) + sat03 = Satisfiability(CNF([clause8, clause9])) + @test verify(sat03) + + # Example 004: unsatisfiable 3-SAT (trivial example) + clause10 = CNFClause([x1, x1, x1]) + clause11 = CNFClause([nx1, nx1, nx1]) + sat04 = Satisfiability(CNF([clause10, clause11])) + @test verify_unsatisfiable(sat04) + + # Example 005: unsatisfiable 1-SAT (equivalent with example 004) + sat05 = Satisfiability(CNF([CNFClause([x1]), CNFClause([nx1])])) + @test verify_unsatisfiable(sat05) + + # Example 006: unsatisfiable 2-SAT + sat06 = Satisfiability(CNF([CNFClause([x1, x2]), CNFClause([x1, nx2]), CNFClause([nx1, x2]), CNFClause([nx1, nx2])])) + @test verify_unsatisfiable(sat06) + + # Example 007: satisfiable 2-SAT + sat07 = Satisfiability(CNF([CNFClause([x1, x2]), CNFClause([x1, nx2]), CNFClause([nx1, x2])])) + @test verify(sat07) +end \ No newline at end of file From d000e10fed74864f3755f1931fc6714483707d53 Mon Sep 17 00:00:00 2001 From: SciCodePhy Date: Wed, 21 Aug 2024 08:57:24 -0400 Subject: [PATCH 2/6] Typo: "TO" -> "To" --- src/ProblemReductions.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl index 3672d50..042c280 100644 --- a/src/ProblemReductions.jl +++ b/src/ProblemReductions.jl @@ -39,7 +39,7 @@ export ReductionCircuitToSpinGlass, ReductionMaxCutToSpinGlass, ReductionSpinGla ReductionSpinGlassToQUBO, ReductionQUBOToSpinGlass export findbest, BruteForce export CNF -export ReductionSATToIndependentSet, ReductionSATTODominatingSet +export ReductionSATToIndependentSet, ReductionSATToDominatingSet # reduction path export ReductionGraph, reduction_graph, reduction_paths, implement_reduction_path From 44bc2983b7b608424327c328be39fe23fc84018c Mon Sep 17 00:00:00 2001 From: SciCodePhy Date: Wed, 21 Aug 2024 09:03:18 -0400 Subject: [PATCH 3/6] Modify struct; Add Docstring --- src/rules/sat_dominatingset.jl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/rules/sat_dominatingset.jl b/src/rules/sat_dominatingset.jl index 1d55491..495ffba 100644 --- a/src/rules/sat_dominatingset.jl +++ b/src/rules/sat_dominatingset.jl @@ -1,4 +1,12 @@ -struct ReductionSATToDominatingSet{T, GT<:AbstractGraph} <: AbstractReductionResult +""" +$TYPEDEF + +The reduction result of a general SAT problem to an Dominating Set problem. + +### Fields +$TYPEDFIELDS +""" +struct ReductionSATToDominatingSet{GT<:AbstractGraph} <: AbstractReductionResult target::DominatingSet{GT} # the target problem num_literals::Int # number of literals in the SAT problem num_clauses::Int # number of clauses in the SAT problem From d9016aed8c877e62aaa60f68d728bf0783980580 Mon Sep 17 00:00:00 2001 From: SciCodePhy Date: Wed, 21 Aug 2024 09:05:49 -0400 Subject: [PATCH 4/6] Forget to include using in test --- test/rules/sat_dominatingset.jl | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/rules/sat_dominatingset.jl b/test/rules/sat_dominatingset.jl index ac2cef3..04300af 100644 --- a/test/rules/sat_dominatingset.jl +++ b/test/rules/sat_dominatingset.jl @@ -1,3 +1,5 @@ +using Test, ProblemReductions, Graphs + @testset "sat_dominatingset" begin function verify(sat) reduction_results = reduceto(DominatingSet, sat) From 0846b4289ba81c2cc6ce68b35cc899aff6cdc22d Mon Sep 17 00:00:00 2001 From: SciCodePhy Date: Wed, 21 Aug 2024 09:08:48 -0400 Subject: [PATCH 5/6] Include dominatingset in rules.jl --- src/rules/rules.jl | 1 + 1 file changed, 1 insertion(+) diff --git a/src/rules/rules.jl b/src/rules/rules.jl index e3d6e6d..49994f4 100644 --- a/src/rules/rules.jl +++ b/src/rules/rules.jl @@ -88,3 +88,4 @@ include("sat_coloring.jl") include("vertexcovering_setcovering.jl") include("factoring_sat.jl") include("sat_independentset.jl") +include("sat_dominatingset.jl") From 450aeda8df9f38a864cf47d7eadb14b416aa5017 Mon Sep 17 00:00:00 2001 From: SciCodePhy Date: Wed, 21 Aug 2024 09:17:40 -0400 Subject: [PATCH 6/6] clean up --- src/rules/sat_dominatingset.jl | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/rules/sat_dominatingset.jl b/src/rules/sat_dominatingset.jl index 495ffba..f5e6ea5 100644 --- a/src/rules/sat_dominatingset.jl +++ b/src/rules/sat_dominatingset.jl @@ -40,14 +40,12 @@ function extract_solution(res::ReductionSATToDominatingSet, sol) assignment = fill(0, res.num_literals) for (i, value) in enumerate(sol) if value == 1 - if value == 1 - if rem(i, 3) == 1 - assignment[div(i, 3)+1] = 1 - elseif rem(i, 3) == 2 - assignment[div(i, 3)+1] = 0 - elseif rem(i, 3) == 0 - assignment[div(i, 3)] = rand([0,1]) - end + if rem(i, 3) == 1 + assignment[div(i, 3)+1] = 1 + elseif rem(i, 3) == 2 + assignment[div(i, 3)+1] = 0 + elseif rem(i, 3) == 0 + assignment[div(i, 3)] = rand([0,1]) end end end