Merge branch 'lib-feature'

* lib-feature: (24 commits)
  added rho subset func, fix README
  fix test script
  fix test script permissions
  updated functionality examples, fix requirements file
  update documentation, rename problem module
  update combine_t algorithm. some fixes
  updated tests, removed problem instance dependency from space module
  updated combine_t algorithm
  partially updated unit tests
  added formulas core precheck to solver using unit propagation, fix gad sampling generation
  connect 'pysatmc' subcomponent to other evoguess modules, update requirements
  SAT logic has been separated (variables, encoding, solver and instance modules) into new 'pysatmc' subcomponent and implemented its functionality
  updated encoding interface, added maxSAT solver
  try to fix header in source encoding
  added source encoding
  added minisatCS wrapper
  separate budget logic to module, update function typings, fix intervals, update tests
  fix tests
  fixed runtime errors and added log_search algorithm
  separated space module to package, added searchable interface, added interval backdoors
  ...

.github/workflows/run-tests.yml

@@ -21,4 +21,4 @@ jobs:
           python -m pip install --upgrade pip
           pip install -r requirements.txt
       - name: Test with unittest
-        run: python -m unittest discover tests
+        run: ./run_tests.sh

.gitignore

@@ -3,5 +3,6 @@ docs/build
 data/experiments
 
 tools/
+examples/data
 examples/logs
 examples/solvers

README.md

