at.jku.fmv.qbf.pcnf

Class PG86

java.lang.Object

at.jku.fmv.qbf.pcnf.PG86

All Implemented Interfaces:

CNFEncoder

public class PG86
extends Object
implements CNFEncoder

An optimized variant of Tseitin transformation [PG86].

Removes constraints of unnegated And/Or nodes.

[PG86] D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 2(3): 293-304, 1986.

Author:

phlo

Constructor Summary

Constructors

Constructor and Description
PG86()

Method Summary

Modifier and Type	Method and Description
List<QBF>	getClauses(QBF skeleton) Gets a list of clauses for the given propositional skeleton.

Methods inherited from class java.lang.Object

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

Methods inherited from interface at.jku.fmv.qbf.pcnf.CNFEncoder

encode

Constructor Detail

PG86

public PG86()

Method Detail

getClauses

public List<QBF> getClauses(QBF skeleton)

Description copied from interface: CNFEncoder

Gets a list of clauses for the given propositional skeleton.

Specified by:

getClauses in interface CNFEncoder

Parameters:

skeleton - a propositional skeleton

Returns:

a satisfiability equivalent list of clauses