Getting started

This section describes how to get started with Pindakaas.

Installation

$ pip install pindakaas

Basic example

#!/usr/bin/env python
import pindakaas

# Instantiate solver, create two new literals, and encode a XOR constraint
slv = pindakaas.solver.CaDiCaL()
x, y, z = slv.new_vars(3)
slv += x ^ y

# Solve and inspect status and literal values
with slv.solve() as result:
    assert result.status == pindakaas.solver.Status.SATISFIED
    assert result.value(x) != result.value(y)

Further examples

Model and encode Boolean formulae and pseudo-Boolean constraints:

#!/usr/bin/env python
import pindakaas

f = pindakaas.CNF()
x, y, z = f.new_vars(3)
f += (x & ~y) | (y == z)  # `x and not y, or y iff z`
f += 2 * x + 3 * y + 5 * z <= 6
print(f.to_dimacs())

Solve incrementally using assumptions:

#!/usr/bin/env python
import pindakaas

f = pindakaas.CNF()
x, y, z = f.new_vars(3)
f += (x & ~y) | (y == z)  # `x and not y, or y iff z`
f += 2 * x + 3 * y + 5 * z <= 6
print(f.to_dimacs())