Merge branch 'master' of https://github.com/hdavid16/DisjunctiveProgramming.jl

Author: hdavid16

Project.toml

@@ -1,7 +1,7 @@
 name = "DisjunctiveProgramming"
 uuid = "0d27d021-0159-4c7d-b4a7-9ccb5d9366cf"
 authors = ["hdavid16 <[email protected]>"]
-version = "0.2.1"
+version = "0.3.0"
 
 [deps]
 IntervalArithmetic = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253"

src/DisjunctiveProgramming.jl

@@ -4,6 +4,7 @@ using JuMP, IntervalArithmetic, Symbolics, Suppressor
 
 export add_disjunction!, add_proposition!, reformulate_disjunction
 export @disjunction, @proposition
+export choose!
 
 include("constraint.jl")
 include("logic.jl")

src/logic.jl

@@ -1,17 +1,39 @@
+"""
+    choose!(m::Model, n::Int, vars::VariableRef...; mode)
+
+Add constraint to select n elements from the list of variables. Options for mode
+are `:at_least`, `:at_most`, `:exactly`.
+"""
+function choose!(m::Model, n::Int, vars::VariableRef...; mode=:exactly)
+    @assert length(vars) >= n "Not enough variables passed."
+    @assert all(is_valid.(m, vars)) "Invalid VariableRefs passed."
+    add_selection!(m, n, vars...; mode)
+end
+function choose!(m::Model, vars::VariableRef...; mode=:exactly)
+    @assert all(is_valid.(m, vars)) "Invalid VariableRefs passed."
+    n = vars[1] #first variable is the n
+    add_selection!(m, n, vars...; mode)
+end
+function add_selection!(m::Model, n, vars::VariableRef...; mode::Symbol)
+    display(n)
+    if mode == :exactly
+        display(@constraint(m, sum(vars) == n))
+    elseif mode == :at_least
+        @constraint(m, sum(vars) ≥ n)
+    elseif mode == :at_most
+        @constraint(m, sum(vars) ≥ n)
+    end
+end
+
 """
     to_cnf!(m::Model, expr::Expr)
 
 Convert logical proposition expression into conjunctive normal form.
 """
 function to_cnf!(m::Model, expr::Expr)
-    expr_name = Symbol(expr) #get name to register reformulated logical proposition
+    expr_name = Symbol("{$expr}") #get name to register reformulated logical proposition
     replace_Symvars!(expr, m; logical_proposition = true) #replace all JuMP variables with Symbolic variables
-    check_logical_proposition(expr) #check that valid boolean symbols and variables are used in the logical proposition
-    eliminate_equivalence!(expr) #eliminate ⇔
-    eliminate_implication!(expr) #eliminmate ⇒
-    move_negations_inwards!(expr) #expand ¬
-    clause_list = distribute_and_over_or_recursively!(expr) #distribute ∧ over ∨ recursively
-    @assert !isempty(clause_list) "Conversion to CNF failed."
+    clause_list = to_cnf!(expr)
     #replace symbolic variables with JuMP variables and boolean operators with their algebraic counterparts
     for clause in clause_list
         replace_JuMPvars!(clause, m)
@@ -29,6 +51,22 @@ function to_cnf!(m::Model, expr::Expr)
     end
 end
 
