Minimum/minimal hitting set solver (pysat.examples.hitman)

List of classes

Hitman

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.

1

Erick Moreno-Centeno, Richard M. Karp. The Implicit Hitting Set Approach to Solve Combinatorial Optimization Problems with an Application to Multigenome Alignment. Operations Research 61(2). 2013. pp. 453-468

2

António Morgado, Carmine Dodaro, Joao Marques-Silva. Core-Guided MaxSAT with Soft Cardinality Constraints. CP 2014. pp. 564-573

3

António Morgado, Alexey Ignatiev, Joao Marques-Silva. MSCG: Robust Core-Guided MaxSAT Solving. JSAT 9. 2014. pp. 129-134

4

Alexey Ignatiev, António Morgado, Joao Marques-Silva. RC2: a Python-based MaxSAT Solver. MaxSAT Evaluation 2018. p. 22

5

Carlos Mencía, Alessandro Previti, Joao Marques-Silva. Literal-Based MCS Extraction. IJCAI. 2015. pp. 1973-1979

6

Joao Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, Anton Belov. On Computing Minimal Correction Subsets. IJCAI. 2013. pp. 615-622

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 7 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)
7

Jessica Davies, Fahiem Bacchus. Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. CP 2011. pp. 225-239

Module details

class examples.hitman.Hitman(bootstrap_with=[], solver='g3', htype='sorted')

A cardinality-/subset-minimal hitting set enumerator. The enumerator can be set up to use either a MaxSAT solver RC2 or an MCS enumerator (either LBX or MCSls). 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.

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 setting htype to one of the following values: 'maxsat', 'mxsat', or 'rc2'. Alternatively, by setting it to 'mcs' or 'lbx', a user can enforce using the LBX MCS enumerator. If htype is set to 'mcsls', the MCSls enumerator is used.

In either case, an underlying problem solver can use a SAT oracle specified as an input parameter solver. The default SAT solver is Glucose3 (specified as g3, see SolverNames for details).

Objects of class Hitman can be bootstrapped with an iterable of iterables, e.g. a list of lists. This is handled using the bootstrap_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 in init().

Parameters
  • bootstrap_with (iterable(iterable(obj))) – input set of sets to hit

  • solver (str) – name of SAT solver

  • htype (str) – enumerator type

block(to_block)

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.

Parameters

to_block (iterable(obj)) – a set to block

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 by block(). 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)

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.

Parameters

to_hit (iterable(obj)) – a new set to hit

init(bootstrap_with)

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.

Parameters

bootstrap_with (iterable(iterable(obj))) – input set of sets to hit