Package org.variantsync.diffdetective.analysis.logic

Class Tseytin

java.lang.Object
org.variantsync.diffdetective.analysis.logic.Tseytin
public final class Tseytin extends Object
Class with methods for Tseytin conversion. The Tseytin conversion produces an equisatisfiable CNF for a propositional formula. The produced CNF is usually small at the cost of introducing new variables.
Author:
Chico Sundermann, Paul Bittner

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    private static class 
    Tseytin.Convert
    Helper class for Tseytin conversion that remembers generated formulas.

  • Constructor Summary

    Constructors
    Modifier
    Constructor
    Description
    private
    Tseytin()
     

  • Method Summary

    Modifier and Type
    Method
    Description
    private static org.prop4j.Node
    convert(org.prop4j.Node formula, BiFunction<org.prop4j.Node,org.prop4j.Node,org.prop4j.Node> eq)
     
    static org.prop4j.Node
    toEquisatisfiableCNF(org.prop4j.Node formula)
     
    static org.prop4j.Node
    toEquivalentCNF(org.prop4j.Node formula)
     

    Methods inherited from class java.lang.Object

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

  • Constructor Details

    • Tseytin

      private Tseytin()

  • Method Details

    • convert

      private static org.prop4j.Node convert(org.prop4j.Node formula, BiFunction<org.prop4j.Node,org.prop4j.Node,org.prop4j.Node> eq)

    • toEquisatisfiableCNF

      public static org.prop4j.Node toEquisatisfiableCNF(org.prop4j.Node formula)

    • toEquivalentCNF

      public static org.prop4j.Node toEquivalentCNF(org.prop4j.Node formula)