refactored lib_satprob module, updated solving algorithm

core/impl/solving.py

@@ -1,14 +1,20 @@
+from warnings import warn
 from typing import Dict, Any
 from time import time as now
 
 from ..abc import Core
-
 from space.model import Backdoor
+
 from lib_satprob.solver import Report
 from lib_satprob.derived import get_derived_by
+from lib_satprob.encoding import is_sat_formula
 from lib_satprob.variables import Supplements
 
 
+def warn_bad(backdoor: Backdoor):
+    warn(f'Bad backdoor: {backdoor} (all tasks is hard!)')
+
+
 class Solving(Core):
     slug = 'core:solving'
 
@@ -22,26 +28,33 @@ def add_supplements(_supplements: Supplements):
             for _clause in map(tuple, _constraints):
                 constraints_set.add(_clause)
 
-        def get_report(_status, _stats, _model) -> Report:
-            _time = _stats.get('time', 0.) + now() - stamp
-            return Report(_status, {'time': _time}, _model)
+        def get_report(_status, _stats, _model, _cost) -> Report:
+            _stats = {**_stats, 'time': now() - stamp}
+            return Report(_status, _stats, _model, _cost)
 
-        with self.problem.solver.get_instance(formula) as solver:
+        print(f'Processing {len(backdoors)} passed backdoors...')
+        with self.problem.solver.get_instance(formula, False) as solver:
             for backdoor, easy, hard in [(bd, [], []) for bd in backdoors]:
                 for supplements in backdoor.enumerate():
-                    status, stats, model, _ = solver.propagate(supplements)
+                    status, stats, model, cost = solver.propagate(supplements)
                     (easy if status is False else hard).append(supplements)
-                    if status is True: return get_report(status, {}, model)
 
-                if len(hard) == 0: return get_report(False, {}, None)
-                add_supplements(
+                    if status is True and is_sat_formula(formula):
+                        return get_report(status, stats, model, cost)
+
+                if len(hard) == 0: return get_report(False, {}, None, None)
+                warn_bad(backdoor) if len(easy) == 0 else add_supplements(
                     hard[0] if len(hard) == 1 else get_derived_by(easy)
                 )
 
-            assumptions = list(assumptions_set)
-            constraints = [list(c) for c in constraints_set]
-            report = solver.solve((assumptions, constraints))
-            return get_report(report.status, report.stats, report.model)
+            a_len, c_len = len(assumptions_set), len(constraints_set)
+            print(f'Derived {a_len} literals and {c_len} clauses')
+
+            status, stats, model, cost = solver.solve(([], [
+                *([lit] for lit in assumptions_set),
+                *(list(cl) for cl in constraints_set)
+            ]))
+            return get_report(status, stats, model, cost)
 
     def __config__(self) -> Dict[str, Any]:
         return {}

lib_satprob/encoding/impl/__init__.py

@@ -15,6 +15,11 @@
     # types
     'Clause',
     'Clauses',
+    'SatFormula',
+    'PySatFormula',
+    'MaxSatFormula',
     # utility
-    'wcnf_to_cnf'
+    'to_sat_formula',
+    'is_sat_formula',
+    'is_max_sat_formula'
 ]

lib_satprob/encoding/impl/pysat.py

@@ -5,14 +5,29 @@
 from .._readers import PySatReader, CNFReader, \
     CNFPlusReader, WCNFReader, WCNFPlusReader
 
+#
+# ==============================================================================
 Clause = List[int]
 Clauses = List[Clause]
 
+SatFormula = Union[
+    Clauses,
+    fml.CNF, fml.CNFPlus
+]
+MaxSatFormula = Union[
+    fml.WCNF, fml.WCNFPlus
+]
+PySatFormula = Union[
+    SatFormula, MaxSatFormula
+]
+
 
+#
+# ==============================================================================
 def wcnf_to_cnf(
-        wcnf: fml.WCNF,
+        wcnf: MaxSatFormula,
         only_hard: bool = True
-) -> Union[fml.CNF, fml.CNFPlus]:
+) -> SatFormula:
     if isinstance(wcnf, fml.WCNFPlus):
         cnf = fml.CNFPlus()
         cnf.atmosts = wcnf.atms
