updated encoding interface, added maxSAT solver

.gitignore

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

examples/sgen_example_mpi.py

@@ -1,5 +1,5 @@
 from core.impl import Optimize
-from core.module.space import InputSet
+from core.module.space import SearchSet
 from core.module.sampling import Const
 from core.module.limitation import WallTime
 from core.module.comparator import MinValueMaxSize
@@ -9,6 +9,7 @@
 
 from instance.impl import Instance
 from instance.module.encoding import CNF
+from instance.module.variables import Interval
 
 from function.impl import GuessAndDetermine
 from function.module.measure import SolvingTime
@@ -26,7 +27,10 @@
     logs_path = WorkPath('examples', 'logs')
 
     solution = Optimize(
-        space=InputSet(),
+        space=SearchSet(
+            by_mask=[],
+            variables=Interval(start=1, length=150)
+        ),
         executor=MPIExecutor(),
         sampling=Const(size=4096, split_into=256),
         instance=Instance(

function/impl/function_gad.py

@@ -50,11 +50,11 @@ def gad_supplements(args: WorkerArgs, instance: Instance,
         substitutions = sample_state.randint(0, dimension, shape)[offset:]
 
     if instance.input_dependent:
-        encoding_data = instance.encoding.get_data()
+        formula = instance.encoding.get_formula()
         instance_vars = instance.get_instance_vars()
         # todo: use solver.DEFAULT instead of Glucose3
         # todo: improve function package typing
-        with Glucose3(encoding_data.clauses()) as solver:
+        with Glucose3(formula) as solver:
             for substitution in substitutions:
                 assumptions, _ = instance_vars.get_propagation(sample_state)
                 yield combine(
@@ -72,9 +72,9 @@ def gad_worker_fn(args: WorkerArgs, payload: Payload) -> WorkerResult:
 
     # limit = measure.get_limit(budget)
     times, times2, values, values2 = {}, {}, {}, {}
-    encoding_data, statuses = instance.encoding.get_data(), {}
+    formula, statuses = instance.encoding.get_formula(), {}
     for supplements in gad_supplements(args, instance, backdoor):
-        report = solver.solve(encoding_data, supplements)
+        report = solver.solve(formula, supplements)
         time, value, status = measure.check_and_get(report, budget)
 
         times[status.value] = times.get(status.value, 0.) + time

function/impl/function_ibs.py

@@ -24,11 +24,11 @@ def ibs_supplements(args: WorkerArgs, instance: Instance,
 
     sample_seed, _, offset, length = args
     sample_state = RandomState(sample_seed)
-    encoding_data = instance.encoding.get_data()
+    formula = instance.encoding.get_formula()
     instance_vars = instance.get_instance_vars(searchable)
     # todo: use solver.DEFAULT instead of Glucose3
     # todo: improve function package typing
-    with Glucose3(encoding_data.clauses()) as solver:
+    with Glucose3(formula) as solver:
         for index in range(offset + length):
             assumptions, _ = instance_vars.get_propagation(sample_state)
             if index >= offset:
@@ -41,9 +41,9 @@ def ibs_worker_fn(args: WorkerArgs, payload: Payload) -> WorkerResult:
 
     limit = measure.get_limit(budget)
     times, times2, values, values2 = {}, {}, {}, {}
-    encoding_data, statuses = instance.encoding.get_data(), {}
+    formula, statuses = instance.encoding.get_formula(), {}
     for supplements in ibs_supplements(args, instance, backdoor):
-        report = solver.solve(encoding_data, supplements, limit)
+        report = solver.solve(formula, supplements, limit)
         time, value, status = measure.check_and_get(report, budget)
 
         times[status.value] = times.get(status.value, 0.) + time

function/impl/function_ips.py

@@ -17,8 +17,8 @@ def ips_worker_fn(args: WorkerArgs, payload: Payload) -> WorkerResult:
     searchable, timestamp = space.unpack(instance, bytemask), now()
 
     times, times2, values, values2 = {}, {}, {}, {}
-    encoding_data, statuses = instance.encoding.get_data(), {}
-    with solver.use_incremental(encoding_data) as incremental:
+    formula, statuses = instance.encoding.get_formula(), {}
+    with solver.use_incremental(formula) as incremental:
         for assumptions, _ in ibs_supplements(args, instance, searchable):
             # todo: use constraints with incremental propagation?
             report = incremental.propagate(assumptions)

function/impl/function_rho.py

@@ -18,8 +18,8 @@ def rho_worker_fn(args: WorkerArgs, payload: Payload) -> WorkerResult:
     searchable, timestamp = space.unpack(instance, bytemask), now()
 
     times, times2, values, values2 = {}, {}, {}, {}
-    encoding_data, statuses = instance.encoding.get_data(), {}
-    with solver.use_incremental(encoding_data) as incremental:
+    formula, statuses = instance.encoding.get_formula(), {}
+    with solver.use_incremental(formula) as incremental:
         for assumptions, _ in gad_supplements(args, instance, searchable):
             # todo: use constraints with incremental propagation?
             report = incremental.propagate(assumptions)

function/module/solver/impl/external.py

@@ -2,15 +2,16 @@
 import re
 
 from time import time as now
+from pysat import formula as fml
 from tempfile import NamedTemporaryFile as NTFile
 from subprocess import Popen, TimeoutExpired, PIPE
 
 from util.iterable import concat
 
 from ..solver import Report, Solver, IncrSolver
 
+from instance.module.encoding import Formula
 from function.module.budget import KeyLimit, UNLIMITED
-from instance.module.encoding import EncodingData, CNFData, SourceData
 from typings.searchable import Constraints, Supplements
 
 STATUSES = {
@@ -19,6 +20,13 @@
 }
 
 
+def source(formula: fml.CNF) -> bytes:
+    return ''.join([
+        f'p cnf {formula.nv} {len(formula.clauses)}\n',
+        *(' '.join(map(str, c)) + ' 0\n' for c in formula.clauses)
+    ]).encode()
+
+
 class External(Solver):
     limits = {}
     statistic = {}
@@ -31,23 +39,24 @@ class External(Solver):
     def __init__(self, from_executable: str):
         self.from_executable = from_executable
 
-    def use_incremental(self, encoding_data: EncodingData,
+    def use_incremental(self, formula: Formula,
                         constraints: Constraints = ()) -> IncrSolver:
         raise RuntimeError('External solvers supports only solve procedure')
 
-    def solve(self, encoding_data: EncodingData, supplements: Supplements,
+    def solve(self, formula: Formula, supplements: Supplements,
               limit: KeyLimit = UNLIMITED, add_model: bool = False) -> Report:
         files, launch_args = [], [self.from_executable]
+        assumptions, constraints = supplements
 
-        if isinstance(encoding_data, CNFData) or isinstance(encoding_data, SourceData):
-            source = encoding_data.source(supplements)
+        if isinstance(formula, fml.CNF):
+            formula.extend(constraints + [[lit] for lit in assumptions])
         else:
-            raise TypeError('External solvers works only with Source, CNF or CNF+ encodings')
+            raise TypeError('External solvers works only with CNF or CNF+ encodings')
 
         if self.stdin_file is not None:
             with NTFile(delete=False) as in_file:
+                formula.to_fp(in_file)
                 files.append(in_file.name)
-                in_file.write(source.encode())
                 launch_args.append(self.stdin_file % in_file.name)
 
         if self.stdout_file is not None:
@@ -57,15 +66,15 @@ def solve(self, encoding_data: EncodingData, supplements: Supplements,
 
         timeout, (key, value) = None, limit
         if value is not None and key == 'time':
-            timeout = value + len(source) * 6e-08
+            timeout = value + len(formula.clauses) * 6e-08
         if value is not None and key in self.limits:
             launch_args.append(self.limits[key] % value)
 
         timestamp, process = now(), Popen(
             launch_args, stdin=PIPE, stdout=PIPE, stderr=PIPE
         )
         try:
-            data = None if self.stdin_file else source.encode()
+            data = None if self.stdin_file else source(formula)
             output, error = process.communicate(data, timeout)
             # todo: handle error
 
@@ -94,7 +103,7 @@ def solve(self, encoding_data: EncodingData, supplements: Supplements,
 
         return Report(status, stats, solution)
 
-    def propagate(self, encoding_data: EncodingData, supplements: Supplements) -> Report:
+    def propagate(self, formula: Formula, supplements: Supplements) -> Report:
         raise RuntimeError('External solvers supports only solve procedure')