@@ -42,21 +42,26 @@ 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')
+
+problem = SatProblem(
+    encoding=CNF(from_file=cnf_file),
+    solver=PySatSolver(sat_name='g3'),
+)
 solution = Optimize(
-    space=RhoSubset(
-        by_mask=[],
-        of_size=200,
-        variables=Interval(start=1, length=1213)
-    ),
-    instance=Instance(
-        encoding=CNF(from_file=cnf_file)
+    problem=problem,
+    space=BackdoorSet(
+        by_vector=[],
+        variables=rho_subset(
+            problem,
+            Range(start=1, length=1213),
+            of_size=200
+        )
     ),
     executor=ProcessExecutor(max_workers=16),
     sampling=Const(size=8192, split_into=2048),
     function=RhoFunction(
         penalty_power=2 ** 20,
         measure=Propagations(),
-        solver=pysat.Glucose3()
     ),
     algorithm=Elitism(
         elites_count=2,
@@ -80,11 +85,10 @@ 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(
-        encoding=CNF(from_file=cnf_file)
+    problem=SatProblem(
+        encoding=CNF(from_file=cnf_file),
+        solver=PySatSolver(sat_name='g3'),
     ),
-    measure=SolvingTime(),
-    solver=pysat.Glucose3(),
     logger=OptimizeLogger(logs_path),
     executor=ProcessExecutor(max_workers=16)
 ).launch(*backdoors)

README_en.md

@@ -41,21 +41,26 @@ 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')
+
+problem = SatProblem(
+    encoding=CNF(from_file=cnf_file),
+    solver=PySatSolver(sat_name='g3'),
+)
 solution = Optimize(
-    space=RhoSubset(
-        by_mask=[],
-        of_size=200,
-        variables=Interval(start=1, length=1213)
-    ),
-    instance=Instance(
-        encoding=CNF(from_file=cnf_file)
+    problem=problem,
+    space=BackdoorSet(
+        by_vector=[],
+        variables=rho_subset(
+            problem,
+            Range(start=1, length=1213),
+            of_size=200
+        )
     ),
     executor=ProcessExecutor(max_workers=16),
     sampling=Const(size=8192, split_into=2048),
     function=RhoFunction(
         penalty_power=2 ** 20,
         measure=Propagations(),
-        solver=pysat.Glucose3()
     ),
     algorithm=Elitism(
         elites_count=2,
@@ -79,11 +84,10 @@ 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(
-        encoding=CNF(from_file=cnf_file)
+    problem=SatProblem(
+        encoding=CNF(from_file=cnf_file),
+        solver=PySatSolver(sat_name='g3'),
     ),
-    measure=SolvingTime(),
-    solver=pysat.Glucose3(),
     logger=OptimizeLogger(logs_path),
     executor=ProcessExecutor(max_workers=16)
 ).launch(*backdoors)

algorithm/abc/algorithm.py

@@ -1,45 +1,45 @@
 from typing import List, Tuple, TYPE_CHECKING
 
 from typings.optional import Int
+from typings.searchable import Searchable
 
 if TYPE_CHECKING:
-    from core.model.point import Point, Vector
-    from instance.module.variables import Backdoor
+    from core.model.point import Point, PointSet
 
 
 # todo: move to a separate file
 class PointManager:
-    _vector = None
     _buffer = None
+    _point_set = None
 
     def __init__(self, algorithm: 'Algorithm', point: 'Point'):
         self._algorithm = algorithm
         self._point = point
         self._index = 0
 
     def __enter__(self):
-        self._vector = [self._point]
+        self._point_set = [self._point]
         self._buffer = []
         return self
 
-    def solution(self) -> 'Vector':
-        return sorted(self._vector)
+    def solution(self) -> 'PointSet':
+        return sorted(self._point_set)
 
-    def insert(self, *points: 'Point') -> Tuple[int, 'Vector']:
+    def insert(self, *points: 'Point') -> Tuple[int, 'PointSet']:
         self._buffer.extend(points)
         if len(self._buffer) >= self._algorithm.min_update_size:
-            self._vector = self._algorithm.update(self._vector, *self._buffer)
+            self._point_set = self._algorithm.update(self._point_set, *self._buffer)
             self._index, self._buffer = self._index + 1, []
-            return self._index, self._vector
+            return self._index, self._point_set
 
-    def collect(self, in_queue: int, available: int) -> List['Backdoor']:
+    def collect(self, in_queue: int, available: int) -> List[Searchable]:
         if self._algorithm.max_queue_size is not None:
             max_queue_size = self._algorithm.max_queue_size
             available = max(0, max_queue_size - in_queue)
-        return self._algorithm.next(self._vector, available)
+        return self._algorithm.next(self._point_set, available)
 
     def __exit__(self, exc_type, exc_val, exc_tb):
-        self._vector = None
+        self._point_set = None
         self._buffer = None
 
 
@@ -53,10 +53,10 @@ def __init__(self, min_update_size: int, max_queue_size: Int):
     def start(self, point: 'Point') -> PointManager:
         return PointManager(self, point)
 
-    def update(self, vector: 'Vector', *points: 'Point') -> 'Vector':
+    def next(self, point_set: 'PointSet', count: int) -> List[Searchable]:
         raise NotImplementedError
 
-    def next(self, vector: 'Vector', count: int) -> List['Backdoor']:
+    def update(self, point_set: 'PointSet', *points: 'Point') -> 'PointSet':
         raise NotImplementedError
 
     def __str__(self):

algorithm/abc/evolution.py

@@ -6,10 +6,10 @@
 from ..module.selection import Selection
 
 from typings.optional import Int
+from typings.searchable import Searchable
 
 if TYPE_CHECKING:
-    from core.model.point import Vector, Point
-    from instance.module.variables import Backdoor
+    from core.model.point import Point, PointSet
 
 
 class Evolution(Algorithm):
@@ -21,19 +21,19 @@ def __init__(self, min_update_size: int, max_queue_size: Int,
         self.selection = selection
         self.mutation = mutation
 
-    def update(self, vector: 'Vector', *points: 'Point') -> 'Vector':
+    def update(self, vector: 'PointSet', *points: 'Point') -> 'PointSet':
         return self.join(vector, list(points))
 
-    def join(self, parents: 'Vector', offspring: 'Vector') -> 'Vector':
+    def join(self, parents: 'PointSet', offspring: 'PointSet') -> 'PointSet':
         raise NotImplementedError
 
-    def tweak(self, selected: List['Backdoor']) -> List['Backdoor']:
+    def tweak(self, selected: List[Searchable]) -> List[Searchable]:
         return list(map(self.mutation.mutate, selected))
 
-    def next(self, vector: 'Vector', count: int) -> List['Backdoor']:
+    def next(self, vector: 'PointSet', count: int) -> List[Searchable]:
         count = self.tweak_size * ceil(count / self.tweak_size)
         selected = self.selection.select(vector, count)
-        return self.tweak([p.backdoor for p in selected])
+        return self.tweak([p.searchable for p in selected])
 
     def __info__(self):
         return {

algorithm/abc/genetic.py

@@ -1,3 +1,4 @@
+from util.iterable import slice_by, concat
 from typing import List, Iterable, Tuple, TYPE_CHECKING
 
 from .evolution import Evolution
@@ -6,11 +7,10 @@
 from ..module.crossover import Crossover
 
 from typings.optional import Int
-from util.iterable import slice_by, concat
+from typings.searchable import Searchable
 
 if TYPE_CHECKING:
-    from core.model.point import Vector
-    from instance.module.variables import Backdoor
+    from core.model.point import PointSet
 
 
 class Genetic(Evolution):
@@ -21,15 +21,15 @@ def __init__(self, min_update_size: int, max_queue_size: Int,
         super().__init__(min_update_size, max_queue_size, mutation, selection)
         self.crossover = crossover
 
-    def join(self, parents: 'Vector', offspring: 'Vector') -> 'Vector':
+    def join(self, parents: 'PointSet', offspring: 'PointSet') -> 'PointSet':
         raise NotImplementedError
 
-    def tweak(self, selected: List['Backdoor']) -> List['Backdoor']:
+    def tweak(self, selected: List[Searchable]) -> List[Searchable]:
         return concat(*map(self._apply, slice_by(selected, 2)))
 
-    def _apply(self, individuals: Tuple['Backdoor']) -> Iterable['Backdoor']:
+    def _apply(self, individuals: Tuple[Searchable]) -> Iterable[Searchable]:
         if len(individuals) == 2:
-            individuals = self.crossover.cross(*individuals)
+            individuals = self.crossover.cross2(*individuals)
         return map(self.mutation.mutate, individuals)
 
     def __info__(self):

algorithm/impl/__init__.py

@@ -1,9 +1,11 @@
 from .elitism import *
 from .m_plus_l import *
 from .m_comma_l import *
+from .log_search import *
 
 algorithms = {
     Elitism.slug: Elitism,
+    LogSearch.slug: LogSearch,
     MuPlusLambda.slug: MuPlusLambda,
     MuCommaLambda.slug: MuCommaLambda
 }
@@ -12,5 +14,7 @@
     'algorithms',
     # impls
     'Elitism',
-    'MuPlusLambda'
+    'LogSearch',
+    'MuPlusLambda',
+    'MuCommaLambda'
 ]

algorithm/impl/elitism.py

@@ -6,7 +6,7 @@
 from ..module.selection import Selection
 
 from typings.optional import Int
-from core.model.point import Vector
+from core.model.point import PointSet
 from util.iterable import pick_by, omit_by
 
 
@@ -20,7 +20,7 @@ def __init__(self, population_size: int, elites_count: int, mutation: Mutation,
         self.elites_count, self.population_size = elites_count, population_size
         super().__init__(min_update_size, max_queue_size, mutation, crossover, selection)
 
-    def join(self, parents: Vector, offspring: Vector) -> Vector:
+    def join(self, parents: PointSet, offspring: PointSet) -> PointSet:
         # todo: fix same points in elites
         elite_indexes = argsort(parents)[:self.elites_count]
         additional_size = max(0, self.population_size - len(offspring))

algorithm/impl/log_search.py

@@ -0,0 +1,36 @@
+from typing import TYPE_CHECKING
+
+from ..abc import Evolution
+from ..module.mutation import Mutation
+from ..module.selection import Selection
+
+from typings.optional import Int
+
+if TYPE_CHECKING:
+    from core.model.point import PointSet
+
+
+class LogSearch(Evolution):
+    slug = 'evolution:log_search'
+
+    def __init__(self, population_size: int, mutation: Mutation, selection: Selection,
+                 min_update_size: int = 1, max_queue_size: Int = None):
+        self.population_size = population_size
+        min_update_size = min(min_update_size, population_size)
+        super().__init__(min_update_size, max_queue_size, mutation, selection)
+
+    def join(self, parents: 'PointSet', offspring: 'PointSet') -> 'PointSet':
+        return sorted([*parents, *offspring])[:self.population_size]
+
+    def __info__(self):
+        return {
+            **super().__info__(),
+            'mutation': self.mutation,
+            'selection': self.selection,
+            'population_size': self.population_size,
+        }
+
+
+__all__ = [
+    'LogSearch'
+]

algorithm/impl/m_comma_l.py

@@ -3,7 +3,7 @@
 from ..module.selection import Selection
 
 from typings.optional import Int
-from core.model.point import Vector
+from core.model.point import PointSet
 
 
 class MuCommaLambda(Evolution):
@@ -14,7 +14,7 @@ def __init__(self, mu_size: int, lambda_size: int, mutation: Mutation,
         self.mu_size, self.lambda_size = mu_size, lambda_size
         super().__init__(lambda_size, max_queue_size, mutation, selection)
 
-    def join(self, parents: Vector, offspring: Vector) -> Vector:
+    def join(self, parents: PointSet, offspring: PointSet) -> PointSet:
         return sorted(offspring)[:self.mu_size]
 
     def __info__(self):

algorithm/impl/m_plus_l.py

@@ -5,7 +5,7 @@
 from ..module.selection import Selection
 
 from typings.optional import Int
-from core.model.point import Vector
+from core.model.point import PointSet
 from util.iterable import pick_by, omit_by
 
 
@@ -18,7 +18,7 @@ def __init__(self, mu_size: int, lambda_size: int, mutation: Mutation,
         self.mu_size, self.lambda_size = mu_size, lambda_size
         super().__init__(min_update_size, max_queue_size, mutation, selection)
 
-    def join(self, parents: Vector, offspring: Vector) -> Vector:
+    def join(self, parents: PointSet, offspring: PointSet) -> PointSet:
         mu_indexes = argsort(parents)[:self.mu_size]
         additional_size = max(0, self.lambda_size - len(offspring))
         additional_lmbda = omit_by(parents, mu_indexes)[:additional_size]

algorithm/module/crossover/crossover.py

@@ -2,7 +2,7 @@
 from numpy.random import randint, RandomState
 
 from typings.optional import Int
-from instance.module.variables import Backdoor
+from typings.searchable import Searchable
 
 
 class Crossover:
@@ -12,7 +12,10 @@ def __init__(self, random_seed: Int = None):
         self.random_seed = random_seed or randint(2 ** 32 - 1)
         self.random_state = RandomState(seed=self.random_seed)
 
-    def cross(self, ind1: Backdoor, ind2: Backdoor) -> Tuple[Backdoor, Backdoor]:
+    def cross(self, ind1: Searchable, ind2: Searchable) -> Searchable:
+        return self.cross2(ind1, ind2)[self.random_state.randint(2)]
+
+    def cross2(self, ind1: Searchable, ind2: Searchable) -> Tuple[Searchable, Searchable]:
         raise NotImplementedError
 
     def __info__(self):