@@ -28,6 +43,30 @@ def wcnf_to_cnf(
     return cnf
 
 
+#
+# ==============================================================================
+def is_sat_formula(formula: PySatFormula) -> bool:
+    return isinstance(formula, list) or \
+           isinstance(formula, fml.CNF) or \
+           isinstance(formula, fml.CNFPlus)
+
+
+def is_max_sat_formula(formula: PySatFormula) -> bool:
+    return isinstance(formula, fml.WCNF) or \
+           isinstance(formula, fml.WCNFPlus)
+
+
+def to_sat_formula(formula: PySatFormula) -> SatFormula:
+    if is_max_sat_formula(formula):
+        formula = wcnf_to_cnf(formula)
+
+    return formula
+
+
+#
+# ==============================================================================
+
+
 class PySatEnc(Encoding):
     slug = 'encoding:pysat'
 
@@ -206,6 +245,11 @@ def __copy__(self) -> 'WCNFPlus':
     # types
     'Clause',
     'Clauses',
+    'SatFormula',
+    'PySatFormula',
+    'MaxSatFormula',
     # utility
-    'wcnf_to_cnf'
+    'to_sat_formula',
+    'is_sat_formula',
+    'is_max_sat_formula'
 ]

lib_satprob/solver/impl/py2sat.py

@@ -4,8 +4,10 @@
 from ...variables import Supplements
 from ...variables.vars import VarMap
 
-from ..solver import Report, KeyLimit, UNLIMITED
-from .pysat import _PySatSolver, PySatSolver, PySatFormula, PySatSetts
+from .pysat import PySatSetts, \
+    _PySatSolver, PySatSolver
+from ..solver import Report
+from ...encoding import SatFormula
 
 
 def is2clause(clause: Clause, var_map: VarMap) -> bool:
@@ -24,23 +26,21 @@ def is2clause(clause: Clause, var_map: VarMap) -> bool:
 class _Py2SatSolver(_PySatSolver):
     def __init__(
             self,
-            formula: PySatFormula,
+            formula: SatFormula,
             settings: PySatSetts,
             use_timer: bool = True,
             threshold: float = 1.0,
     ):
         super().__init__(formula, settings, use_timer)
         self.limit = (1 - threshold) * len(formula.clauses)
 
