net.sf.tweety.logics.pl.sat

Class SatSolver

java.lang.Object

net.sf.tweety.logics.pl.sat.SatSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PropositionalFormula>, ConsistencyTester<BeliefSet<PropositionalFormula>>, ConsistencyWitnessProvider<PropositionalFormula>

Direct Known Subclasses:

LingelingSolver, Sat4jSolver

public abstract class SatSolver
extends java.lang.Object
implements BeliefSetConsistencyTester<PropositionalFormula>, ConsistencyWitnessProvider<PropositionalFormula>

Abstract class for specifying SAT solvers.

Author:

Matthias Thimm

Field Summary

Fields

Modifier and Type	Field and Description
private static SatSolver	defaultSatSolver The default SAT solver.
private static java.io.File	tempFolder For temporary files.

Constructor Summary

Constructors

Constructor and Description
SatSolver()

Method Summary

Modifier and Type	Method and Description
protected static Pair<java.lang.String,java.util.List<PropositionalFormula>>	convertToDimacs(java.util.Collection<PropositionalFormula> formulas) Converts the given set of formulas to their string representation in Dimacs CNF.
protected static java.lang.String	convertToDimacs(java.util.Collection<PropositionalFormula> formulas, java.util.List<Proposition> props) Converts the given set of formulas to their string representation in Dimacs CNF.
protected static Pair<java.io.File,java.util.List<PropositionalFormula>>	createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas) Creates a temporary file in Dimacs format and also returns a mapping between formulas and clauses.
protected static java.io.File	createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas, java.util.List<Proposition> props) Creates a temporary file in Dimacs format with the given proposition2variable mapping.
static SatSolver	getDefaultSolver() Returns the default SAT solver. If a default SAT solver has been configured this solver is returned by this method.
Interpretation	getWitness(BeliefSet<PropositionalFormula> bs) If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.
abstract Interpretation	getWitness(java.util.Collection<PropositionalFormula> formulas) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
Interpretation	getWitness(PropositionalFormula formula) If the formula is consistent this method returns some model of it or, if it is inconsistent, null.
static boolean	hasDefaultSolver() Returns "true" if a default SAT solver is configured.
boolean	isConsistent(BeliefSet<PropositionalFormula> beliefSet) Checks whether the given belief base is consistent.
boolean	isConsistent(java.util.Collection<PropositionalFormula> formulas) Checks whether the given collection of formulas is consistent.
boolean	isConsistent(PropositionalFormula formula) Checks whether the given formula is consistent.
abstract boolean	isSatisfiable(java.util.Collection<PropositionalFormula> formulas) Checks whether the given set of formulas is satisfiable.
static void	setDefaultSolver(SatSolver solver) Sets the default SAT solver.
static void	setTempFolder(java.io.File tempFolder) Set the folder for temporary files created by SAT solver.

Methods inherited from class java.lang.Object

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

Field Detail

defaultSatSolver

private static SatSolver defaultSatSolver

The default SAT solver.

tempFolder

private static java.io.File tempFolder

For temporary files.

Constructor Detail

SatSolver

public SatSolver()

Method Detail

setDefaultSolver

public static void setDefaultSolver(SatSolver solver)

Sets the default SAT solver.

Parameters:

solver - some SAT solver

setTempFolder

public static void setTempFolder(java.io.File tempFolder)

Set the folder for temporary files created by SAT solver.

Parameters:

tempFolder - some temp folder.

hasDefaultSolver

public static boolean hasDefaultSolver()

Returns "true" if a default SAT solver is configured.

Returns:

"true" if a default SAT solver is configured.

getDefaultSolver

public static SatSolver getDefaultSolver()

Returns the default SAT solver.

If a default SAT solver has been configured this solver is returned by this method. If no default solver is configured, the Sat4j solver (net.sf.tweety.pl.sat.Sat4jSolver) is returned as a fallback and a message is printed to stderr pointing out that no default SAT solver is configured.

Returns:

the default SAT solver.

convertToDimacs

protected static java.lang.String convertToDimacs(java.util.Collection<PropositionalFormula> formulas,
                                                  java.util.List<Proposition> props)

Converts the given set of formulas to their string representation in Dimacs CNF. Note that a single formula may be represented as multiple clauses, so there is no simple correspondence between the formulas of the set and the Dimacs representation. Use convertToDimacs(.) for obtaining a map between those.

