Package org.mcp.sat

package org.mcp.sat

SAT backend support for MCP symbolic domains and bit-vector encodings.

This package contains LogicNG-based structures for representing finite-domain constraints as propositional formulas:

• SATInteger / MutableSATInteger: integer-to-formula encoding
• SATDomain: finite-domain wrapper around SAT integer encodings
• SATUtils: solver, satisfiability, and assignment utilities

These types enable MCP to run symbolic reasoning with a SAT formula backend in parallel to the BDD backend.

Classes

Class	Description
MutableSATInteger	MutableSATInteger represents a mutable bit-vector for SAT-based integer encoding.
SATDomain<T>	SATDomain wraps a SATInteger around a finite collection of values and provides an API for working directly with those values in SAT-based symbolic computations.
SATInteger	Abstract base class for SAT-based integer encodings.
SATUtils	Utility methods for SAT-based symbolic computations.