Package org.mcp.core

Class MCPFactory

java.lang.Object
org.mcp.core.MCPLabels
org.mcp.core.MCPFactory
public class MCPFactory extends MCPLabels
The MCPFactory class extends MCPLabels and manages symbolic representations of sets of constraints.

Supports both Binary Decision Diagrams (BDD) and SAT formula backends. Provides methods for creating, updating, and querying BDD/SAT domains, as well as converting between representations and exporting to DOT format for visualization.

Since:
2025-02-28

  • Constructor Details

    • MCPFactory

      public MCPFactory()
      Constructs a new MCPFactory instance with BDD as the default backend. Initializes the BDDFactory and internal data structures.

    • MCPFactory

      public MCPFactory(MCPFactory.MCPType type)
      Constructs a new MCPFactory instance with the specified backend type.
      Parameters:
      type - the backend type to use (SAT or BDD)

    • MCPFactory

      public MCPFactory(MCPFactory other)
      Constructs a new MCPFactory instance by copying the state from another MCPFactory.
      Parameters:
      other - the MCPFactory instance to copy from

  • Method Details

    • getSatFactory

      public org.logicng.formulas.FormulaFactory getSatFactory()
      Returns the SAT FormulaFactory if the backend type is SAT.
      Returns:
      the FormulaFactory for SAT
      Throws:
      UnsupportedOperationException - if the backend is not SAT

    • getNumBits

      public Integer getNumBits()
      Returns the total number of bits used in the BDD or SAT representation.
      Returns:
      the number of bits

    • getOne

      public MCPBitVector getOne()
      Returns a bit vector representing logical one (true) for the current backend type.
      Returns:
      MCPBitVector representing logical one

    • getTrue

      public MCPBitVector getTrue()
      Returns a bit vector representing logical true for all domains.
      Returns:
      MCPBitVector representing logical true for all domains

    • isTautology

      public boolean isTautology(Object value)
      Checks if the given value is a tautology (always true).
      Parameters:
      value - the value to check (should be an MCPBitVector)
      Returns:
      true if the value is a tautology, false otherwise

    • isContradiction

      public boolean isContradiction(Object value)
      Checks if the given value is a contradiction (always false).
      Parameters:
      value - the value to check (should be an MCPBitVector)
      Returns:
      true if the value is a contradiction, false otherwise

    • isSatisfying

      public boolean isSatisfying(Object value)
      Checks if the given value is satisfiable.
      Parameters:
      value - the value to check (should be an MCPBitVector)
      Returns:
      true if the value is satisfiable, false otherwise

    • getFalse

      public MCPBitVector getFalse()
      Returns a bit vector representing logical false for the current backend type.
      Returns:
      MCPBitVector representing logical false

    • updates

      public void updates()
      Updates the internal state of the MCPFactory. Recomputes labels, sets the number of BDD variables, and initializes each domain.

    • getBDDResults

      public List<HashMap<String,Integer>> getBDDResults(net.sf.javabdd.BDD bdd)
      Returns all possible satisfying assignments from a given BDD.
      Parameters:
      bdd - the input BDD
      Returns:
      a list of maps, each mapping domain names to integer values for one assignment

    • getBDDResult

      public HashMap<String,Integer> getBDDResult(net.sf.javabdd.BDD bdd)
      Returns a single satisfying assignment from a BDD as a map of domain names to integer values.
      Parameters:
      bdd - the input BDD
      Returns:
      a map from domain names to integer values for one assignment

    • getLabel

      public MCPBitVector getLabel(String domainName, Label value)
      Returns a bit vector representing the given label in the specified domain.
      Parameters:
      domainName - the domain name
      value - the label value
      Returns:
      MCPBitVector representing the label

    • getLabelFillOtherDomain

      public MCPBitVector getLabelFillOtherDomain(String domainName, Label value)
      Returns a bit vector for the given label in one domain, and true in all other domains.
      Parameters:
      domainName - the domain name
      value - the label value
      Returns:
      MCPBitVector representing the label with other domains filled as true

    • getVar

      public MCPBitVector getVar(String domainName, Object value)
      Returns a bit vector representing the given value in the specified domain.
      Parameters:
      domainName - the domain name
      value - the value
      Returns:
      MCPBitVector representing the value

    • getVarFillOtherDomain

      public MCPBitVector getVarFillOtherDomain(String domainName, Object value)
      Returns a bit vector for the given value in one domain, and true in all other domains.
      Parameters:
      domainName - the domain name
      value - the value
      Returns:
      MCPBitVector representing the value with other domains filled as true

    • dot

      public String dot(net.sf.javabdd.BDD bdd)
      Converts a BDD to the Graphviz DOT format for visualization.
      Parameters:
      bdd - the input BDD
      Returns:
      a string representing the BDD in DOT format