mx.unam.iimas.griffin.sat

Class TseitinCNFConverter

java.lang.Object

mx.unam.iimas.griffin.sat.TseitinCNFConverter

All Implemented Interfaces:

CNFConverter

public class TseitinCNFConverter
extends java.lang.Object
implements CNFConverter

Converts a tree formula to CNF using Tseitin method

Version:

1.0

Author:

Stalin Muñoz Gutiérrez (stalinmunoz@yahoo.com)

Constructor Summary

Constructors

Constructor and Description
TseitinCNFConverter(Formula formula) Creates a converter for the given formula

Method Summary

Modifier and Type	Method and Description
int[][]	getCNFFormulaAsArray() Obtains the CNF representation of the formula as an array of integers The CNF is simply an array of clauses, a clause is an array of literals a literal is simply a positive or a negative integer, a positive number n represents the n-th propositional variable a negative number n represents the negation of the n-th propositional variable
Formula	getCNFFormulaTree() Obtains the CNF formula as a tree
java.util.Map<Variable,java.lang.Integer>	getCodingMap() Obtains the coding map that relates the original variables to their index in CNF array of indices representation
java.util.Map<java.lang.Integer,Variable>	getDecodingMap() Obtains the decoding map that relates the indices in the CNF array of indices representation to the variables in the formula

Methods inherited from class java.lang.Object

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

Constructor Detail

TseitinCNFConverter

public TseitinCNFConverter(Formula formula)

Creates a converter for the given formula

Parameters:

formula - the tree formula to convert

Method Detail

getCNFFormulaAsArray

public int[][] getCNFFormulaAsArray()

Description copied from interface: CNFConverter

Obtains the CNF representation of the formula as an array of integers The CNF is simply an array of clauses, a clause is an array of literals a literal is simply a positive or a negative integer, a positive number n represents the n-th propositional variable a negative number n represents the negation of the n-th propositional variable

Specified by:

getCNFFormulaAsArray in interface CNFConverter

Returns:

an array of clauses

getCNFFormulaTree

public Formula getCNFFormulaTree()

Description copied from interface: CNFConverter

Obtains the CNF formula as a tree

Specified by:

getCNFFormulaTree in interface CNFConverter

Returns:

the formula

getCodingMap

public java.util.Map<Variable,java.lang.Integer> getCodingMap()

Description copied from interface: CNFConverter

Obtains the coding map that relates the original variables to their index in CNF array of indices representation

Specified by:

getCodingMap in interface CNFConverter

Returns:

the map

getDecodingMap

public java.util.Map<java.lang.Integer,Variable> getDecodingMap()

Description copied from interface: CNFConverter

Obtains the decoding map that relates the indices in the CNF array of indices representation to the variables in the formula

Specified by:

getDecodingMap in interface CNFConverter

Returns:

the map