updated functionality examples, fix requirements file

core/impl/combine.py

@@ -1,94 +1,106 @@
 from math import ceil
 from time import time as now
-from typing import Any, List, Dict, Optional
-from itertools import chain, product
+from itertools import product
+from typing import Any, List, Dict, Optional, Tuple
 
 from output import Logger
 from executor import Executor
 
 from ..abc import Core
 
-from function.module.measure import Measure
-from function.model import Status, Estimation
+from function.model import Estimation
 
+from lib_satprob.solver import Report
 from lib_satprob.problem import Problem
-from lib_satprob.variables import Assumptions
-from lib_satprob.solver import Solver, _Solver, Report
+from lib_satprob.variables import Supplements, combine
 
 from typings.searchable import Searchable
-from util.iterable import concat, slice_by
+from util.iterable import concat, slice_by, slice_into
 
 
-def get_propagation(solver: _Solver, searchable: Searchable) -> Report:
-    time_sum, value_sum, up_tasks, hard_tasks = 0, 0, [], []
-    for supplements in searchable.enumerate():
-        status, stats, _ = solver.propagate(supplements)
-        (up_tasks if status else hard_tasks).append(supplements)
-        time_sum, value_sum = time_sum + time, value_sum + value
+def prep_worker(problem: Problem, searchable: Searchable) -> List[Supplements]:
+    clauses = problem.encoding.get_formula(copy=False)
+    with problem.solver.get_instance(clauses) as solver:
+        hard_filter = lambda st: st is None or st
+        return [sups for sups in searchable.enumerate()
+                if hard_filter(solver.propagate(sups).status)]
 
-    status = len(hard_tasks) == 0
-    return Report(status, stats, (up_tasks, hard_tasks))
 
+def prod_worker(
+        problem: Problem, acc_tasks: List[Supplements], tasks: List[Supplements]
+) -> Tuple[List[Supplements], float]:
+    _stamp, formula = now(), problem.encoding.get_formula(copy=False)
+    w_acc_hard_task, prod = [], product(acc_tasks, tasks)
 
