Add converter to hard constraints

Project.toml

@@ -1,7 +1,7 @@
 name = "ProblemReductions"
 uuid = "899c297d-f7d2-4ebf-8815-a35996def416"
 authors = ["GiggleLiu <cacate0129@gmail.com> and contributors"]
-version = "0.3.5"
+version = "0.3.6"
 
 [deps]
 BitBasis = "50ba71b6-fa0f-514d-ae9a-0916efc90dcf"
@@ -28,7 +28,7 @@ JSON = "0.21.4"
 JuMP = "1"
 LinearAlgebra = "1"
 MLStyle = "0.4"
-PrettyTables = "2"
+PrettyTables = "3"
 julia = "1.10"
 
 [extras]

src/ProblemReductions.jl

@@ -16,11 +16,11 @@ export num_variables, num_flavors, variables, flavors, flavor_names, weights, se
 export UnitWeight
 
 # models
-export BooleanExpr, Circuit, Assignment, simple_form, CircuitSAT, @circuit, booleans, ¬, ∨, ∧, ⊻, is_literal, is_cnf, is_dnf
+export BooleanExpr, Circuit, Assignment, simple_form, CircuitSAT, CircuitSATHard, @circuit, booleans, ¬, ∨, ∧, ⊻, is_literal, is_cnf, is_dnf
 export SpinGlass, spinglass_gadget
-export Coloring, is_vertex_coloring
+export Coloring, ColoringHard, is_vertex_coloring
 export SetCovering, is_set_covering
-export BoolVar, CNFClause, CNF, AbstractSatisfiabilityProblem, Satisfiability, is_kSAT, satisfiable, KSatisfiability
+export BoolVar, CNFClause, CNF, AbstractSatisfiabilityProblem, Satisfiability, SatisfiabilityHard, is_kSAT, satisfiable, KSatisfiability, KSatisfiabilityHard
 export MaxCut
 export IndependentSet, is_independent_set
 export VertexCovering, is_vertex_covering

src/models/Circuit.jl

@@ -276,6 +276,11 @@ function CircuitSAT(circuit::Circuit; use_constraints::Bool=false)
     vars = symbols(simplified)
     CircuitSAT{OBJ}(simplified, vars, UnitWeight(length(simplified.exprs)))
 end
+const CircuitSATHard{T, WT} = CircuitSAT{T, WT, SAT} where {T, WT}
+function CircuitSATHard(sat::CircuitSAT)
+    return CircuitSAT{SAT}(sat.circuit, sat.symbols, sat.weights)
+end
+
 function Base.show(io::IO, x::CircuitSAT)
     println(io, "$(typeof(x)):")
     print_statements(io, x.circuit.exprs)

src/models/Coloring.jl

