Skip to content

Commit

Permalink
Merge pull request #216 from Crypto-TII/add_method_to_get_MILP_solver…
Browse files Browse the repository at this point in the history
…_names

Add method to get milp solver names
  • Loading branch information
peacker authored Apr 5, 2024
2 parents 77e0391 + a671af4 commit cb28bed
Show file tree
Hide file tree
Showing 15 changed files with 188 additions and 104 deletions.
72 changes: 50 additions & 22 deletions claasp/cipher_modules/models/milp/milp_model.py
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,8 @@

from sage.numerical.mip import MixedIntegerLinearProgram, MIPSolverException

from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT, get_external_milp_solver_configuration
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT, MODEL_DEFAULT_PATH, MILP_SOLVERS_EXTERNAL, \
MILP_SOLVERS_INTERNAL
from claasp.cipher_modules.models.milp.utils.utils import _get_data, _parse_external_solver_output, _write_model_to_lp_file
from claasp.cipher_modules.models.utils import convert_solver_solution_to_dictionary

Expand Down Expand Up @@ -256,24 +257,30 @@ def init_model_in_sage_milp_class(self, solver_name=SOLVER_DEFAULT):
sage: milp._model
Mixed Integer Program (no objective, 0 variables, 0 constraints)
"""
if solver_name.upper().endswith("_EXT"):
solver_name = SOLVER_DEFAULT
self._model = MixedIntegerLinearProgram(maximization=False, solver=solver_name)
self._binary_variable = self._model.new_variable(binary=True)
self._integer_variable = self._model.new_variable(integer=True)
self._non_linear_component_id = []

def _solve_with_external_solver(self, model_type, model_path, solver_name=SOLVER_DEFAULT):

solvers_configuration = get_external_milp_solver_configuration(f'{model_path[:-3]}.sol')
if solver_name not in solvers_configuration:
raise ValueError(f"Invalid solver name: {solver_name}."
f"Currently supported solvers are 'Gurobi', 'cplex', 'scip' and 'glpk'.")

solver_specs = solvers_configuration[solver_name]
command = solver_specs['command']
options = solver_specs['options']
tracemalloc.start()
solver_specs = [specs for specs in MILP_SOLVERS_EXTERNAL if specs["solver_name"] == solver_name.upper()][0]
solution_file_path = f'{MODEL_DEFAULT_PATH}/{model_path[:-3]}.sol'

command += model_path + options
command = ""
for key in solver_specs['keywords']['command']['format']:
parameter = solver_specs['keywords']['command'][key]
if key == "input_file":
parameter += " " + model_path
elif key == "output_file":
parameter = parameter + solution_file_path if parameter.endswith('=') else parameter + " " + solution_file_path
elif key == "options":
parameter = " ".join(parameter)
command += " " + parameter
tracemalloc.start()
solver_process = subprocess.run(command, capture_output=True, shell=True, text=True)
milp_memory = tracemalloc.get_traced_memory()[1] / 10 ** 6
tracemalloc.stop()
Expand All @@ -282,29 +289,29 @@ def _solve_with_external_solver(self, model_type, model_path, solver_name=SOLVER
raise MIPSolverException("Make sure that the solver is correctly installed.")

if 'memory' in solver_specs:
milp_memory = _get_data(solver_specs['memory'], str(solver_process))
milp_memory = _get_data(solver_specs['keywords']['memory'], str(solver_process))

return _parse_external_solver_output(self, solvers_configuration, model_type, solver_name, solver_process) + (milp_memory,)
return _parse_external_solver_output(self, solver_specs, model_type, solution_file_path, solver_process.stdout) + (milp_memory,)

def _solve_with_internal_solver(self):

mip = self._model

status = 'UNSATISFIABLE'
self._verbose_print("Solving model in progress ...")
time_start = time.time()
tracemalloc.start()
try:
mip.solve()
status = 'SATISFIABLE'

except MIPSolverException as milp_exception:
print(milp_exception)
finally:
milp_memory = tracemalloc.get_traced_memory()[1] / 10 ** 6
tracemalloc.stop()
time_end = time.time()
milp_time = time_end - time_start
self._verbose_print(f"Time for solving the model = {milp_time}")
status = 'SATISFIABLE'

except MIPSolverException as milp_exception:
status = 'UNSATISFIABLE'
print(milp_exception)

return status, milp_time, milp_memory

Expand All @@ -329,23 +336,44 @@ def solve(self, model_type, solver_name=SOLVER_DEFAULT, external_solver_name=Non
...
sage: solution = milp.solve("xor_differential") # random
"""
if external_solver_name:
solver_name_in_solution = external_solver_name
if external_solver_name or (solver_name.upper().endswith("_EXT")):
solver_choice = external_solver_name or solver_name
if solver_choice.upper() not in [specs["solver_name"] for specs in MILP_SOLVERS_EXTERNAL]:
raise ValueError(f"Invalid solver name: {solver_choice}.\n"
f"Please select a solver in the following list: {[specs['solver_name'] for specs in MILP_SOLVERS_EXTERNAL]}.")

