npycomp.problems.ThreeSAT.

reduce

ThreeSAT.reduce(target)

Reduce the problem to a specified target problem.

Consults a directory of known problems and reduction functions to traverse a path of problem transformations. For example, if reducing from TSP to SAT is possible, this method looks up the appropriate chain of reductions and applies them sequentially to transform the current problem’s parameters.

Parameters:

targetstr

The name of the target problem (e.g., ‘SAT’, ‘clique’, etc.).

Returns:

dict

A dictionary of keyword arguments representing the target problem instance. This dictionary is typically consumed by the corresponding problem’s constructor.

Raises:

NotImplementedError

If the target problem is unknown, or if there is a missing link in the chain of reduction functions required to reach the target.

See also

npycomp.reductions

Directory of known reduction functions.

Examples

To reduce a clique problem to SAT clauses:

>>> from npycomp.problems import Clique
>>>
>>> A = [
...     [0, 1],
...     [1, 0],
... ]
>>> k = 2
>>> clique = Clique(A, k)
>>> clique.reduce("SAT")
[['y_0_0', 'y_1_0'],
['y_0_1', 'y_1_1'],
['~y_0_0', '~y_0_1'],
['~y_1_0', '~y_1_1']]

These clauses can then be passed to a SAT solver to find a satisfying assignment.

>>> from npycomp.problems import SAT
>>> sat = SAT(clique.reduce("SAT"))
>>> sat.solve()
[1, 0, 0, 1]