npycomp.solvers.DPLL.

solve

DPLL.solve()

Solve a SAT problem.

Returns:

list[int] | False

A satisfying assignment if one exists, or False otherwise.

Examples

Solve a SAT problem defined by a list of clauses.

>>> from npycomp.solvers import DPLL
>>> clauses = [("x1", "~x2"), ("x1", "x2")]
>>> solver = DPLL(clauses)
>>> model = solver.solve()
>>> model
[1, None]
>>> solver.model_to_string(model)
x1 = 1, x2 ∈ {0, 1}

Reduce a problem to SAT and solve it.

>>> from npycomp.problems import Clique
>>> A = [
...     [0, 1],
...     [1, 0],
... ]
>>> k = 2
>>> clique = Clique(A, k)
>>> clauses = clique.reduce("SAT")
>>> solver = DPLL(clauses)
>>> model = solver.solve()
[1, 0, 0, 1]