# `satisfiability`¶

Functionality for determining logic satisfiasbility.

## `satisfiability.picosat` module¶

Python wrapper around the _clibs PicoSAT extension.

`tt.satisfiability.picosat.``sat_all`(clauses, assumptions=None)[source]

Find all solutions that satisfy the specified clauses and assumptions.

This provides a light Python wrapper around the same method in the PicoSAT C-extension. While completely tested and usable, this method is probably not as useful as the interface provided through the `sat_all` method in the `BooleanExpression` class.

Parameters: clauses (List[List[`int`]]) – CNF (AND of ORs) clauses; positive integers represent non-negated terms and negative integers represent negated terms. assumptions (List[`int`]) – Assumed terms; same negation logic from `clauses` applies here. Note that assumptions cannot be an empty list; leave it as `None` if there are no assumptions to include. An iterator of solutions; if no satisfiable solutions exist, the iterator will be empty. Iterator[List[`int`]] InvalidArgumentTypeError – If `clauses` is not a list of lists of ints or `assumptions` is not a list of ints. InvalidArgumentValueError – If any literal ints are equal to zero.

Here’s an example showing the basic usage:

```>>> from tt import picosat
>>> for solution in picosat.sat_all([, [2, 3, 4], [2, 3]]):
...     print(solution)
...
[1, 2, 3, 4]
[1, 2, 3, -4]
[1, 2, -3, 4]
[1, 2, -3, -4]
[1, -2, 3, 4]
[1, -2, 3, -4]
```

We can cut down on some of the above solutions by including an assumption:

```>>> for solution in picosat.sat_all([, [2, 3, 4], [2, 3]],
...                                 assumptions=[-3]):
...     print(solution)
...
[1, 2, -3, 4]
[1, 2, -3, -4]
```
`tt.satisfiability.picosat.``sat_one`(clauses, assumptions=None)[source]

Find a solution that satisfies the specified clauses and assumptions.

This provides a light Python wrapper around the same method in the PicoSAT C-extension. While completely tested and usable, this method is probably not as useful as the interface provided through the `sat_one` method in the `BooleanExpression` class.

Parameters: clauses (List[List[`int`]]) – CNF (AND of ORs) clauses; positive integers represent non-negated terms and negative integers represent negated terms. assumptions (List[`int`]) – Assumed terms; same negation logic from `clauses` applies here. Note that assumptions cannot be an empty list; leave it as `None` if there are no assumptions to include. If solution is found, a list of ints representing the terms of the solution; otherwise, if no solution found, `None`. List[`int`] or `None` InvalidArgumentTypeError – If `clauses` is not a list of lists of ints or `assumptions` is not a list of ints. InvalidArgumentValueError – If any literal ints are equal to zero.

Let’s look at a simple example with no satisfiable solution:

```>>> from tt import picosat
>>> picosat.sat_one([, [-1]]) is None
True
```

Here’s an example where a solution exists:

```>>> picosat.sat_one([[1, 2, 3], [-2, -3], [1, -2], [2, -3], [-2]])
[1, -2, -3]
```

Finally, here’s an example using assumptions:

```>>> picosat.sat_one([[1, 2, 3], [2, 3]], assumptions=[-1, -3])
[-1, 2, -3]
```