Add Statisfiability Problem (#37)

* Add Statisfiability Problem

* Fix the Test file

* Change the test method for variables function

* Generic is_kSAT function

* Change variables and num_variables function: dispatch is_kSAT

* Fix return type issue of is_kSAT function; Change test file; Evaluate function not included

* Delete test for terms function

* Delete doctest (under development); Evaluate function needed

* fix sat (#1)

---------

Co-authored-by: Jinguo Liu <cacate0129@gmail.com>

CITATION.bib

@@ -0,0 +1,30 @@
+@ARTICLE{Liu2022Computing,
+       author = {{Liu}, Jin-Guo and {Gao}, Xun and {Cain}, Madelyn and {Lukin}, Mikhail D. and {Wang}, Sheng-Tao},
+        title = "{Computing solution space properties of combinatorial optimization problems via generic tensor networks}",
+      journal = {arXiv e-prints},
+     keywords = {Condensed Matter - Statistical Mechanics},
+         year = 2022,
+        month = may,
+          eid = {arXiv:2205.03718},
+        pages = {arXiv:2205.03718},
+archivePrefix = {arXiv},
+       eprint = {2205.03718},
+ primaryClass = {cond-mat.stat-mech},
+       adsurl = {https://ui.adsabs.harvard.edu/abs/2022arXiv220503718L},
+      adsnote = {Provided by the SAO/NASA Astrophysics Data System}
+}
+
+@article{Ebadi_2022,
+	doi = {10.1126/science.abo6587},
+	url = {https://doi.org/10.1126%2Fscience.abo6587},
+	year = 2022,
+	month = {jun},
+	publisher = {American Association for the Advancement of Science ({AAAS})},
+	volume = {376},
+	number = {6598},
+	pages = {1209--1215},
+	author = {S. Ebadi and A. Keesling and M. Cain and T. T. Wang and H. Levine and D. Bluvstein and G. Semeghini and A. Omran and J.-G. Liu and R. Samajdar and X.-Z. Luo and B. Nash and X. Gao and B. Barak and E. Farhi and S. Sachdev and N. Gemelke and L. Zhou and S. Choi and H. Pichler and S.-T. Wang and M. Greiner and V. Vuleti{\'{c}
+} and M. D. Lukin},
+	title = {Quantum optimization of maximum independent set using Rydberg atom arrays},
+	journal = {Science}
+}

src/ProblemReductions.jl

@@ -21,6 +21,7 @@ export target_problem, AbstractProblem, AbstractReductionResult, reduceto, extra
 export LogicGadget, truth_table
 export spinglass_circuit, ReductionCircuitToSpinGlass
 export findbest, BruteForce
+export CNF
 
 include("truth_table.jl")
 include("topology.jl")

src/models/Satisfiability.jl

@@ -0,0 +1,161 @@
+"""
+Basic useful functions for Boolean algebra (https://github.com/QuEraComputing/GenericTensorNetworks.jl/blob/master/src/networks/Satisfiability.jl)
+"""
+
+"""
+    BoolVar{T}
+    BoolVar(name, neg)
+
+Boolean variable for constructing CNF clauses.
+"""
+struct BoolVar{T}
+    name::T
+    neg::Bool
+end
+BoolVar(name) = BoolVar(name, false)
+function Base.show(io::IO, b::BoolVar)
+    b.neg && print(io, "¬")
+    print(io, b.name)
+end
+
+"""
+    CNFClause{T}
+    CNFClause(vars)
+
+A clause in [`CNF`](@ref), its value is the logical or of `vars`, where `vars` is a vector of [`BoolVar`](@ref).
+"""
+struct CNFClause{T}
+    vars::Vector{BoolVar{T}}
+end
+function Base.show(io::IO, b::CNFClause)
+    print(io, join(string.(b.vars), " ∨ "))
+end
+Base.:(==)(x::CNFClause, y::CNFClause) = x.vars == y.vars
+Base.length(x::CNFClause) = length(x.vars)
+
+"""
+    CNF{T}
+    CNF(clauses)
+
+Boolean expression in [conjunctive normal form](https://en.wikipedia.org/wiki/Conjunctive_normal_form).
+`clauses` is a vector of [`CNFClause`](@ref), if and only if all clauses are satisfied, this CNF is satisfied.
+
+Example
+------------------------
+Under development
+"""
+struct CNF{T}
+    clauses::Vector{CNFClause{T}}
+end
+function Base.show(io::IO, c::CNF)
+    print(io, join(["($k)" for k in c.clauses], " ∧ "))
+end
+Base.:(==)(x::CNF, y::CNF) = x.clauses == y.clauses
+Base.length(x::CNF) = length(x.clauses)
+
+"""
+    ¬(var::BoolVar)
+
+Negation of a boolean variables of type [`BoolVar`](@ref).
+"""
+¬(var::BoolVar{T}) where T = BoolVar(var.name, ~var.neg)
+
+"""
+    ∨(vars...)
+
+Logical `or` applied on [`BoolVar`](@ref) and [`CNFClause`](@ref).
+Returns a [`CNFClause`](@ref).
+"""
+∨(var::BoolVar{T}, vars::BoolVar{T}...) where T = CNFClause([var, vars...])
+∨(c::CNFClause{T}, var::BoolVar{T}) where T = CNFClause([c.vars..., var])
+∨(c::CNFClause{T}, d::CNFClause{T}) where T = CNFClause([c.vars..., d.vars...])
+∨(var::BoolVar{T}, c::CNFClause) where T = CNFClause([var, c.vars...])
+
+
+"""
+    ∧(vars...)
+
+Logical `and` applied on [`CNFClause`](@ref) and [`CNF`](@ref).
+Returns a new [`CNF`](@ref).
+"""
+∧(c::CNFClause{T}, cs::CNFClause{T}...) where T = CNF([c, cs...])
+∧(c::CNFClause{T}, cs::CNF{T}) where T = CNF([c, cs.clauses...])
+∧(cs::CNF{T}, c::CNFClause{T}) where T = CNF([cs.clauses..., c])
+∧(cs::CNF{T}, ds::CNF{T}) where T = CNF([cs.clauses..., ds.clauses...])
+
+"""
+    @bools(syms::Symbol...)
+
+Create some boolean variables of type [`BoolVar`](@ref) in current scope that can be used in create a [`CNF`](@ref).
+
+Example
+------------------------
+Under Development
+"""
+macro bools(syms::Symbol...)
+    esc(Expr(:block, [:($s = $BoolVar($(QuoteNode(s)))) for s in syms]..., nothing))
+end
+
+
+"""
+The formal definition of SAT problem
+
+The [satisfiability](https://queracomputing.github.io/GenericTensorNetworks.jl/dev/generated/Satisfiability/) problem.
+
+Positional arguments
+-------------------------------
+* `cnf` is a conjunctive normal form ([`CNF`](@ref)) for specifying the satisfiability problems.
+* `weights` are associated with clauses.
+
+Examples
+-------------------------------
+Under Development
+"""
+struct Satisfiability{T} <:AbstractProblem
+    cnf::CNF{T}
+    function Satisfiability(cnf::CNF{T}) where {T}
+        new{T}(cnf)
+    end
+end
+
+struct KSatisfiability{K, T} <:AbstractProblem
+    cnf::CNF{T}
+    function KSatisfiability{K}(cnf::CNF{T}) where {K, T}
+        @assert is_kSAT(cnf, K) "The CNF is not a $K-SAT problem"
+        new{K, T}(cnf)
+    end
+end
+is_kSAT(cnf::CNF, k::Int) = all(c -> k == length(c.vars), cnf.clauses)
+
+function variables(c::Satisfiability{T}) where T
+    var_names = T[]
+    for clause in c.cnf.clauses
+        for var in clause.vars
+            push!(var_names, var.name)
+        end
+    end
+    return unique(var_names)
+end
+num_variables(c::Satisfiability) = length(variables(c))
+flavors(::Type{<:Satisfiability}) = [0, 1]  # false, true
+
+function evaluate(c::Satisfiability, config)
+    @assert length(config) == num_variables(c)
+    dict = Dict(zip(variables(c), config))
+    count(x->!satisfiable(x, dict), c.cnf.clauses)
+end
+
+"""
+    satisfiable(cnf::CNF, config::AbstractDict)
+
+Returns true if an assignment of variables satisfies a [`CNF`](@ref).
+"""
+function satisfiable(cnf::CNF{T}, config::AbstractDict{T}) where T
+    all(x->satisfiable(x, config), cnf.clauses)
+end
+function satisfiable(c::CNFClause{T}, config::AbstractDict{T}) where T
+    any(x->satisfiable(x, config), c.vars)
+end
+function satisfiable(v::BoolVar{T}, config::AbstractDict{T}) where T
+    config[v.name] == ~v.neg
+end

src/models/models.jl

@@ -93,4 +93,5 @@ Base.eltype(::UnitWeight) = Int
 include("SpinGlass.jl")
 include("Circuit.jl")
 include("Coloring.jl")
+include("Satisfiability.jl")
 include("SetCovering.jl")

test/models/Satisfiability.jl

@@ -0,0 +1,34 @@
+using ProblemReductions, Test, Graphs
+using ProblemReductions: BoolVar, CNFClause, CNF, Satisfiability, is_kSAT, variables, satisfiable
+
+@testset "satisfiability" begin
+    bv1 = BoolVar("x")
+    bv2 = BoolVar("y")
+    bv3 = BoolVar("z", true)    
+
+    clause1 = CNFClause([bv1, bv2, bv3])
+    clause2 = CNFClause([BoolVar("w"), bv1, BoolVar("x", true)])
+
+    cnf_test = CNF([clause1, clause2])
+
+    sat_test = Satisfiability(cnf_test)
+
+    @test sat_test isa Satisfiability
+    @test is_kSAT(sat_test.cnf, 3)
+    vars = ["x", "y", "z", "w"]
+    @test variables(sat_test) == vars
+    @test num_variables(sat_test) == 4
+
+    cfg = [1, 1, 1, 1]
+    assignment = Dict(zip(vars, cfg))
+    @test satisfiable(sat_test.cnf, assignment) == true
+    @test evaluate(sat_test, cfg) == 0
+
+    cfg = [0, 0, 1, 0]
+    assignment = Dict(zip(vars, cfg))
+    @test satisfiable(sat_test.cnf, assignment) == false
+    @test evaluate(sat_test, cfg) == 1
+
+    res = findbest(sat_test, BruteForce())
+    @test length(res) == 14
+end

test/models/models.jl

@@ -12,6 +12,10 @@ end
     include("Coloring.jl")
 end
 
+@testset "Satisfiability" begin
+    include("Satisfiability.jl")
+end
+
 @testset "SetCovering" begin
     include("SetCovering.jl")
 end