Feature/ADD: add options and weight parameter for sat linear model

Crypto-TII · Nov 7, 2024 · a687bb7 · a687bb7
1 parent ed41e5d
commit a687bb7
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git 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
@@ -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']))