mx.unam.iimas.griffin.sat

Interface CNFConverter

All Known Implementing Classes:

TseitinCNFConverter

public interface CNFConverter

CNF converter A standarised interface for converting a sentence to conjunctive normal form (CNF)

Version:

1.0

Author:

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

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

Method Detail

getCNFFormulaAsArray

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

Returns:

an array of clauses

getCNFFormulaTree

Formula getCNFFormulaTree()

Obtains the CNF formula as a tree

Returns:

the formula

getCodingMap

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

Returns:

the map

getDecodingMap

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

Returns:

the map