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

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

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.
Note that currently only < and <= constraints are supported for weighted literals (wlits).

Documentation

For further information and examples, see the notebook in the docs/ directory. ReadTheDocs documentation will be available in the future.