Minimum/minimal hitting set solver (pysat.examples.hitman
)#
List of classes#
A cardinality-/subset-minimal hitting set enumerator. |
Module description#
A SAT-based implementation of an implicit minimal hitting set [1] enumerator. The implementation is capable of computing/enumerating cardinality- and subset-minimal hitting sets of a given set of sets. Cardinality-minimal hitting set enumeration can be seen as ordered (sorted by size) subset-minimal hitting enumeration.
The minimal hitting set problem is trivially formulated as a MaxSAT formula in WCNF, as follows. Assume \(E=\{e_1,\ldots,e_n\}\) to be a universe of elements. Also assume there are \(k\) sets to hit: \(s_i=\{e_{i,1},\ldots,e_{i,j_i}\}\) s.t. \(e_{i,l}\in E\). Every set \(s_i=\{e_{i,1},\ldots,e_{i,j_i}\}\) is translated into a hard clause \((e_{i,1} \vee \ldots \vee e_{i,j_i})\). This results in the set of hard clauses having size \(k\). The set of soft clauses comprises unit clauses of the form \((\neg{e_{j}})\) s.t. \(e_{j}\in E\), each having weight 1.
Taking into account this problem formulation as MaxSAT, ordered hitting
enumeration is done with the use of the state-of-the-art MaxSAT solver
called RC2
[2] [3] [4] while unordered hitting set enumeration
is done through the minimal correction subset (MCS) enumeration, e.g.
using the LBX
- [5] or MCSls
-like [6] MCS enumerators.
Note that this implementation additionally supports pure SAT-based minimal hitting set enumeration with the use of preferred variable polarity setting following the approach of [7].
Hitman
supports hitting set enumeration in the implicit manner,
i.e. when sets to hit can be added on the fly as well as hitting sets can
be blocked on demand.
An example usage of Hitman
through the Python import
interface
is shown below. Here we target unordered subset-minimal hitting set
enumeration.
>>> from pysat.examples.hitman import Hitman
>>>
>>> h = Hitman(solver='m22', htype='lbx')
>>> # adding sets to hit
>>> h.hit([1, 2, 3])
>>> h.hit([1, 4])
>>> h.hit([5, 6, 7])
>>>
>>> h.get()
[1, 5]
>>>
>>> h.block([1, 5])
>>>
>>> h.get()
[2, 4, 5]
>>>
>>> h.delete()
Enumerating cardinality-minimal hitting sets can be done as follows:
>>> from pysat.examples.hitman import Hitman
>>>
>>> sets = [[1, 2, 3], [1, 4], [5, 6, 7]]
>>> with Hitman(bootstrap_with=sets, htype='sorted') as hitman:
... for hs in hitman.enumerate():
... print(hs)
...
[1, 5]
[1, 6]
[1, 7]
[3, 4, 7]
[2, 4, 7]
[3, 4, 6]
[3, 4, 5]
[2, 4, 6]
[2, 4, 5]
Finally, implicit hitting set enumeration can be used in practical problem solving. As an example, let us show the basic flow of a MaxHS-like [8] algorithm for MaxSAT:
>>> from pysat.examples.hitman import Hitman
>>> from pysat.solvers import Solver
>>>
>>> hitman = Hitman(htype='sorted')
>>> oracle = Solver()
>>>
>>> # here we assume that the SAT oracle
>>> # is initialized with a MaxSAT formula,
>>> # whose soft clauses are extended with
>>> # selector literals stored in "sels"
>>> while True:
... hs = hitman.get() # hitting the set of unsatisfiable cores
... ts = set(sels).difference(set(hs)) # soft clauses to try
...
... if oracle.solve(assumptions=ts):
... print('s OPTIMUM FOUND')
... print('o', len(hs))
... break
... else:
... core = oracle.get_core()
... hitman.hit(core)
Jessica Davies, Fahiem Bacchus. Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. CP 2011. pp. 225-239
Module details#
- class examples.hitman.Atom(obj, sign=True)#
Atoms are elementary (signed) objects necessary when dealing with hitting sets subject to hard constraints.
- class examples.hitman.Hitman(bootstrap_with=[], weights=None, subject_to=[], solver='g3', htype='sorted', mxs_adapt=False, mxs_exhaust=False, mxs_minz=False, mxs_trim=0, mcs_usecld=False)#
A cardinality-/subset-minimal hitting set enumerator. The enumerator can be set up to use either a MaxSAT solver
RC2
or an MCS enumerator (eitherLBX
orMCSls
). In the former case, the hitting sets enumerated are ordered by size (smallest size hitting sets are computed first), i.e. sorted. In the latter case, subset-minimal hitting are enumerated in an arbitrary order, i.e. unsorted. Additionally, Hitman supports pure SAT-based minimal hitting set enumeration with the use of polarity preferences.This is handled with the use of parameter
htype
, which is set to be'sorted'
by default. The MaxSAT-based enumerator can be chosen by settinghtype
to one of the following values:'maxsat'
,'mxsat'
, or'rc2'
. Alternatively, by setting it to'mcs'
or'lbx'
, a user can enforce using theLBX
MCS enumerator. Ifhtype
is set to'mcsls'
, theMCSls
enumerator is used. Finally, value'sat'
can be given, in which case minimal hitting set enumeration will performed by means of a SAT solver (can be either MiniSat-GH, or Lingeling, or CaDiCaL 153) with polarity setting.In either case, unless pure SAT-based hitting set enumeration is selected, an underlying problem solver can use a SAT oracle specified as an input parameter
solver
. The default SAT solver is Glucose3 (specified asg3
, seeSolverNames
for details). For SAT-based enumeration, MinisatGH is used as an underlying SAT solver.Objects of class
Hitman
can be bootstrapped with an iterable of iterables, e.g. a list of lists. This is handled using thebootstrap_with
parameter. Each set to hit can comprise elements of any type, e.g. integers, strings or objects of any Python class, as well as their combinations. The bootstrapping phase is done ininit()
.Another optional parameter
subject_to
can be used to specify arbitrary hard constraints that must be respected when computing hitting sets of the given sets. Note thatsubject_to
should be an iterable containing pure clauses and/or native AtMostK constraints. Note that native cardinality constraints supported only by MiniCard-like solvers. Finally, note that these hard constraints must be defined over the set of signed atomic objects, i.e. instances of classAtom
.A few other optional parameters include the possible options for RC2 as well as for LBX- and MCSls-like MCS enumerators that control the behaviour of the underlying solvers.
- Parameters:
bootstrap_with (iterable(iterable(obj))) – input set of sets to hit
weights (dict(obj)) – a mapping from objects to their weights (if weighted)
subject_to (iterable(iterable(Atom))) – hard constraints (either clauses or native AtMostK constraints)
solver (str) – name of SAT solver
htype (str) – enumerator type
mxs_adapt (bool) – detect and process AtMost1 constraints in RC2
mxs_exhaust (bool) – apply unsatisfiable core exhaustion in RC2
mxs_minz (bool) – apply heuristic core minimization in RC2
mxs_trim (int) – trim unsatisfiable cores at most this number of times
mcs_usecld (bool) – use clause-D heuristic in the MCS enumerator
- add_hard(clause, weights=None)#
Add a hard constraint, which can be either a pure clause or an AtMostK constraint.
Note that an optional parameter that can be passed to this method is
weights
, which contains a mapping the objects under question into weights. Also note that the weight of an object must not change from one call ofhit()
to another.- Parameters:
clause (iterable(obj)) – hard constraint (either a clause or a native AtMostK constraint)
weights (dict(obj)) – a mapping from objects to weights
- block(to_block, weights=None)#
The method serves for imposing a constraint forbidding the hitting set solver to compute a given hitting set. Each set to block is encoded as a hard clause in the MaxSAT problem formulation, which is then added to the underlying oracle.
Note that an optional parameter that can be passed to this method is
weights
, which contains a mapping the objects under question into weights. Also note that the weight of an object must not change from one call ofhit()
to another.- Parameters:
to_block (iterable(obj)) – a set to block
weights (dict(obj)) – a mapping from objects to weights
- delete()#
Explicit destructor of the internal hitting set oracle.
- enumerate()#
The method can be used as a simple iterator computing and blocking the hitting sets on the fly. It essentially calls
get()
followed byblock()
. Each hitting set is reported as a list of objects in the original problem domain, i.e. it is mapped back from the solutions over Boolean variables computed by the underlying oracle.- Return type:
list(obj)
- get()#
This method computes and returns a hitting set. The hitting set is obtained using the underlying oracle operating the MaxSAT problem formulation. The computed solution is mapped back to objects of the problem domain.
- Return type:
list(obj)
- hit(to_hit, weights=None)#
This method adds a new set to hit to the hitting set solver. This is done by translating the input iterable of objects into a list of Boolean variables in the MaxSAT problem formulation.
Note that an optional parameter that can be passed to this method is
weights
, which contains a mapping the objects under question into weights. Also note that the weight of an object must not change from one call ofhit()
to another.- Parameters:
to_hit (iterable(obj)) – a new set to hit
weights (dict(obj)) – a mapping from objects to weights
- init(bootstrap_with, weights=None, subject_to=[])#
This method serves for initializing the hitting set solver with a given list of sets to hit. Concretely, the hitting set problem is encoded into partial MaxSAT as outlined above, which is then fed either to a MaxSAT solver or an MCS enumerator.
An additional optional parameter is
weights
, which can be used to specify non-unit weights for the target objects in the sets to hit. This only works if'sorted'
enumeration of hitting sets is applied.Another optional parameter is available, namely,
subject_to
. It can be used to specify arbitrary hard constraints that must be respected when computing hitting sets of the given sets. Note thatsubject_to
should be an iterable containing pure clauses and/or native AtMostK constraints. Finally, note that these hard constraints must be defined over the set of signed atomic objects, i.e. instances of classAtom
.- Parameters:
bootstrap_with (iterable(iterable(obj))) – input set of sets to hit
weights (dict(obj)) – weights of the objects in case the problem is weighted
subject_to (iterable(iterable(Atom))) – hard constraints (either clauses or native AtMostK constraints)
- oracle_time()#
Report the total SAT solving time.
- switch_phase()#
If a pure SAT-based hitting set enumeration is used, it is possible to instruct it to switch from enumerating target sets to enumerating dual sets, by polarity switching. This is what this method enables a user to do.