New Reduction: SAT to Dominating Set

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

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")

src/rules/sat_dominatingset.jl

@@ -0,0 +1,90 @@
+"""
+$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
+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 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
+    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
+

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

test/rules/sat_dominatingset.jl

@@ -0,0 +1,72 @@
+using Test, ProblemReductions, Graphs
+
+@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