pycosat

https://pypi.org/project/pycosat/
Admin
pycosat provides efficient Python bindings to the PicoSAT SAT solver on the C level, enabling fast...
Tokens:1,233
Snippets:15
Trust Score:10
Update:1 month ago
Show doc for...
Tokens:
Raw
### DIMACS CNF Representation

Source: https://pypi.org/project/pycosat

Example of clauses represented in the DIMACS CNF format.

```text
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0
```

--------------------------------

### Naive Python implementation of itersolve

Source: https://pypi.org/project/pycosat

This implementation is for explanatory purposes only and should not be used in production due to performance issues and side effects on the input list.

```python
def py_itersolve(clauses): # don't use this function!
    while True:            # (it is only here to explain things)
        sol = pycosat.solve(clauses)
        if isinstance(sol, list):
            yield sol
            clauses.append([-x for x in sol])
        else: # no more solutions -- stop iteration
            return
```

--------------------------------

### Iterate All Solutions

Source: https://pypi.org/project/pycosat

Find all possible solutions for a set of clauses using pycosat.itersolve.

```python
>>> for sol in pycosat.itersolve(cnf):
...     print sol
...
[1, -2, -3, -4, 5]
[1, -2, -3, 4, -5]
[1, -2, -3, 4, 5]
...
>>> len(list(pycosat.itersolve(cnf)))
18
```

--------------------------------

### pycosat.solve(clauses, prop_limit=None, vars=None, verbose=0)

Source: https://pypi.org/project/pycosat

Finds a single solution for the given iterable of clauses.

```APIDOC
## pycosat.solve(clauses, prop_limit=None, vars=None, verbose=0)

### Description
Returns one solution as a list of integers, "UNSAT" if unsatisfiable, or "UNKNOWN" if the propagation limit is reached.

### Parameters
- **clauses** (iterable) - Required - An iterable of clauses, where each clause is an iterable of non-zero integers.
- **prop_limit** (integer) - Optional - The propagation limit.
- **vars** (integer) - Optional - Number of variables.
- **verbose** (integer) - Optional - The verbosity level.
```

--------------------------------

### Limit Solution Iteration

Source: https://pypi.org/project/pycosat

Use itertools.islice to retrieve a specific number of solutions from the itersolve iterator.

```python
>>> import itertools
>>> list(itertools.islice(pycosat.itersolve(cnf), 3))
[[1, -2, -3, -4, 5], [1, -2, -3, 4, -5], [1, -2, -3, 4, 5]]
```

--------------------------------

### pycosat.itersolve(clauses, prop_limit=None, vars=None, verbose=0)

Source: https://pypi.org/project/pycosat

Returns an iterator over all solutions for the given iterable of clauses.

```APIDOC
## pycosat.itersolve(clauses, prop_limit=None, vars=None, verbose=0)

### Description
Returns an iterator over solutions. When a propagation limit is specified, exhausting the iterator may not yield all possible solutions.

### Parameters
- **clauses** (iterable) - Required - An iterable of clauses, where each clause is an iterable of non-zero integers.
- **prop_limit** (integer) - Optional - The propagation limit.
- **vars** (integer) - Optional - Number of variables.
- **verbose** (integer) - Optional - The verbosity level.
```

--------------------------------

### Solve SAT Clauses

Source: https://pypi.org/project/pycosat

Find a single solution for a given set of clauses using pycosat.solve.

```python
>>> import pycosat
>>> cnf = [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]]
>>> pycosat.solve(cnf)
[1, -2, -3, -4, 5]
```
Tokens:
Raw