Skip to content

Commit

Permalink
add support for exact
Browse files Browse the repository at this point in the history
  • Loading branch information
@Wout4
Wout4 committed May 16, 2024
1 parent cb22ee9 commit df746db
Show file tree
Hide file tree
Showing 3 changed files with 133 additions and 90 deletions.
2 changes: 1 addition & 1 deletion benchmarks/results.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
slowthreshold = 0.2
fastthreshold = 0.2
#filename of reference instance, should be in results folder!
refname = 'main_ortools_2024-05-16 13.55.25.615425.csv'
refname = 'main_ortools_2024-05-16 14.17.52.619920.csv'

results = []
cwd = os.getcwd()
Expand Down
14 changes: 11 additions & 3 deletions benchmarks/run_benchmarks.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@
os.rename(xmlmodel, xmlmodel[:len(xmlmodel) - len(name)] + 'unsupported\\' + name)
'''
print(xmlmodels)
for xmlmodel in xmlmodels[:10]:
for xmlmodel in xmlmodels[:2]:
model = None
def parse():
parser = ParserXCSP3(xmlmodel)
Expand Down Expand Up @@ -82,12 +82,16 @@ def solv():
timings = s.timings
timings['solve'] = t_solve
timings['parse'] = t_parse
for opt in ['parse', 'decompose', 'flatten', 'reify', 'only_numexpr', 'only_bv', 'only_implies', 'linearize', 'only_pos_bv', 'get_vars', 'post_cons', 'solve']:
if opt not in timings:
# add unused transformations
timings[opt] = 0
alltimes[xmlmodel] = timings


import pandas as pd
# Maak een lege DataFrame aan
df = pd.DataFrame(columns=['parse', 'decompose', 'flatten', 'reify', 'only_numexpr', 'only_bv', 'only_implies', 'get_vars', 'post_cons', 'solve'])
df = pd.DataFrame(columns=['parse', 'decompose', 'flatten', 'reify', 'only_numexpr', 'only_bv', 'only_implies', 'linearize', 'only_pos_bv', 'get_vars', 'post_cons', 'solve'])
dfs = []
for instance, values in alltimes.items():
instance_df = pd.DataFrame({
Expand All @@ -98,6 +102,8 @@ def solv():
'only_numexpr': [values['only_numexpr']],
'only_bv': [values['only_bv']],
'only_implies': [values['only_implies']],
'linearize': [values['linearize']],
'only_pos_bv': [values['only_pos_bv']],
'get_vars': [values['get_vars']],
'post_cons': [values['post_cons']],
'solve': [values['solve']]
Expand All @@ -106,13 +112,15 @@ def solv():

df = pd.concat(dfs, ignore_index=False)
total = pd.DataFrame({
'parse': [df['parse']],
'parse': [df['parse'].sum()],
'decompose': [df['decompose'].sum()],
'flatten': [df['flatten'].sum()],
'reify': [df['reify'].sum()],
'only_numexpr': [df['only_numexpr'].sum()],
'only_bv': [df['only_bv'].sum()],
'only_implies': [df['only_implies'].sum()],
'linearize': [df['linearize'].sum()],
'only_pos_bv': [df['only_pos_bv'].sum()],
'get_vars': [df['get_vars'].sum()],
'post_cons': [df['post_cons'].sum()],
'solve': [df['solve'].sum()]
Expand Down
207 changes: 121 additions & 86 deletions cpmpy/solvers/exact.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,7 @@ def __init__(self, cpm_model=None, subsolver=None):
# for domain sizes > 10, the most efficient one is probably "log", so that is the default.
# "onehot" is less efficient, but required to prune domains with Exact (TODO: implement this).
self.encoding="log"
self.timings = None

# initialise everything else and post the constraints/objective
super().__init__(name="exact", cpm_model=cpm_model)
Expand Down Expand Up @@ -407,20 +408,45 @@ def transform(self, cpm_expr):
:return: list of Expression
"""

import timeit
global cpm_cons
# apply transformations, then post internally
# expressions have to be linearized to fit in MIP model. See /transformations/linearize
cpm_cons = toplevel_list(cpm_expr)
cpm_cons = decompose_in_tree(cpm_cons, supported=frozenset({'alldifferent'})) # Alldiff has a specialzed MIP decomp
cpm_cons = flatten_constraint(cpm_cons) # flat normal form
cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) # constraints that support reification
cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum"])) # supports >, <, !=
cpm_cons = only_bv_reifies(cpm_cons)
cpm_cons = only_implies(cpm_cons) # anything that can create full reif should go above...
cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum"})) # the core of the MIP-linearization
cpm_cons = only_positive_bv(cpm_cons) # after linearisation, rewrite ~bv into 1-bv
return cpm_cons

def decompose():
global cpm_cons
cpm_cons = decompose_in_tree(cpm_cons, supported=frozenset({'alldifferent'})) # Alldiff has a specialzed MIP decomp
def flatten():
global cpm_cons
cpm_cons = flatten_constraint(cpm_cons) # flat normal form
def reify():
global cpm_cons
cpm_cons = reify_rewrite(cpm_cons, supported=frozenset(['sum', 'wsum'])) # constraints that support reification
def only_num():
global cpm_cons
cpm_cons = only_numexpr_equality(cpm_cons, supported=frozenset(["sum", "wsum"])) # supports >, <, !=
def only_bv():
global cpm_cons
cpm_cons = only_bv_reifies(cpm_cons)
def only_impl():
global cpm_cons
cpm_cons = only_implies(cpm_cons) # anything that can create full reif should go above...
def linear():
global cpm_cons
cpm_cons = linearize_constraint(cpm_cons, supported=frozenset({"sum","wsum"})) # the core of the MIP-linearization
def only_pos():
global cpm_cons
cpm_cons = only_positive_bv(cpm_cons) # after linearisation, rewrite ~bv into 1-bv

t_decomp = timeit.timeit(stmt=decompose, number=1)
t_flatten = timeit.timeit(stmt=flatten, number=1)
t_reify = timeit.timeit(stmt=reify, number=1)
t_only_num = timeit.timeit(stmt=only_num, number=1)
t_only_bv = timeit.timeit(stmt=only_bv, number=1)
t_only_impl = timeit.timeit(stmt=only_impl, number=1)
t_linear = timeit.timeit(stmt=linear, number=1)
t_only_pos = timeit.timeit(stmt=only_pos, number=1)
return cpm_cons, t_decomp, t_flatten, t_reify, t_only_num, t_only_bv, t_only_impl, t_linear, t_only_pos
# NOTE: the transformations that are still done specifically for Exact are two-fold:
# 1) transform '==' and '<=' to '>='
# 2) transform implications with negative conditions to ones with positive consequences
Expand Down Expand Up @@ -484,94 +510,103 @@ def __add__(self, cpm_expr_orig):
:return: self
"""
from exact import Exact as xct
import timeit

# add new user vars to the set
get_variables(cpm_expr_orig, collect=self.user_vars)
def get_vars():
get_variables(cpm_expr_orig, collect=self.user_vars)
t_getvars = timeit.timeit(stmt=get_vars, number=1)

cons, t_decomp, t_flatten, t_reify, t_only_num, t_only_bv, t_only_impl, t_linear, t_only_pos = self.transform(cpm_expr_orig)

# transform and post the constraints
for cpm_expr in self.transform(cpm_expr_orig):
# Comparisons: only numeric ones as 'only_implies()' has removed the '==' reification for Boolean expressions
# numexpr `comp` bvar|const
if isinstance(cpm_expr, Comparison):
lhs, rhs = cpm_expr.args
xct_coefs, xct_vars, xct_rhs = self._make_numexpr(lhs,rhs)

# linearize removed '<', '>' and '!='
if cpm_expr.name == '<=':
self._add_xct_constr(xct_coefs, xct_vars, False, 0, True, xct_rhs)
elif cpm_expr.name == '>=':
self._add_xct_constr(xct_coefs, xct_vars, True, xct_rhs, False, 0)
elif cpm_expr.name == '==':
# a BoundedLinearExpression LHS, special case, like in objective
self._add_xct_constr(xct_coefs, xct_vars, True, xct_rhs, True, xct_rhs)
else:
raise NotImplementedError(
"Constraint not supported by Exact '{}' {}".format(lhs.name, cpm_expr))
def post_cons():
for cpm_expr in cons:
# Comparisons: only numeric ones as 'only_implies()' has removed the '==' reification for Boolean expressions
# numexpr `comp` bvar|const
if isinstance(cpm_expr, Comparison):
lhs, rhs = cpm_expr.args
xct_coefs, xct_vars, xct_rhs = self._make_numexpr(lhs,rhs)

# linearize removed '<', '>' and '!='
if cpm_expr.name == '<=':
self._add_xct_constr(xct_coefs, xct_vars, False, 0, True, xct_rhs)
elif cpm_expr.name == '>=':
self._add_xct_constr(xct_coefs, xct_vars, True, xct_rhs, False, 0)
elif cpm_expr.name == '==':
# a BoundedLinearExpression LHS, special case, like in objective
self._add_xct_constr(xct_coefs, xct_vars, True, xct_rhs, True, xct_rhs)
else:
raise NotImplementedError(
"Constraint not supported by Exact '{}' {}".format(lhs.name, cpm_expr))

elif isinstance(cpm_expr, Operator) and cpm_expr.name == "->":
# Indicator constraints
# Take form bvar -> sum(x,y,z) >= rvar
cond, sub_expr = cpm_expr.args
assert isinstance(cond, _BoolVarImpl), f"Implication constraint {cpm_expr} must have BoolVar as lhs"
assert isinstance(sub_expr, Comparison), "Implication must have linear constraints on right hand side"
elif isinstance(cpm_expr, Operator) and cpm_expr.name == "->":
# Indicator constraints
# Take form bvar -> sum(x,y,z) >= rvar
cond, sub_expr = cpm_expr.args
assert isinstance(cond, _BoolVarImpl), f"Implication constraint {cpm_expr} must have BoolVar as lhs"
assert isinstance(sub_expr, Comparison), "Implication must have linear constraints on right hand side"

lhs, rhs = sub_expr.args
lhs, rhs = sub_expr.args

xct_coefs, xct_vars, xct_rhs = self._make_numexpr(lhs,rhs)
xct_coefs, xct_vars, xct_rhs = self._make_numexpr(lhs,rhs)

if isinstance(cond, NegBoolView):
cond, bool_val = self.solver_var(cond._bv), False
else:
cond, bool_val = self.solver_var(cond), True

if sub_expr.name == "==":
if bool_val:
# a -> b==c
# a -> b>=c and a -> -b>=-c
self._add_xct_reif_right(cond, xct_coefs,xct_vars,xct_rhs)
self._add_xct_reif_right(cond, [-x for x in xct_coefs],xct_vars,-xct_rhs)
if isinstance(cond, NegBoolView):
cond, bool_val = self.solver_var(cond._bv), False
else:
# !a -> b==c
# !a -> b>=c and !a -> -b>=-c
# a <- b<c and a <- -b<-c
# a <- -b>=1-c and a <- b>=1+c
self._add_xct_reif_left(cond, xct_coefs,xct_vars,1+xct_rhs)
self._add_xct_reif_left(cond, [-x for x in xct_coefs],xct_vars,1-xct_rhs)
elif sub_expr.name == ">=":
if bool_val:
# a -> b >= c
self._add_xct_reif_right(cond, xct_coefs,xct_vars,xct_rhs)
cond, bool_val = self.solver_var(cond), True

if sub_expr.name == "==":
if bool_val:
# a -> b==c
# a -> b>=c and a -> -b>=-c
self._add_xct_reif_right(cond, xct_coefs,xct_vars,xct_rhs)
self._add_xct_reif_right(cond, [-x for x in xct_coefs],xct_vars,-xct_rhs)
else:
# !a -> b==c
# !a -> b>=c and !a -> -b>=-c
# a <- b<c and a <- -b<-c
# a <- -b>=1-c and a <- b>=1+c
self._add_xct_reif_left(cond, xct_coefs,xct_vars,1+xct_rhs)
self._add_xct_reif_left(cond, [-x for x in xct_coefs],xct_vars,1-xct_rhs)
elif sub_expr.name == ">=":
if bool_val:
# a -> b >= c
self._add_xct_reif_right(cond, xct_coefs,xct_vars,xct_rhs)
else:
# !a -> b>=c
# a <- b<c
# a <- -b>=1-c
self._add_xct_reif_left(cond, [-x for x in xct_coefs],xct_vars,1-xct_rhs)
elif sub_expr.name == "<=":
if bool_val:
# a -> b=<c
# a -> -b>=-c
self._add_xct_reif_right(cond, [-x for x in xct_coefs],xct_vars,-xct_rhs)
else:
# !a -> b=<c
# a <- b>c
# a <- b>=1+c
self._add_xct_reif_left(cond, xct_coefs,xct_vars,1+xct_rhs)
else:
# !a -> b>=c
# a <- b<c
# a <- -b>=1-c
self._add_xct_reif_left(cond, [-x for x in xct_coefs],xct_vars,1-xct_rhs)
elif sub_expr.name == "<=":
if bool_val:
# a -> b=<c
# a -> -b>=-c
self._add_xct_reif_right(cond, [-x for x in xct_coefs],xct_vars,-xct_rhs)
else:
# !a -> b=<c
# a <- b>c
# a <- b>=1+c
self._add_xct_reif_left(cond, xct_coefs,xct_vars,1+xct_rhs)
else:
raise NotImplementedError(
"Unexpected condition constraint for Exact '{}' {}".format(lhs.name,cpm_expr))
raise NotImplementedError(
"Unexpected condition constraint for Exact '{}' {}".format(lhs.name,cpm_expr))

# True or False
elif isinstance(cpm_expr, BoolVal):
self._add_xct_constr([], [], True, 0 if cpm_expr.args[0] else 1, False, 0)
# True or False
elif isinstance(cpm_expr, BoolVal):
self._add_xct_constr([], [], True, 0 if cpm_expr.args[0] else 1, False, 0)

# a direct constraint, pass to solver
elif isinstance(cpm_expr, DirectConstraint):
cpm_expr.callSolver(self, self.xct_solver)
return self
# a direct constraint, pass to solver
elif isinstance(cpm_expr, DirectConstraint):
cpm_expr.callSolver(self, self.xct_solver)
return self

else:
raise NotImplementedError(cpm_expr) # if you reach this... please report on github

else:
raise NotImplementedError(cpm_expr) # if you reach this... please report on github

t_post = timeit.timeit(stmt=post_cons, number=1)
self.timings = {'decompose': t_decomp, 'flatten': t_flatten, 'reify': t_reify, 'only_numexpr': t_only_num,
'only_bv': t_only_bv, 'only_implies': t_only_impl, 'linearize': t_linear, 'only_pos_bv': t_only_pos, 'get_vars': t_getvars, 'post_cons': t_post}
return self

def get_core(self):
Expand Down

0 comments on commit df746db

Please sign in to comment.