-    def solve(
+    def propagate(
             self, supplements: Supplements,
-            limit: KeyLimit = UNLIMITED,
-            extract_model: bool = True
+            ignore_constraints: bool = False
     ) -> Report:
-        raise RuntimeError(f'Unsupported method \'solve\'')
-
-    def propagate(self, supplements: Supplements) -> Report:
-        report = super().propagate(supplements)
+        report = super().propagate(
+            supplements, ignore_constraints
+        )
         if report.status is not None: return report
 
         _, stats, literals, cost = report
@@ -66,7 +66,7 @@ def __init__(self, threshold: float = 1.0, sat_name: str = 'm22'):
         self.threshold = threshold
 
     def get_instance(
-            self, formula: PySatFormula, use_timer: bool = True
+            self, formula: SatFormula, use_timer: bool = True
     ) -> _Py2SatSolver:
         return _Py2SatSolver(formula, self.settings, use_timer)
 

lib_satprob/solver/impl/pysat.py

@@ -4,43 +4,13 @@
 from typing import Dict, Union, \
     Any, Tuple, Optional, NamedTuple
 
+from pysat import solvers as slv
 from pysat.examples.rc2 import RC2
-from pysat import solvers as slv, formula as fml
 
-from ...encoding import Clauses, wcnf_to_cnf
-from ...variables import Assumptions, Supplements
 from ..solver import Solver, _Solver, Report, KeyLimit, UNLIMITED
-
-#
-# ==============================================================================
-SatFormula = Union[
-    Clauses,
-    fml.CNF, fml.CNFPlus
-]
-MaxSatFormula = Union[
-    fml.WCNF, fml.WCNFPlus
-]
-PySatFormula = Union[
-    SatFormula, MaxSatFormula
-]
-
-
-def is_sat_formula(formula: PySatFormula) -> bool:
-    return isinstance(formula, list) or \
-           isinstance(formula, fml.CNF) or \
-           isinstance(formula, fml.CNFPlus)
-
-
-def is_max_sat_formula(formula: PySatFormula) -> bool:
-    return isinstance(formula, fml.WCNF) or \
-           isinstance(formula, fml.WCNFPlus)
-
-
-def to_sat_formula(formula: PySatFormula) -> SatFormula:
-    if is_max_sat_formula(formula):
-        formula = wcnf_to_cnf(formula)
-
-    return formula
+from ...encoding import SatFormula, PySatFormula, MaxSatFormula, \
+    to_sat_formula, is_sat_formula, is_max_sat_formula
+from ...variables import Assumptions, Supplements
 
 
 #
@@ -50,10 +20,10 @@ class PySatSetts(NamedTuple):
     max_sat_alg: str
 
 
-def is_supports_atms(sat_name: str) -> bool:
-    return sat_name in slv.SolverNames.gluecard3 or \
-           sat_name in slv.SolverNames.gluecard4 or \
-           sat_name in slv.SolverNames.minicard
+# def is_supports_atms(sat_name: str) -> bool:
+#     return sat_name in slv.SolverNames.gluecard3 or \
+#            sat_name in slv.SolverNames.gluecard4 or \
+#            sat_name in slv.SolverNames.minicard
 
 
 #
@@ -243,14 +213,19 @@ def _init_solver(
             self, supplements: Supplements,
             formula: Optional[PySatFormula] = None
     ) -> Tuple[Optional[AnySolver], Assumptions]:
+        name = self.settings.sat_name
         formula = formula or self.formula
         assumptions, constraints = supplements
 
         if is_sat_formula(formula):
-            name = self.settings.sat_name
-            solver = slv.Solver(name, formula)
-            solver.append_formula(constraints)
-            return solver.solver, assumptions
+            if len(constraints) > 0:
+                solver = slv.Solver(name, formula)
+                solver.append_formula(constraints)
+                return solver.solver, assumptions
+            elif self._solver is None:
+                solver = slv.Solver(name, formula)
+                self._solver = solver.solver
+            return None, assumptions
         elif is_max_sat_formula(formula):
             return get_max_sat_alg(
                 self.settings, formula
@@ -277,22 +252,14 @@ def solve(
         assumptions, constraints = supplements
         args = (limit, extract_model, self.use_timer)
 
-        if len(constraints) > 0:
-            solver, assumptions = self._init_solver(
-                (assumptions, constraints), self.formula
-            )
-            with solver:
-                return _solve(solver, assumptions, *args)
-
-        if self._solver is None:
-            solver, assumptions = self._init_solver(
-                (assumptions, constraints), self.formula
-            )
-            self._solver = solver
-
-        return self._fix_stats(
+        solver, assumptions = self._init_solver(
+            (assumptions, constraints), self.formula
+        )
+        if not solver: return self._fix_stats(
             _solve(self._solver, assumptions, *args)
         )
+        with solver:
+            return _solve(solver, assumptions, *args)
 
     def propagate(
             self, supplements: Supplements,
@@ -301,24 +268,15 @@ def propagate(
         assumptions, constraints = supplements
         if ignore_constraints: constraints = []
 
-        if len(constraints) > 0:
-            formula = to_sat_formula(self.formula)
-            solver, assumptions = self._init_solver(
-                (assumptions, constraints), formula
-            )
-            with solver:
-                return _propagate(solver, assumptions)
-
-        if self._propagator is None:
-            formula = to_sat_formula(self.formula)
-            solver, assumptions = self._init_solver(
-                (assumptions, constraints), formula
-            )
-            self._propagator = solver
-
-        return self._fix_stats(
-            _propagate(self._propagator, assumptions)
+        formula = to_sat_formula(self.formula)
+        solver, assumptions = self._init_solver(
+            (assumptions, constraints), formula
+        )
+        if not solver: return self._fix_stats(
+            _propagate(self._solver, assumptions)
         )
+        with solver:
+            return _propagate(solver, assumptions)
 
 
 #
@@ -348,5 +306,4 @@ def __config__(self) -> Dict[str, Any]:
     # types
     'PySatTimer',
     'PySatSetts',
-    'PySatFormula'
 ]