-def hard_worker(solver: Solver, problem: Problem, up_tasks: List[Assumptions],
-                hard_tasks: List[Assumptions]) -> Report:
-    time_sum, value_sum, formula = 0, 0, problem.encoding.get_formula()
-    with solver.get_instance(formula) as incremental:
-        for up_task_assumptions in chain(up_tasks, hard_tasks):
-            time, value, _, _ = incremental.solve(
-                (up_task_assumptions, []), extract_model=False
+    with problem.solver.get_instance(formula) as solver:
+        for acc_hard_task in [combine(*prs) for prs in prod]:
+            report = solver.propagate(acc_hard_task)
+            if report.status is None or report.status:
+                w_acc_hard_task.append(acc_hard_task)
+
+    return w_acc_hard_task, now() - _stamp
+
+
+def hard_worker(problem: Problem, hard_tasks: List[Supplements]) -> Report:
+    stats_sum, formula = {}, problem.encoding.get_formula()
+    with problem.solver.get_instance(formula) as incremental:
+        for i, supplements in enumerate(hard_tasks):
+            status, stats, _, _ = incremental.solve(
+                supplements, extract_model=False
             )
-            time_sum, value_sum = time_sum + time, value_sum + value
+            for key, value in stats.items():
+                stats_sum[key] = stats_sum.get(key, 0.) + value
 
-    return Report(time_sum, value_sum, Status.RESOLVED, None)
+    return Report(True, stats_sum, None)
 
 
 class Combine(Core):
     slug = 'core:combine'
 
-    def __init__(self, logger: Logger, measure: Measure, problem: Problem,
+    def __init__(self, logger: Logger, problem: Problem,
                  executor: Executor, random_seed: Optional[int] = None):
-        self.measure = measure
         self.executor = executor
         super().__init__(logger, problem, random_seed)
 
+        self.stats_sum = {}
+
     def launch(self, *searchables: Searchable) -> Estimation:
-        formula = self.problem.encoding.get_formula()
         total_var_set, start_stamp = set(concat(*searchables)), now()
-        time_sum, value_sum, all_up_tasks, all_hard_tasks = 0, 0, [], []
-        with self.problem.solver.get_instance(formula) as solver:
-            for searchable in searchables:
-                report = get_propagation(solver, searchable)
-                time, value, status, (up_tasks, hard_tasks) = report
-                time_sum, value_sum = time_sum + time, value_sum + value
-                all_up_tasks.extend(up_tasks), all_hard_tasks.append(hard_tasks)
-            all_hard_tasks = sorted(all_hard_tasks, key=len, reverse=True)
-
-            # todo: accumulate using executor
-            [acc_hard_tasks, *all_hard_tasks] = all_hard_tasks
-            for hard_tasks, count in [(ts, len(ts)) for ts in all_hard_tasks]:
-                hard_tasks_count = count * len(acc_hard_tasks)
-                acc_hard_tasks = [
-                    concat(*parts) for parts in
-                    product(acc_hard_tasks, hard_tasks)
-                    if solver.propagate((concat(*parts), [])).status
-                ]
-                ratio = round(len(acc_hard_tasks) / hard_tasks_count, 2)
-                print(
-                    f'reduced: {hard_tasks_count} -> {len(acc_hard_tasks)} (x{ratio})')
+        self.stats_sum['prod_time'], self.stats_sum['grow_time'] = 0, 0
+
+        results = [future.result() for future in self.executor.submit_all(
+            prep_worker, *((self.problem, sch) for sch in searchables)
+        ).as_complete()]
+
+        all_hard_tasks = sorted(results, key=len)
+        [acc_hard_tasks, *all_hard_tasks] = all_hard_tasks
+
+        for i, hard_tasks in enumerate(all_hard_tasks):
+            next_acc_hard_tasks = []
+            prod_size = len(acc_hard_tasks) * len(hard_tasks)
+            for future in self.executor.submit_all(prod_worker, *((
+                    self.problem, acc_part_hard_tasks, hard_tasks
+            ) for acc_part_hard_tasks in slice_into(
+                acc_hard_tasks, self.executor.max_workers
+            ))).as_complete():
+                prod_tasks, prod_time = future.result()
+                self.stats_sum['prod_time'] += prod_time
+                next_acc_hard_tasks.extend(prod_tasks)
+
+            acc_hard_tasks = next_acc_hard_tasks
+            ratio = round(len(acc_hard_tasks) / prod_size, 2)
+            print(f'reduced: {prod_size} -> {len(acc_hard_tasks)} (x{ratio})')
 
         split_into = ceil(len(acc_hard_tasks) / self.executor.max_workers)
         for future in self.executor.submit_all(hard_worker, *(
-                (self.solver, self.problem, all_up_tasks, hard_tasks)
-                for hard_tasks in slice_by(acc_hard_tasks, split_into)
+                (self.problem, hard_tasks) for hard_tasks
+                in slice_by(acc_hard_tasks, split_into)
         )).as_complete():
-            time, value, _, _ = future.result()
-            time_sum, value_sum = time_sum + time, value_sum + value
+            for key, value in future.result().stats.items():
+                self.stats_sum[key] = self.stats_sum.get(key, 0.) + value
 
         return {
-            'value': time_sum,
-            'time_sum': time_sum,
-            'value_sum': value_sum,
+            'stats': self.stats_sum,
             'real_time': now() - start_stamp,
             'hard_tasks': len(acc_hard_tasks),
             'total_tasks': 2 ** len(total_var_set)

core/impl/combine_t.py

@@ -287,17 +287,6 @@ def launch(self, *searchables: Searchable) -> Estimation:
                 len(acc_hard_tasks), len(acc_hard_tasks)
             )]
 
-            xx_count = len(acc_hard_tasks)
-            xx_plot_data = [xx_count]
-            for i, hard_tasks in enumerate(all_hard_tasks):
-                xx_count = xx_count * len(hard_tasks)
-                xx_plot_data.append(xx_count)
-                print(xx_plot_data[-1])
-                if i == 46:
-                    print()
-                    print(xx_plot_data)
-                    exit(0)
-
             for i, hard_tasks in enumerate(all_hard_tasks):
                 next_acc_hard_tasks = []
                 prod_size = len(acc_hard_tasks) * len(hard_tasks)

examples/bivium_search_example.py

@@ -6,22 +6,22 @@
 
 # function module imports
 from function.impl import InversePolynomialSets
-from function.module.solver import TwoSAT
 from function.module.measure import Propagations
 
-# instance module imports
-from instance.impl import StreamCipher
-from instance.module.encoding import CNF
-from instance.module.variables import Interval
-from typings.work_path import WorkPath
+# satprob lib imports
+from lib_satprob.encoding import CNF
+from lib_satprob.variables import Range
+from lib_satprob.problem import SatProblem
+from lib_satprob.solver import Py2SatSolver
 
 # space submodule imports
-from core.module.space import InputSet
+from space.impl import BackdoorSet
 
 # executor module imports
 from executor.impl import ProcessExecutor
 
 # core submodule imports
+from util.work_path import WorkPath
 from core.module.sampling import Const
 from core.module.limitation import WallTime
 
@@ -36,16 +36,18 @@
     logs_path = root_path.to_path('logs', 'bivium')
     cnf_file = data_path.to_file('bivium-no-200.cnf', 'bivium')
     solution = Optimize(
-        space=InputSet(),
-        instance=StreamCipher(
+        space=BackdoorSet(
+            variables=Range(start=1, length=177)
+        ),
+        problem=SatProblem(
             encoding=CNF(from_file=cnf_file),
-            input_set=Interval(start=1, length=177),
-            output_set=Interval(start=1838, length=200),
+            solver=Py2SatSolver(sat_name='g3'),
+            input_set=Range(start=1, length=177),
+            output_set=Range(start=1838, length=200),
         ),
         executor=ProcessExecutor(max_workers=16),
         sampling=Const(size=8192, split_into=2048),
         function=InversePolynomialSets(
-            solver=TwoSAT(),
             measure=Propagations(),
         ),
         algorithm=Elitism(

examples/comb_example_1.py

@@ -1,18 +1,17 @@
-# function submodule imports
-from function.module.solver import pysat
-from function.module.measure import SolvingTime
-
-# instance module imports
-from instance.impl import Instance
-from instance.module.encoding import CNF
-from instance.module.variables import Indexes, make_backdoor
+# satprob lib imports
+from lib_satprob.encoding import CNF
+from lib_satprob.variables import Indexes
+from lib_satprob.solver import PySatSolver
+from lib_satprob.problem import SatProblem
 
 # other imports
 from core.impl import Combine
+from space.model import Backdoor
 from output.impl import OptimizeLogger
-from typings.work_path import WorkPath
 from executor.impl import ProcessExecutor
 
+from util.work_path import WorkPath
+
 if __name__ == '__main__':
     str_backdoors = [
         '131 132 133 134 135',
@@ -22,23 +21,22 @@
         '6 7 10 136 137 138 139 140',
     ]
     backdoors = [
-        make_backdoor(Indexes(from_string=str_vars))
-        for str_vars in str_backdoors
+        Backdoor(variables=Indexes(
+            from_string=str_vars
+        )) for str_vars in str_backdoors
     ]
 
     root_path = WorkPath('examples')
     data_path = root_path.to_path('data')
     cnf_file = data_path.to_file('sgen_150.cnf')
     logs_path = root_path.to_path('logs', 'sgen_150_comb')
-    combine = Combine(
-        instance=Instance(
+    estimation = Combine(
+        problem=SatProblem(
+            solver=PySatSolver(sat_name='g3'),
             encoding=CNF(from_file=cnf_file)
         ),
-        measure=SolvingTime(),
-        solver=pysat.Glucose3(),
         logger=OptimizeLogger(logs_path),
         executor=ProcessExecutor(max_workers=4)
-    )
+    ).launch(*backdoors)
 
-    estimation = combine.launch(*backdoors)
     print(estimation)

examples/comb_example_2.py

@@ -1,18 +1,17 @@
-# function submodule imports
-from function.module.solver import pysat
-from function.module.measure import SolvingTime
-
-# instance module imports
-from instance.impl import Instance
-from instance.module.encoding import CNF
-from instance.module.variables import Indexes, make_backdoor
+# satprob lib imports
+from lib_satprob.encoding import CNF
+from lib_satprob.problem import SatProblem
+from lib_satprob.solver import PySatSolver
+from lib_satprob.variables import Indexes
 
 # other imports
 from core.impl import Combine
+from space.model import Backdoor
 from output.impl import OptimizeLogger
-from typings.work_path import WorkPath
 from executor.impl import ProcessExecutor
 
+from util.work_path import WorkPath
+
 if __name__ == '__main__':
     str_backdoors = [
         '348 470 682 684 686 687 702 706 708 710 715',
@@ -22,20 +21,20 @@
         '164 176 177 348 470 683 684 689 708 710 715',
     ]
     backdoors = [
-        make_backdoor(Indexes(from_string=str_vars))
-        for str_vars in str_backdoors
+        Backdoor(variables=Indexes(
+            from_string=str_vars
+        )) for str_vars in str_backdoors
     ]
 
     root_path = WorkPath('examples')
     data_path = root_path.to_path('data')
     cnf_file = data_path.to_file('pvs_4_7.cnf', 'sort')
     logs_path = root_path.to_path('logs', 'pvs_4_7_comb')
     estimation = Combine(
-        instance=Instance(
+        problem=SatProblem(
+            solver=PySatSolver(sat_name='g3'),
             encoding=CNF(from_file=cnf_file)
         ),
-        measure=SolvingTime(),
-        solver=pysat.Glucose3(),
         logger=OptimizeLogger(logs_path),
         executor=ProcessExecutor(max_workers=4)
     ).launch(*backdoors)