solver_name_in_solution = solver_choice
model_path = _write_model_to_lp_file(self, model_type)
solution_file_path, status, objective_value, components_values, milp_time, milp_memory = self._solve_with_external_solver(
model_type, model_path, external_solver_name)
model_type, model_path, solver_choice)
os.remove(model_path)
os.remove(f"{solution_file_path}")
else:
objective_value = None
components_values = None
solver_name_in_solution = solver_name
status, milp_time, milp_memory = self._solve_with_internal_solver()
objective_value, components_values = self._parse_solver_output()
if status == 'SATISFIABLE':
objective_value, components_values = self._parse_solver_output()

solution = convert_solver_solution_to_dictionary(self._cipher, model_type, solver_name_in_solution, milp_time,
milp_memory, components_values, objective_value)
solution['status'] = status
return solution

def solver_names(self, verbose=False):
solver_names = []

keys = ['solver_brand_name', 'solver_name']
for solver in MILP_SOLVERS_INTERNAL:
solver_names.append({key: solver[key] for key in keys})
if verbose:
keys = ['solver_brand_name', 'solver_name', 'keywords']

for solver in MILP_SOLVERS_EXTERNAL:
solver_names.append({key: solver[key] for key in keys})
return solver_names

@property
def binary_variable(self):
return self._binary_variable
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
# ****************************************************************************

import time
from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_BITWISE_DETERMINISTIC_TRUNCATED, \
MILP_BACKWARD_SUFFIX, MILP_BUILDING_MESSAGE, MILP_TRUNCATED_XOR_DIFFERENTIAL_OBJECTIVE
from claasp.cipher_modules.models.milp.utils.milp_truncated_utils import \
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
import time

from claasp.cipher_modules.inverse_cipher import get_key_schedule_component_ids
from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.milp_models.milp_bitwise_deterministic_truncated_xor_differential_model import \
MilpBitwiseDeterministicTruncatedXorDifferentialModel
from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_BITWISE_IMPOSSIBLE, \
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
# ****************************************************************************

import time
from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.milp_model import MilpModel
from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_WORDWISE_DETERMINISTIC_TRUNCATED, \
MILP_BUILDING_MESSAGE, MILP_TRUNCATED_XOR_DIFFERENTIAL_OBJECTIVE
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
import time

from claasp.cipher_modules.inverse_cipher import get_key_schedule_component_ids
from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.milp_models.milp_wordwise_deterministic_truncated_xor_differential_model import MilpWordwiseDeterministicTruncatedXorDifferentialModel
from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_WORDWISE_IMPOSSIBLE_AUTO, \
MILP_WORDWISE_IMPOSSIBLE, MILP_BACKWARD_SUFFIX, MILP_BUILDING_MESSAGE
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@

from bitstring import BitArray

from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.milp_model import MilpModel
from claasp.cipher_modules.models.milp.utils.milp_name_mappings import MILP_XOR_DIFFERENTIAL, MILP_PROBABILITY_SUFFIX, \
MILP_BUILDING_MESSAGE, MILP_XOR_DIFFERENTIAL_OBJECTIVE
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@

from bitstring import BitArray

from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.utils.generate_inequalities_for_xor_with_n_input_bits import \
update_dictionary_that_contains_xor_inequalities_between_n_input_bits, \
output_dictionary_that_contains_xor_inequalities
Expand Down
120 changes: 120 additions & 0 deletions claasp/cipher_modules/models/milp/solvers.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
import os

# ****************************************************************************
# Copyright 2023 Technology Innovation Institute
#
# This program is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <https://www.gnu.org/licenses/>.
# ****************************************************************************


