Package org.mcp.sat

Class SATUtils

java.lang.Object
org.mcp.sat.SATUtils
public class SATUtils extends Object
Utility methods for SAT-based symbolic computations.

Provides helper functions for creating SAT solvers, bit vectors, checking satisfiability, and extracting assignments.

Since:
2025-02-28
Author:

  • Constructor Summary

    Constructors
    Constructor
    Description
    SATUtils()
     

  • Method Summary

    Modifier and Type
    Method
    Description
    static org.logicng.formulas.Variable[]
    bitvector(org.logicng.formulas.FormulaFactory factory, int length, int start, boolean reverse)
    Creates a bit vector of SAT variables.
    static org.logicng.formulas.Variable[]
    concatBitvectors(org.logicng.formulas.Variable[]... arrays)
    Concatenates multiple bit vectors into a single array.
    static org.logicng.solvers.SATSolver
    createSolver(org.logicng.formulas.FormulaFactory factory)
    Creates a new SAT solver instance for the given formula factory.
    static org.logicng.datastructures.Assignment
    getAssignment(org.logicng.formulas.FormulaFactory factory, org.logicng.formulas.Formula formula, org.logicng.formulas.Variable[] bitvec)
    Returns a satisfying assignment for the given formula and bit vector.
    static boolean
    isSatisfying(org.logicng.formulas.FormulaFactory factory, org.logicng.formulas.Formula formula)
    Checks if the given formula is satisfiable.

    Methods inherited from class java.lang.Object

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

  • Constructor Details

    • SATUtils

      public SATUtils()

  • Method Details

    • createSolver

      public static org.logicng.solvers.SATSolver createSolver(org.logicng.formulas.FormulaFactory factory)
      Creates a new SAT solver instance for the given formula factory.
      Parameters:
      factory - the formula factory
      Returns:
      a new SATSolver instance

    • bitvector

      public static org.logicng.formulas.Variable[] bitvector(org.logicng.formulas.FormulaFactory factory, int length, int start, boolean reverse)
      Creates a bit vector of SAT variables.
      Parameters:
      factory - the formula factory
      length - the number of bits
      start - the starting index for variable names
      reverse - whether to reverse the bit order
      Returns:
      an array of SAT variables

    • concatBitvectors

      public static org.logicng.formulas.Variable[] concatBitvectors(org.logicng.formulas.Variable[]... arrays)
      Concatenates multiple bit vectors into a single array.
      Parameters:
      arrays - arrays of SAT variables to concatenate
      Returns:
      a single concatenated array of SAT variables

    • isSatisfying

      public static boolean isSatisfying(org.logicng.formulas.FormulaFactory factory, org.logicng.formulas.Formula formula)
      Checks if the given formula is satisfiable.
      Parameters:
      factory - the formula factory
      formula - the formula to check
      Returns:
      true if satisfiable, false otherwise

    • getAssignment

      public static org.logicng.datastructures.Assignment getAssignment(org.logicng.formulas.FormulaFactory factory, org.logicng.formulas.Formula formula, org.logicng.formulas.Variable[] bitvec)
      Returns a satisfying assignment for the given formula and bit vector. Throws an assertion error if the formula is not satisfiable.
      Parameters:
      factory - the formula factory
      formula - the formula to solve
      bitvec - the bit vector variables
      Returns:
      the satisfying assignment