Welcome to Paramita¶
Paramita is an extensible framework for building applications around SAT, MaxSAT and related satisfiability technologies. It provides a unified API for interacting with different solvers, supports plugins written in C++ and Python, and includes modelling tools for constructing and solving problems.
Currently, Paramita has more than 30 plugins available, including SAT solvers, MaxSAT solvers and Pseudo-Boolean encoders. For a complete list of implemented plugins see this reference page.
Features¶
- Unified API for:
- Solvers (SatSolvers and MaxSatSolvers).
- Solving utilities (Propagators and Learners).
- Pseudo-Boolean encoders (PbToCnfEncoders) and decoders (CnfToPbDecoder).
- Plugin system for extending Paramita with new solvers, encoders and translators.
- More than 30 plugins available.
- Plugins can be implemented in either C++ or Python.
- Runtime loading of compiled plugins.
- Native support for IPASIR, IPASIR-UP and IPAMIR compliant solvers.
- High-level modelling language supporting:
- Boolean formulas.
- Pseudo-Boolean constraints.
- Linear objective functions.
- Python bindings generated with
nanobind1.
Quick Start¶
Paramita is available at PyPI and can be installed using pip:
Warning
At the moment, we only support Linux systems and Python versions from 3.8 to 3.13.
Windows support is currently in an internal experimental phase, while Mac support is scheduled for a future release.
The core Paramita package is independent of any specific solver. Solvers, encoders and other components are distributed as plugins that can be installed independently. For this example, we will download, compile and install CaDiCaL version 3.0.02 from the default paramita-plugins repository:
For more information about building external plugins, see the Building an external Plugin section.
Then, we can use the compiled CaDiCaL 3.0.0 SAT solver to solve a CNF formula in Python:
from paramita.solvers import SatSolver
solver = SatSolver.from_name("Cadical300")
solver.add_clauses([[1, 2], [-1, -2]])
is_sat = solver.solve()
print(is_sat)
Where to go next¶
If you are new to Paramita:
- Start with the Tutorials for complete examples. You might need to install some plugins (i.e., SAT or MaxSAT solvers), so you should check the Building an external Plugin section at some point.
If you are already familiar with Paramita:
- The How-to Guides section explains how to perform specific tasks.
- The Reference section includes the C++ and Python API References.
- The Understanding Paramita section explains some other technical details about Paramita.