SOLVER_DEFAULT = "GLPK"
MODEL_DEFAULT_PATH = os.getcwd()



MILP_SOLVERS_INTERNAL = [
{"solver_brand_name": "GLPK (GNU Linear Programming Kit) (using Sage backend)", "solver_name": "GLPK"},
{"solver_brand_name": "GLPK (GNU Linear Programming Kit) with simplex method based on exact arithmetic (using Sage backend)", "solver_name": "GLPK/exact"},
{"solver_brand_name": "COIN-BC (COIN Branch and Cut) (using Sage backend)", "solver_name": "Coin"},
{"solver_brand_name": "CVXOPT (Python Software for Convex Optimization) (using Sage backend)", "solver_name": "CVXOPT"},
{"solver_brand_name": "Gurobi Optimizer (using Sage backend)", "solver_name": "Gurobi"},
{"solver_brand_name": "PPL (Parma Polyhedra Library) (using Sage backend)", "solver_name": "PPL"},
{"solver_brand_name": "InteractiveLP (using Sage backend)", "solver_name": "InteractiveLP"},
]

MILP_SOLVERS_EXTERNAL = [
{
"solver_brand_name": "Gurobi Optimizer (external)",
"solver_name": "GUROBI_EXT",
"keywords": {
"command": {
"executable": "gurobi_cl",
"options": [],
"input_file": "",
"solve": "",
"output_file": "ResultFile=",
"end": "",
"format": ["executable", "output_file", "input_file"],
},
"time": r"Explored \d+ nodes \(\d+ simplex iterations\) in ([0-9]*[.]?[0-9]+) seconds",
"unsat_condition": "Model is infeasible",
},
},
{
"solver_brand_name": "GLPK (GNU Linear Programming Kit) (external)",
"solver_name": "GLPK_EXT",
"keywords": {
"command": {
"executable": "glpsol",
"options": ["--lp"],
"input_file": "",
"solve": "",
"output_file": "--output ",
"end": "",
"format": ["executable", "options", "input_file", "output_file"],
},
"time": r"Time used:[\s]+([0-9]*[.]?[0-9]+) secs",
"memory": r"Memory used:[\s]+([0-9]*[.]?[0-9]+) Mb",
"unsat_condition": r"PROBLEM HAS NO (\w+) FEASIBLE SOLUTION",
},
},
{
"solver_brand_name": "SCIP (Solving Constraint Integer Programs) (external)",
"solver_name": "SCIP_EXT",
"keywords": {
"command": {
"executable": "scip",
"options": ["-c", '"'],
"input_file": "read",
"solve": "optimize",
"output_file": "write solution",
"end": '"quit',
"format": [
"executable",
"options",
"input_file",
"solve",
"output_file",
"end",
],
},
"time": r"Solving Time \(sec\)[\s]+:[\s]+([0-9]*[.]?[0-9]+)",
"unsat_condition": r"problem is solved \[infeasible\]",
},
},
{
"solver_brand_name": "IBM ILOG CPLEX Optimizer (external)",
"solver_name": "CPLEX_EXT",
"keywords": {
"command": {
"executable": "cplex",
"options": ["-c"],
"input_file": "read",
"solve": "optimize",
"output_file": "set logfile",
"end": "display solution variables -",
"format": [
"executable",
"options",
"input_file",
"solve",
"output_file",
"end",
],
},
"time": r"Solution time =[\s]+([0-9]*[.]?[0-9]+) sec.",
"unsat_condition": "MIP - Integer infeasible.",
},
},
]
59 changes: 0 additions & 59 deletions claasp/cipher_modules/models/milp/utils/config.py

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@


"""The target of this module is to generate MILP inequalities for a AND operation between 2 input bits."""
from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT


def and_inequalities():
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@
from claasp.cipher_modules.models.milp import MILP_AUXILIARY_FILE_PATH
from sage.rings.integer_ring import ZZ

from claasp.cipher_modules.models.milp.utils.config import SOLVER_DEFAULT
from claasp.cipher_modules.models.milp.solvers import SOLVER_DEFAULT

small_sbox_file_name = "dictionary_that_contains_inequalities_for_small_sboxes.obj"
small_sbox_xor_linear_file_name = "dictionary_that_contains_inequalities_for_small_sboxes_xor_linear.obj"
Expand Down
Loading

0 comments on commit cb28bed

Please sign in to comment.