at.jku.fmv.qbf.pcnf

Interface CNFEncoder

All Known Implementing Classes:

PG86

public interface CNFEncoder

A conjunctive normal form encoder.

Author:

phlo

Method Summary

Modifier and Type	Method and Description
default QBF	encode(QBF pnf) Transforms the given formula from PNF into PCNF.
List<QBF>	getClauses(QBF skeleton) Gets a list of clauses for the given propositional skeleton.

Method Detail

getClauses

List<QBF> getClauses(QBF skeleton)

Gets a list of clauses for the given propositional skeleton.

Parameters:

skeleton - a propositional skeleton

Returns:

a satisfiability equivalent list of clauses

encode

default QBF encode(QBF pnf)

Transforms the given formula from PNF into PCNF.

Parameters:

pnf - QBF in PNF

Returns:

QBF in PCNF