+"""
+    to_cnf!(expr::Expr)
+
+Convert an expression of symbolic Boolean variables and operators to CNF.
+"""
+function to_cnf!(expr::Expr)
+    check_logical_proposition(expr) #check that valid boolean symbols and variables are used in the logical proposition
+    eliminate_equivalence!(expr) #eliminate ⇔
+    eliminate_implication!(expr) #eliminmate ⇒
+    move_negations_inwards!(expr) #expand ¬
+    clause_list = distribute_and_over_or_recursively!(expr) #distribute ∧ over ∨ recursively
+    @assert !isempty(clause_list) "Conversion to CNF failed."
+
+    return clause_list
+end
+
 """
     check_logical_proposition(expr::Expr)
 
@@ -53,11 +91,13 @@ function eliminate_equivalence!(expr)
     if expr isa Expr
         if expr.args[1] == :⇔
             @assert length(expr.args) == 3 "Double implication cannot have more than two clauses."
-            A = expr.args[2]
-            B = expr.args[3]
+            A1 = expr.args[2]
+            B1 = expr.args[3]
+            A2 = A1 isa Expr ? copy(A1) : A1
+            B2 = B1 isa Expr ? copy(B1) : B1
             expr.args[1] = :∧
-            expr.args[2] = :($A ⇒ $B)
-            expr.args[3] = :($B ⇒ $A)
+            expr.args[2] = :($A1 ⇒ $B1)
+            expr.args[3] = :($B2 ⇒ $A2)
         end
         for i in eachindex(expr.args)
             expr.args[i] = eliminate_equivalence!(expr.args[i])

src/macros.jl

@@ -50,14 +50,14 @@ macro disjunction(m, args...)
         end
     end
 
-    #XOR constraint name
-    xor_con = Symbol("XOR($disj_name)")
+    # #XOR constraint name
+    # xor_con = Symbol("XOR($disj_name)")
 
     #build disjunction
     code = quote
         @assert !in($name, keys(object_dictionary($m))) "The disjunction name $name is already registered in the model. Specify new name."
         $m[$name] = @variable($m, [eachindex($disjunction)], Bin, base_name = string($name), lower_bound = 0, upper_bound = 1)
-        @constraint($m, $xor_con, sum($m[$name]) == 1)
+        # @constraint($m, $xor_con, sum($m[$name]) == 1)
         reformulate_disjunction($m, $(disjunction...); bin_var = $name, reformulation = $reformulation, param = $param)
     end
 
@@ -114,15 +114,15 @@ function add_disjunction!(m::Model,disj...;reformulation::Symbol,M=missing,ϵ=1e
     bin_var = ismissing(name) ? Symbol("disj",gensym()) : name
     disj_name = ismissing(name) ? bin_var : Symbol("disj_",name)
 
-    #XOR constraint name
-    xor_con = "XOR($disj_name)"
+    # #XOR constraint name
+    # xor_con = "XOR($disj_name)"
 
     #apply reformulation
     @assert !in(bin_var, keys(object_dictionary(m))) "The disjunction name $bin_var is already registered in the model. Specify new name."
     #create indicator variable
     m[bin_var] = @variable(m, [eachindex(disj)], Bin, base_name = string(bin_var), lower_bound = 0, upper_bound = 1)
-    #add xor constraint on binary variable
-    m[Symbol(xor_con)] = @constraint(m, sum(m[bin_var]) == 1, base_name = xor_con)
+    # #add xor constraint on binary variable
+    # m[Symbol(xor_con)] = @constraint(m, sum(m[bin_var]) == 1, base_name = xor_con)
     #reformulate disjunction
     reformulate_disjunction(m, disj...; bin_var, reformulation, param)
 end
@@ -135,17 +135,7 @@ Add logical proposition macro.
 macro proposition(m, expr)
     #get args
     expr = QuoteNode(expr)
-    code = :(add_proposition!($m, $expr))
-
+    code = :(DisjunctiveProgramming.to_cnf!($m, $expr))
+    
     return esc(code)
 end
-
-"""
-    add_proposition!(m::Model, expr::Expr)
-
-Add logical proposition expression to a JuMP model.
-"""
-function add_proposition!(m::Model, expr::Expr)
-    @assert m isa Model "A valid JuMP Model must be provided."
-    to_cnf!(m, expr)
-end

src/reformulate.jl

@@ -30,7 +30,7 @@ function reformulate_disjunction(m::Model, disj...; bin_var, reformulation, para
     new_constraints = Dict{Symbol,Any}(
         Symbol(bin_var,"[$i]") => disj[i] for i in eachindex(disj)
     )
-    new_constraints[Symbol(bin_var,"_XOR")] = constraint_by_name(m, "XOR(disj_$bin_var)")
+    # new_constraints[Symbol(bin_var,"_XOR")] = constraint_by_name(m, "XOR(disj_$bin_var)")
     if reformulation == :hull
         for var in m[:gdp_variable_refs]
             agg_con_name = "$(var)_$(bin_var)_aggregation"