Metadata-Version: 2.4
Name: aperture-solver
Version: 0.1.0.dev1
Summary: A SAT-based optimization solver
Home-page: 
Author: Yam Slonimski
Author-email: Yam Slonimski <yamslonimski@campus.technion.ac.il>
License-Expression: MIT
Keywords: SAT,MaxSAT,OBV,Black-Box,solver,optimization,constraint,satisfiability
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 :: C++
Classifier: Operating System :: POSIX :: Linux
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Intended Audience :: Science/Research
Classifier: Intended Audience :: Developers
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: author
Dynamic: license-file
Dynamic: requires-python

# Aperture Python API

Aperture is a SAT-based optimization solver providing a Python interface for:
- **SAT solving** – check satisfiability of CNF Boolean formulas
- **MaxSAT solving** – minimize satisfied (weighted) soft literals
- **OBV solving** – optimize modulo bit-vector problems
- **Black-box optimization** – optimize generic objective functions

All solving quiries can be called incrementally under assumptions.

## Quick Start

```python
import aperture as ap

solver = ap.Solver(sat_solver="topor")
x = solver.new_var()
y = solver.new_var()

solver.add_clause(ap.lits([x, y]))  # x OR y

sat = solver.solve()

if sat:
    print("SAT")
    print(solver.get_latest_solution())
else:
    print(solver.get_latest_solve_status())
```

## Supported SAT Solvers

- `"topor"` 
- `"cadical"`
- `"glucose"` (default)
- `"kissat"` – initial SAT query only

## Core Methods

| Method | Purpose |
|--------|---------|
| `new_var()` | Create a new Boolean variable |
| `add_clause(lits)` | Add a clause |
| `solve(assumptions=[])` | Solve SAT |
| `solve_maxsat(assumptions, soft_lits, fix_model_value, callback_on_solution_found=None)` | Solve MaxSAT |
| `solve_weighted_maxsat(assumptions, soft_wlits, fix_model_value, callback_on_solution_found=None)` | Solve weighted MaxSAT |
| `solve_obv(assumptions, targets, callback_on_solution_found=None)` | Optimize bit-vectors |
| `solve_black_box(assumptions, observables, pb_func, callback_on_solution_found=None)` | Black-box optimization |
| `get_latest_solution()` | Get solution (assignment) of the last solve query |
| `get_latest_solve_status()` | Get status ("SAT", "UNSAT", "ERROR", "UNKNOWN") |

## Constraints

Add cardinality and pseudo-Boolean constraints:
- `add_constraint_less_than((w)lits, rhs, selector=None)`
- `add_constraint_less_than_equal((w)lits, rhs, selector=None)`
- `add_constraint_equal(lits, rhs, selector=None)`
- `add_constraint_greater_than_equal(lits, rhs, selector=None)`
- `add_constraint_greater_than(lits, rhs, selector=None)`

All methods return `bool` ans supports adding an optional selector to all the generated clauses. <br>
Note that currently only < and <= constraints are supported for weighted literals (wlits).

## Documentation

For further information and examples, see the [notebook](https://github.com/YamSln/Aperture/tree/main/aperture/docs/notebooks) in the docs/ directory. ReadTheDocs documentation will be available in the future.
