Package org.tweetyproject.logics.pl.sat

Class SatSolver

java.lang.Object

org.tweetyproject.logics.pl.sat.SatSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

Direct Known Subclasses:

DimacsSatSolver, MaxSatSolver, SimpleDpllSolver

public abstract class SatSolver
extends Object
implements BeliefSetConsistencyTester<PlFormula>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

Abstract class for specifying SAT solvers. Also includes methods to convert knowledge bases into the Dimacs format.

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor	Description
SatSolver()	Default Constructor

Method Summary

Modifier and Type	Method	Description
static SatSolver	getDefaultSolver()	Returns the default SAT solver. If a default SAT solver has been configured this solver is returned by this method.
abstract Interpretation<PlBeliefSet,PlFormula>	getWitness(Collection<PlFormula> formulas)	If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
Interpretation<PlBeliefSet,PlFormula>	getWitness(BeliefSet<PlFormula,?> bs)	If the belief set is consistent this method returns some model of it or, if it is inconsistent, null.
Interpretation<PlBeliefSet,PlFormula>	getWitness(PlFormula 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(Collection<PlFormula> formulas)	Checks whether the given collection of formulas is consistent.
boolean	isConsistent(BeliefSet<PlFormula,?> beliefSet)	Checks whether the given belief base is consistent.
boolean	isConsistent(PlFormula formula)	Checks whether the given formula is consistent.
abstract boolean	isInstalled()	Return whether the solve ris installed
abstract boolean	isSatisfiable(Collection<PlFormula> formulas)	Checks whether the given set of formulas is satisfiable.
static void	setDefaultSolver(SatSolver solver)	Sets the default SAT solver.

Methods inherited from class java.lang.Object

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

Constructor Details

SatSolver

public SatSolver()

Default Constructor

Method Details

setDefaultSolver

public static void setDefaultSolver(SatSolver solver)

Sets the default SAT solver.

Parameters:

solver - some SAT solver

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 (org.tweetyproject.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.

getWitness

public abstract Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> 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<PlBeliefSet,PlFormula>

Parameters:

formulas - a set of formulas

Returns:

some model of the formulas or null.

isSatisfiable

public abstract boolean isSatisfiable(Collection<PlFormula> 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<PlFormula,?> beliefSet)

Description copied from interface: ConsistencyTester

Checks whether the given belief base is consistent.

Specified by:

isConsistent in interface BeliefSetConsistencyTester<PlFormula>

Specified by:

isConsistent in interface ConsistencyTester<BeliefSet<PlFormula,?>>

Parameters:

beliefSet - a belief base.

Returns:

"true" iff the given belief base is consistent.

isConsistent

public boolean isConsistent(Collection<PlFormula> formulas)

Description copied from interface: BeliefSetConsistencyTester

Checks whether the given collection of formulas is consistent.

Specified by:

isConsistent in interface BeliefSetConsistencyTester<PlFormula>

Parameters:

formulas - a collection of formulas.

Returns:

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

isConsistent

public boolean isConsistent(PlFormula formula)

Description copied from interface: BeliefSetConsistencyTester

Checks whether the given formula is consistent.

Specified by:

isConsistent in interface BeliefSetConsistencyTester<PlFormula>

Parameters:

formula - a formulas.

Returns:

"true" iff the formula is consistent.

getWitness

public Interpretation<PlBeliefSet,PlFormula> getWitness(PlFormula 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<PlBeliefSet,PlFormula>

Parameters:

formula - a formula

Returns:

some model of the formula or null.

getWitness

public Interpretation<PlBeliefSet,PlFormula> getWitness(BeliefSet<PlFormula,?> 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<PlBeliefSet,PlFormula>

Parameters:

bs - a belief set

Returns:

some model of the belief set or null.

isInstalled

public abstract boolean isInstalled()

Return whether the solve ris installed

Returns:

whether the solve ris installed