From cf6557de506478c660f8c84f1556dda8e40b139a Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Mon, 22 Sep 2025 23:44:13 +0800 Subject: [PATCH] update --- Project.toml | 4 ++-- src/ProblemReductions.jl | 6 +++--- src/models/Circuit.jl | 5 +++++ src/models/Coloring.jl | 5 +++++ src/models/Satisfiability.jl | 8 ++++++++ src/models/models.jl | 4 ++-- src/truth_table.jl | 2 +- test/models/Circuit.jl | 2 ++ test/models/Coloring.jl | 2 ++ test/models/Satisfiability.jl | 4 ++++ 10 files changed, 34 insertions(+), 8 deletions(-) diff --git a/Project.toml b/Project.toml index c01bce33..65ab1235 100644 --- a/Project.toml +++ b/Project.toml @@ -1,7 +1,7 @@ name = "ProblemReductions" uuid = "899c297d-f7d2-4ebf-8815-a35996def416" authors = ["GiggleLiu 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] diff --git a/src/ProblemReductions.jl b/src/ProblemReductions.jl index 82c6a866..4e409da8 100644 --- a/src/ProblemReductions.jl +++ b/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 diff --git a/src/models/Circuit.jl b/src/models/Circuit.jl index fce03578..919bedbd 100644 --- a/src/models/Circuit.jl +++ b/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) diff --git a/src/models/Coloring.jl b/src/models/Coloring.jl index 8fcca01e..30a80f2c 100644 --- a/src/models/Coloring.jl +++ b/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)) diff --git a/src/models/Satisfiability.jl b/src/models/Satisfiability.jl index aca3be26..1d15b523 100644 --- a/src/models/Satisfiability.jl +++ b/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) diff --git a/src/models/models.jl b/src/models/models.jl index 5d04fd8d..c0f1c3a6 100644 --- a/src/models/models.jl +++ b/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) """ diff --git a/src/truth_table.jl b/src/truth_table.jl index 7c6a6e27..ba2049ed 100644 --- a/src/truth_table.jl +++ b/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 diff --git a/test/models/Circuit.jl b/test/models/Circuit.jl index c5739393..aef6610d 100644 --- a/test/models/Circuit.jl +++ b/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] diff --git a/test/models/Coloring.jl b/test/models/Coloring.jl index 6fb26bf1..f8ef6730 100644 --- a/test/models/Coloring.jl +++ b/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 diff --git a/test/models/Satisfiability.jl b/test/models/Satisfiability.jl index e37d6782..1040e9cb 100644 --- a/test/models/Satisfiability.jl +++ b/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))))