Skip to content

Commit

Permalink
added rho subset func, fix README
Browse files Browse the repository at this point in the history
  • Loading branch information
alpavlenko committed Nov 29, 2023

Verified

This commit was signed with the committer’s verified signature.
renovate-bot Mend Renovate
1 parent 87bc423 commit a021c5f
Showing 7 changed files with 78 additions and 38 deletions.
28 changes: 16 additions & 12 deletions README.md
Original file line number Diff line number Diff line change
@@ -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)
28 changes: 16 additions & 12 deletions README_en.md
Original file line number Diff line number Diff line change
@@ -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)
24 changes: 15 additions & 9 deletions examples/pvs_search_example.py
Original file line number Diff line number Diff line change
@@ -15,7 +15,8 @@
from lib_satprob.problem import SatProblem

# space module imports
from space.impl import RhoSubset
from space import rho_subset
from space.impl import BackdoorSet

# executor module imports
from executor.impl import ProcessExecutor
@@ -35,15 +36,20 @@
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=Range(start=1, length=1213)
),
problem=SatProblem(
encoding=CNF(from_file=cnf_file),
solver=PySatSolver(sat_name='g3'),
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),
12 changes: 8 additions & 4 deletions examples/rho_func_example_2.py
Original file line number Diff line number Diff line change
@@ -15,7 +15,8 @@
from lib_satprob.problem import SatProblem

# space module imports
from space.impl import RhoSubset
from space import rho_subset
from space.impl import BackdoorSet

# executor module imports
from executor.impl import ProcessExecutor
@@ -54,10 +55,13 @@
solver=PySatSolver(sat_name='g3'),
) # read from file './examples/data/sort/pvs_4_7.cnf

space = RhoSubset(
of_size=100,
space = BackdoorSet(
by_vector=[],
variables=Range(start=1, length=1213)
variables=rho_subset(
problem,
Range(start=1, length=1213),
of_size=100
)
) # reduce to subset of 100 “off” var

executor = ProcessExecutor(max_workers=16)
2 changes: 1 addition & 1 deletion lib_satprob/solver/impl/pysat.py
Original file line number Diff line number Diff line change
@@ -240,7 +240,7 @@ def _fix_stats(self, report):
value - self._last_stats.get(key, 0)
for key, value in report.stats.items()
}
status, self.last_stats, model, weight = report
status, self._last_stats, model, weight = report
return Report(status, fixed_stats, model, weight)

def solve(
4 changes: 4 additions & 0 deletions space/__init__.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
from .abc import Space
from .impl import spaces

from ._utility import *


def SpaceBuilder(configuration, **kwargs):
slug = configuration.pop('slug')
@@ -9,6 +11,8 @@ def SpaceBuilder(configuration, **kwargs):

__all__ = [
'Space',
# utility
'rho_subset',
# builder
'SpaceBuilder'
]
18 changes: 18 additions & 0 deletions space/_utility.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
from numpy import argsort
from util.iterable import pick_by

from lib_satprob.problem import Problem
from lib_satprob.variables import Variables


def rho_subset(
problem: Problem, variables: Variables, of_size: int
) -> Variables:
formula = problem.encoding.get_formula()
with problem.solver.get_instance(formula, use_timer=False) as solver:
_indexes = argsort([sum((
solver.propagate(var.substitute({var: 0})).stats['propagations'],
solver.propagate(var.substitute({var: 1})).stats['propagations'],
)) for var in variables])[::-1][:of_size]

return Variables(from_vars=pick_by(variables.variables(), _indexes))

0 comments on commit a021c5f

Please sign in to comment.