From a687bb70d7277c106ddd39d480aeb5a4ee1cf932 Mon Sep 17 00:00:00 2001 From: cs Date: Fri, 8 Nov 2024 03:21:48 +0400 Subject: [PATCH] Feature/ADD: add options and weight parameter for sat linear model --- claasp/cipher_modules/models/sat/sat_model.py | 1 - .../models/sat/sat_models/sat_xor_linear_model.py | 6 +++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/claasp/cipher_modules/models/sat/sat_model.py b/claasp/cipher_modules/models/sat/sat_model.py index 40527ae0..0f8fef4e 100644 --- a/claasp/cipher_modules/models/sat/sat_model.py +++ b/claasp/cipher_modules/models/sat/sat_model.py @@ -295,7 +295,6 @@ def _solve_with_external_sat_solver(self, model_type, solver_name, options, host input_file, output_file) elif solver_specs['solver_name'] == 'PARKISSAT_EXT': input_file = f'{self.cipher_id}_{file_id}_sat_input.cnf' - options = ["-c=80"] status, sat_time, sat_memory, values = utils.run_parkissat(solver_specs, options, dimacs, input_file) elif solver_specs['solver_name'] == 'YICES_SAT_EXT': input_file = f'{self.cipher_id}_{file_id}_sat_input.cnf' diff --git a/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py b/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py index 7268637a..e19b75a4 100644 --- a/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py +++ b/claasp/cipher_modules/models/sat/sat_models/sat_xor_linear_model.py @@ -236,7 +236,7 @@ def find_all_xor_linear_trails_with_weight_at_most(self, min_weight, max_weight, return solutions_list - def find_lowest_weight_xor_linear_trail(self, fixed_values=[], solver_name=solvers.SOLVER_DEFAULT): + def find_lowest_weight_xor_linear_trail(self, fixed_values=[], solver_name=solvers.SOLVER_DEFAULT, options=None, start_weight=0): """ Return the solution representing a XOR LINEAR trail with the lowest possible weight. By default, the search removes the key schedule, if any. @@ -277,7 +277,7 @@ def find_lowest_weight_xor_linear_trail(self, fixed_values=[], solver_name=solve sage: trail['total_weight'] 3.0 """ - current_weight = 0 + current_weight = start_weight start_building_time = time.time() self.build_xor_linear_trail_model(weight=current_weight, fixed_variables=fixed_values) end_building_time = time.time() @@ -290,7 +290,7 @@ def find_lowest_weight_xor_linear_trail(self, fixed_values=[], solver_name=solve start_building_time = time.time() self.build_xor_linear_trail_model(weight=current_weight, fixed_variables=fixed_values) end_building_time = time.time() - solution = self.solve(XOR_LINEAR, solver_name=solver_name) + solution = self.solve(XOR_LINEAR, solver_name=solver_name, options=options) solution['building_time_seconds'] = end_building_time - start_building_time total_time += solution['solving_time_seconds'] max_memory = max((max_memory, solution['memory_megabytes']))