Package org.mcp.sat

Class SATDomain<T>

java.lang.Object
org.mcp.sat.SATDomain<T>
public final class SATDomain<T> extends Object
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.

Supports encoding, decoding, and value lookup for SAT-based domains.

Since:
2025-02-28
Author:

  • Constructor Summary

    Constructors
    Constructor
    Description
    SATDomain(org.logicng.formulas.FormulaFactory factory, List<T> values, int index)
    Constructs a SATDomain from a formula factory, value list, and bit index offset.
    SATDomain(SATDomain<T> other)
    Copy constructor.

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    equals(Object o)
    Checks equality with another object.
    MutableSATInteger
    getInteger()
    Returns the underlying MutableSATInteger.
    int
    hashCode()
    Returns the hash code for this SATDomain.
    static int
    numBits(int size)
    Returns the number of bits used to represent a domain of the given size.
    T
    satAssignmentToValue(org.logicng.formulas.Formula satAssignment)
    Decodes a SAT assignment to the corresponding value in the domain.
    void
    setInteger(MutableSATInteger i)
    Sets the underlying MutableSATInteger.
    org.logicng.formulas.Formula
    value(T value)
    Returns a formula representing the assignment of the given value.

    Methods inherited from class java.lang.Object

    clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

  • Constructor Details

    • SATDomain

      public SATDomain(org.logicng.formulas.FormulaFactory factory, List<T> values, int index)
      Constructs a SATDomain from a formula factory, value list, and bit index offset.
      Parameters:
      factory - the formula factory
      values - the list of values in the domain
      index - the starting bit index

    • SATDomain

      public SATDomain(SATDomain<T> other)
      Copy constructor.
      Parameters:
      other - the SATDomain to copy

  • Method Details

    • numBits

      public static int numBits(int size)
      Returns the number of bits used to represent a domain of the given size.
      Parameters:
      size - the number of elements in the domain
      Returns:
      the number of bits required

    • value

      public org.logicng.formulas.Formula value(T value)
      Returns a formula representing the assignment of the given value.
      Parameters:
      value - the value to encode
      Returns:
      the formula representing the value

    • satAssignmentToValue

      public T satAssignmentToValue(org.logicng.formulas.Formula satAssignment)
      Decodes a SAT assignment to the corresponding value in the domain.
      Parameters:
      satAssignment - the SAT assignment formula
      Returns:
      the value corresponding to the assignment

    • getInteger

      public MutableSATInteger getInteger()
      Returns the underlying MutableSATInteger.
      Returns:
      the MutableSATInteger

    • setInteger

      public void setInteger(MutableSATInteger i)
      Sets the underlying MutableSATInteger.
      Parameters:
      i - the MutableSATInteger to set

    • equals

      public boolean equals(Object o)
      Checks equality with another object.
      Overrides:
      equals in class Object
      Parameters:
      o - the object to compare
      Returns:
      true if equal, false otherwise

    • hashCode

      public int hashCode()
      Returns the hash code for this SATDomain.
      Overrides:
      hashCode in class Object
      Returns:
      the hash code