Metadata-Version: 2.2
Name: pyapproxmc
Version: 4.3.1
Summary: Bindings to ApproxMC, an approximate model counter
Keywords: sat,model-counting
Author-Email: Mate Soos <soos.mate@gmail.com>
Maintainer-Email: Mate Soos <soos.mate@gmail.com>
License: MIT License
         
         Copyright (c) 2018 Meel Group
         Kuldeep Meel
         Mate Soos
         Daniel Freemont
         and others
         
         Permission is hereby granted, free of charge, to any person obtaining a copy
         of this software and associated documentation files (the "Software"), to deal
         in the Software without restriction, including without limitation the rights
         to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
         copies of the Software, and to permit persons to whom the Software is
         furnished to do so, subject to the following conditions:
         
         The above copyright notice and this permission notice shall be included in all
         copies or substantial portions of the Software.
         
         THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
         IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
         FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
         AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
         LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
         OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
         SOFTWARE.
         
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: C++
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: License :: OSI Approved :: MIT License
Classifier: Topic :: Utilities
Requires-Python: >=3.9
Description-Content-Type: text/markdown

# pyapproxmc: Python bindings to ApproxMC

Python bindings to [ApproxMC](https://github.com/meelgroup/approxmc), an
approximate model counter with PAC (Probably Approximately Correct) guarantees.
ApproxMC counts the number of satisfying assignments of CNF formulas.

## Installing

```bash
pip install pyapproxmc
```

## Building from source

```bash
# Install build tools
pip install scikit-build-core build

# Clone the repository
git clone --recurse-submodules https://github.com/meelgroup/approxmc
cd approxmc

# Build and install into a virtual environment
python -m venv .venv && source .venv/bin/activate
pip install .
```

The build system uses scikit-build-core and CMake. All C++ dependencies
(CryptoMiniSat, Arjun, and their sub-dependencies) are fetched and built
automatically by CMake during the `pip install` step. The only system library
required is [GMP](https://gmplib.org/):

- **Linux**: `sudo apt-get install libgmp-dev`  (or `dnf install gmp-devel`)
- **macOS**: `brew install gmp`

## Usage

```python
import pyapproxmc

c = pyapproxmc.Counter()
c.add_clause([1, 2, 3])
c.add_clause([3, 20])
count = c.count()
print("Approximate count is: %d*2**%d" % (count[0], count[1]))
```

`count()` may only be called **once** per `Counter` instance; create a new
`Counter` if you need to count a different formula.

The above prints `Approximate count is: 11*2**16`. Since the largest variable
in the clauses is 20, the formula has at most 2\*\*20 models; the two clauses
restrict this to approximately 11\*2\*\*16 ≈ 720896 models.

### Counting over a projection set

Pass a projection set (sampling set) to `count()` to count models projected
onto a subset of variables:

```python
import pyapproxmc

c = pyapproxmc.Counter()
c.add_clause([1, 2, 3])
c.add_clause([3, 20])
count = c.count(range(1, 10))
print("Approximate count is: %d*2**%d" % (count[0], count[1]))
```

This prints `Approximate count is: 7*2**6`, the approximate count projected
over variables 1–9.

### Adding clauses from arrays

For performance-critical code, multiple clauses can be added in one call via
`add_clauses()` with a flat, zero-terminated `array.array`. This uses the
buffer protocol and avoids per-element Python overhead:

```python
import pyapproxmc
from array import array

c = pyapproxmc.Counter()
# Clauses [1,2,3] and [3,20], each terminated by 0
c.add_clauses(array('i', [1, 2, 3, 0, 3, 20, 0]))
count = c.count()
```

Note: `add_clause()` (singular) also accepts any iterable including arrays,
but iterates element by element and does not use the buffer protocol.

## Counter constructor parameters

| Parameter   | Default | Description |
|-------------|---------|-------------|
| `seed`      | 1       | Random seed for reproducibility |
| `verbosity` | 0       | Output verbosity (0 = silent) |
| `epsilon`   | 0.8     | Tolerance: how approximate the count is |
| `delta`     | 0.2     | Confidence: probability the count is within tolerance |

Example:

```python
c = pyapproxmc.Counter(seed=42, epsilon=0.5, delta=0.1)
```

## Version

```python
import pyapproxmc
print(pyapproxmc.__version__)
```
