Package org.mcp.sat

Class SATInteger

java.lang.Object
org.mcp.sat.SATInteger
All Implemented Interfaces:
Serializable
Direct Known Subclasses:
MutableSATInteger
public abstract class SATInteger extends Object implements Serializable
Abstract base class for SAT-based integer encodings.

Provides methods for encoding, decoding, and querying integer values using SAT formulas. Supports conversion between SAT assignments and integer values, and value constraints.

Since:
2025-02-28
Author:
See Also:

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    protected final org.logicng.formulas.Variable[]
    _bitvec
    Bit vector representing the integer (each bit is a SAT variable).
    protected final org.logicng.formulas.FormulaFactory
    _factory
    Formula factory for creating SAT formulas.
    protected final long
    _maxVal
    Maximum value representable by this SATInteger.

  • Constructor Summary

    Constructors
    Modifier
    Constructor
    Description
    protected
    SATInteger(org.logicng.formulas.FormulaFactory factory, org.logicng.formulas.Variable[] bitvec)
    Constructs a SATInteger from a formula factory and bit vector.

  • Method Summary

    Modifier and Type
    Method
    Description
    protected abstract org.logicng.formulas.Formula
    firstBitsEqual(long val, int length)
    Returns a formula representing the first length bits equal to the given value.
    org.logicng.formulas.Variable[]
    getBitvec()
    Returns the bit vector.
    org.logicng.formulas.FormulaFactory
    getFactory()
    Returns the formula factory.
    Long
    getValueSatisfying(org.logicng.formulas.Formula formula)
    Returns the value satisfying the given formula, or 0 if unsatisfiable.
    int
    getValueSatisfyingToInt(org.logicng.formulas.Formula formula)
    Converts a SAT assignment to an int value.
    List<Long>
    getValuesSatisfying(org.logicng.formulas.Formula formula, int max)
    Returns a list of values satisfying the input formula, up to a maximum number.
    abstract long
    satAssignmentToLong(org.logicng.datastructures.Assignment assignment)
    Converts a SAT assignment to a long value.
    int
    size()
    Returns the number of bits in this SATInteger.
    final org.logicng.formulas.Formula
    value(long val)
    Returns a formula representing the exact value.

    Methods inherited from class java.lang.Object

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

  • Field Details

    • _factory

      protected final org.logicng.formulas.FormulaFactory _factory
      Formula factory for creating SAT formulas.

    • _bitvec

      protected final org.logicng.formulas.Variable[] _bitvec
      Bit vector representing the integer (each bit is a SAT variable).

    • _maxVal

      protected final long _maxVal
      Maximum value representable by this SATInteger.

  • Constructor Details

    • SATInteger

      protected SATInteger(org.logicng.formulas.FormulaFactory factory, org.logicng.formulas.Variable[] bitvec)
      Constructs a SATInteger from a formula factory and bit vector.
      Parameters:
      factory - the formula factory
      bitvec - the bit vector (array of SAT variables)

  • Method Details

    • size

      public int size()
      Returns the number of bits in this SATInteger.
      Returns:
      the number of bits

    • satAssignmentToLong

      public abstract long satAssignmentToLong(org.logicng.datastructures.Assignment assignment)
      Converts a SAT assignment to a long value.
      Parameters:
      assignment - the SAT assignment
      Returns:
      the corresponding long value

    • getValueSatisfyingToInt

      public int getValueSatisfyingToInt(org.logicng.formulas.Formula formula)
      Converts a SAT assignment to an int value. Only supports up to 31 bits.
      Parameters:
      formula - the SAT formula assignment
      Returns:
      the corresponding int value

    • getValueSatisfying

      public Long getValueSatisfying(org.logicng.formulas.Formula formula)
      Returns the value satisfying the given formula, or 0 if unsatisfiable.
      Parameters:
      formula - the SAT formula assignment
      Returns:
      the value as a Long, or 0L if unsatisfiable

    • getValuesSatisfying

      public List<Long> getValuesSatisfying(org.logicng.formulas.Formula formula, int max)
      Returns a list of values satisfying the input formula, up to a maximum number.
      Parameters:
      formula - the SAT formula constraint
      max - the maximum number of values desired
      Returns:
      the list of satisfying values

    • value

      public final org.logicng.formulas.Formula value(long val)
      Returns a formula representing the exact value.
      Parameters:
      val - the value to encode
      Returns:
      the formula representing the value

    • getFactory

      public org.logicng.formulas.FormulaFactory getFactory()
      Returns the formula factory.
      Returns:
      the formula factory

    • getBitvec

      public org.logicng.formulas.Variable[] getBitvec()
      Returns the bit vector.
      Returns:
      the bit vector (array of SAT variables)

    • firstBitsEqual

      protected abstract org.logicng.formulas.Formula firstBitsEqual(long val, int length)
      Returns a formula representing the first length bits equal to the given value.
      Parameters:
      val - the value to compare
      length - the number of bits to check
      Returns:
      the formula representing the equality