Package org.variantsync.diffdetective.analysis.logic

Class SAT

java.lang.Object
org.variantsync.diffdetective.analysis.logic.SAT
public final class SAT extends Object
Class with static functions for satisfiability solving, potentially with some optimizations.
Author:
Paul Bittner

  • Constructor Details

    • SAT

      private SAT()

  • Method Details

    • checkSATviaDNF

      public static boolean checkSATviaDNF(FixTrueFalse.Formula formula)

    • checkSATviaSat4J

      public static boolean checkSATviaSat4J(FixTrueFalse.Formula formula)
      Invokes a SAT solver on the given formula and returns its result.
      Parameters:
      formula - Formula to check for being satisfiable.
      Returns:
      True iff the given formula is a satisfiable.

    • isSatisfiable

      public static boolean isSatisfiable(FixTrueFalse.Formula formula)
      Checks whether the given formula is satisfiable. This method uses the Tseytin transformation for formulas with more than 40 literals as a heuristic to optimize SAT solving times for larger formulas.
      Parameters:
      formula - Formula to check for being satisfiable.
      Returns:
      True iff the given formula is a satisfiable.

    • isSatisfiable

      public static boolean isSatisfiable(org.prop4j.Node formula)
      Checks whether the given formula is satisfiable. This method uses the Tseytin transformation for formulas with more than 40 literals as a heuristic to optimize SAT solving times for larger formulas.
      Parameters:
      formula - Formula to check for being satisfiable.
      Returns:
      True iff the given formula is a satisfiable.

    • isTautology

      public static boolean isTautology(org.prop4j.Node formula)
      Checks whether the given formula is a tautology.
      Parameters:
      formula - Formula to check for being a tautology.
      Returns:
      True iff the given formula is a tautology.

    • implies

      public static boolean implies(org.prop4j.Node left, org.prop4j.Node right)
      Checks whether left => right is a tautology. This means that the left formula implies the right one for all assignments.
      Parameters:
      left - Left-hand side propositional formula of implication check.
      right - Right-hand side propositional formula of implication check.
      Returns:
      True iff left => right is a tautology.

    • equivalent

      public static boolean equivalent(org.prop4j.Node left, org.prop4j.Node right)
      Checks whether left <=> right is a tautology. This means that both formula evaluate to the same boolean value for every assignment.
      Parameters:
      left - Left-hand side propositional formula of equivalency check.
      right - Right-hand side propositional formula of equivalency check.
      Returns:
      True iff left <=> right is a tautology.