@@ -44,6 +44,11 @@ function Coloring{K}(graph::SimpleGraph{Int64}, weights::AbstractVector=UnitWeig
     OBJ = use_constraints ? SAT : EXTREMA
     return Coloring{K, OBJ}(graph, weights)
 end
+const ColoringHard{K, T, WT} = Coloring{K, T, WT, SAT} where {K, T, WT}
+function ColoringHard(c::Coloring{K}) where {K}
+    return Coloring{K, SAT}(c.graph, c.weights)
+end
+
 Base.:(==)(a::Coloring, b::Coloring) = a.graph == b.graph && a.weights == b.weights
 problem_size(c::Coloring) = (; num_vertices=nv(c.graph), num_edges=ne(c.graph))
 

src/models/Satisfiability.jl

@@ -162,6 +162,10 @@ function Satisfiability(cnf::CNF{S}, weights::AbstractVector=UnitWeight(length(c
     OBJ = use_constraints ? SAT : EXTREMA
     Satisfiability{OBJ}(symbols(cnf), cnf, weights)
 end
+const SatisfiabilityHard{S, T, WT} = Satisfiability{S, T, WT, SAT}
+function SatisfiabilityHard(sat::Satisfiability)
+    return Satisfiability{SAT}(sat.symbols, sat.cnf, sat.weights)
+end
 clauses(c::Satisfiability) = c.cnf.clauses
 num_variables(c::Satisfiability) = length(c.symbols)
 symbols(c::Satisfiability) = c.symbols
@@ -199,6 +203,10 @@ function KSatisfiability{K}(cnf::CNF{S}, weights::WT=UnitWeight(length(cnf.claus
     OBJ = use_constraints ? SAT : EXTREMA
     KSatisfiability{K, OBJ}(symbols(cnf), cnf, weights, allow_less)
 end
+const KSatisfiabilityHard{K, S, T, WT} = KSatisfiability{K, S, T, WT, SAT}
+function KSatisfiabilityHard(sat::KSatisfiability{K}) where {K}
+    return KSatisfiability{K, SAT}(sat.symbols, sat.cnf, sat.weights, sat.allow_less)
+end
 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)

src/models/models.jl

@@ -81,7 +81,7 @@ function Base.show(io::IO, spec::LocalConstraint)
     print(io, "LocalConstraint on $(spec.variables)\n")
     data = hcat(collect(combinations(spec.num_flavors, length(spec.variables))), spec.specification)
     header = ["Configuration", "Valid"]
-    pretty_table(io, data, header=header, alignment=:c)
+    pretty_table(io, data, column_labels=header, alignment=:c)
 end
 Base.show(io::IO, ::MIME"text/plain", spec::LocalConstraint) = show(io, spec)
 """
@@ -126,7 +126,7 @@ function Base.show(io::IO, spec::LocalSolutionSize{T}) where T
     print(io, "LocalSolutionSize{$T} on $(spec.variables)\n")
     data = hcat(collect(combinations(spec.num_flavors, length(spec.variables))), spec.specification)
     header = ["Configuration", "Size"]
-    pretty_table(io, data, header=header, alignment=:c)
+    pretty_table(io, data, column_labels=header, alignment=:c)
 end
 Base.show(io::IO, ::MIME"text/plain", spec::LocalSolutionSize) = show(io, spec)
 """

src/truth_table.jl

@@ -42,7 +42,7 @@ Base.show(io::IO, ::MIME"text/plain", tb::TruthTable) = show(io, tb)
 function Base.show(io::IO, tb::TruthTable)
     ni, no = length(tb.inputs), length(tb.outputs)
     entries = [Int(k > ni ? readbit(v, k-ni) : readbit(l-1, k)) for (l, v) in enumerate(tb.values), k in 1:ni+no]
-	pretty_table(io, entries; header=vcat(tb.inputs, tb.outputs))
+	pretty_table(io, entries; column_labels=vcat(tb.inputs, tb.outputs))
 	return nothing
 end
 

test/models/Circuit.jl

@@ -56,6 +56,8 @@ end
         d = x ∨ (c ∧ ¬z)
     end
     sat = CircuitSAT(circuit)
+    @test !(sat isa CircuitSATHard)
+    @test CircuitSATHard(sat) isa CircuitSATHard
     @test problem_size(sat) == (; num_exprs = 4, num_variables = 7)
     println(sat)
     @test sat.symbols[[1, 2, 3, 5, 7]] == [:c, :x, :y, :z, :d]

test/models/Coloring.jl

@@ -11,6 +11,8 @@ using Test, ProblemReductions, Graphs
     add_edge!(g, 3, 4)
     add_edge!(g, 4, 1)
     c = Coloring{3}(g, UnitWeight(nv(g)))
+    @test !(c isa ColoringHard)
+    @test ColoringHard(c) isa ColoringHard
     @test set_weights(c, [1, 2, 2, 1]) == Coloring{3}(g, [1, 2, 2, 1])
     c2 = Coloring{3}(g)
     @test c2 == c

test/models/Satisfiability.jl

@@ -12,6 +12,8 @@ using ProblemReductions: KSatisfiability,clauses
 
     cnf_test = CNF([clause1, clause2])
     sat_test = Satisfiability(cnf_test)
+    @test !(sat_test isa SatisfiabilityHard)
+    @test SatisfiabilityHard(sat_test) isa SatisfiabilityHard
     @test set_weights(sat_test, [1, 2]) == Satisfiability(CNF([clause1, clause2]), [1, 2])
 
     @test sat_test isa Satisfiability
@@ -39,6 +41,8 @@ using ProblemReductions: KSatisfiability,clauses
 
     # Tests for KSatisfiability
     ksat_test = KSatisfiability{3}(cnf_test)
+    @test !(ksat_test isa KSatisfiabilityHard)
+    @test KSatisfiabilityHard(ksat_test) isa KSatisfiabilityHard
     @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))))