Parameters:

formulas - a collection of formulas

a - list of propositions (=signature) where the indices are used for writing the clauses.

Returns:

a string in Dimacs CNF.

convertToDimacs

protected static Pair<java.lang.String,java.util.List<PropositionalFormula>> convertToDimacs(java.util.Collection<PropositionalFormula> formulas)

Converts the given set of formulas to their string representation in Dimacs CNF. The return value is a pair of
1.) the string representation
2.) a list of collections of formulas (all from the given set); the interpretation of this list is that the generated clause no K originated from the propositional formula given at index k.

Parameters:

formulas - a collection of formulas.

Returns:

a string in Dimacs CNF and a mapping between clauses and original formulas.

createTmpDimacsFile

protected static java.io.File createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas,
                                                  java.util.List<Proposition> props)
                                           throws java.io.IOException

Creates a temporary file in Dimacs format with the given proposition2variable mapping.

Parameters:

formulas - a collection of formulas

a - list of propositions (=signature) where the indices are used for writing the clauses.

Returns:

the file handler.

Throws:

java.io.IOException - if something went wrong while creating a temporary file.

createTmpDimacsFile

protected static Pair<java.io.File,java.util.List<PropositionalFormula>> createTmpDimacsFile(java.util.Collection<PropositionalFormula> formulas)
                                                                                      throws java.io.IOException

Creates a temporary file in Dimacs format and also returns a mapping between formulas and clauses.

Parameters:

formulas - a collection of formulas

a - list of propositions (=signature) where the indices are used for writing the clauses (a list of collections of formulas (all from the given set); the interpretation of this list is that the generated clause no K originated from the propositional formula given at index k).

Returns:

the file handler and a mapping between clauses and original formulas.

Throws:

java.io.IOException - if something went wrong while creating a temporary file.

getWitness

public abstract Interpretation getWitness(java.util.Collection<PropositionalFormula> formulas)

If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.

Specified by:

getWitness in interface ConsistencyWitnessProvider<PropositionalFormula>

Returns:

some model of the formulas or null.

isSatisfiable

public abstract boolean isSatisfiable(java.util.Collection<PropositionalFormula> formulas)

Checks whether the given set of formulas is satisfiable.

Parameters:

formulas - a set of formulas.

Returns:

"true" if the set is consistent.

isConsistent

public boolean isConsistent(BeliefSet<PropositionalFormula> beliefSet)

Description copied from interface: ConsistencyTester

Checks whether the given belief base is consistent.

Specified by:

isConsistent in interface BeliefSetConsistencyTester<PropositionalFormula>

Specified by:

isConsistent in interface ConsistencyTester<BeliefSet<PropositionalFormula>>

Parameters:

beliefSet - a belief base.

Returns:

"true" iff the given belief base is consistent.

isConsistent

public boolean isConsistent(java.util.Collection<PropositionalFormula> formulas)

Description copied from interface: BeliefSetConsistencyTester

Checks whether the given collection of formulas is consistent.

Specified by:

isConsistent in interface BeliefSetConsistencyTester<PropositionalFormula>

Parameters:

formulas - a collection of formulas.

Returns:

"true" iff the given collection of formulas is consistent.

isConsistent

public boolean isConsistent(PropositionalFormula formula)

Description copied from interface: BeliefSetConsistencyTester

Checks whether the given formula is consistent.

Specified by:

isConsistent in interface BeliefSetConsistencyTester<PropositionalFormula>

Parameters:

formula - a formulas.

Returns:

"true" iff the formula is consistent.

getWitness

public Interpretation getWitness(PropositionalFormula formula)

Description copied from interface: ConsistencyWitnessProvider

If the formula is consistent this method returns some model of it or, if it is inconsistent, null.

Specified by:

getWitness in interface ConsistencyWitnessProvider<PropositionalFormula>

Returns:

some model of the formula or null.

getWitness

public Interpretation getWitness(BeliefSet<PropositionalFormula> bs)

Description copied from interface: ConsistencyWitnessProvider

If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.

Specified by:

getWitness in interface ConsistencyWitnessProvider<PropositionalFormula>

Returns:

some model of the belief set or null.