Package org.tweetyproject.logics.pl.sat

Class DimacsSatSolver

java.lang.Object

org.tweetyproject.logics.pl.sat.SatSolver

org.tweetyproject.logics.pl.sat.DimacsSatSolver

All Implemented Interfaces:

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

Direct Known Subclasses:

CmdLineSatSolver, Sat4jSolver

public abstract class DimacsSatSolver
extends SatSolver

Interface for SAT solvers which work on the Dimacs format. It adds some utility methods for directly manipulating clauses in Dimacs format.

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor	Description
DimacsSatSolver()	Default Constructor

Method Summary

Modifier and Type	Method	Description
static List<String>	convertToDimacs(Collection<PlFormula> formulas)	Converts the given set of formulas to their string representation in Dimacs CNF.
static List<String>	convertToDimacs(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, List<String> additional_clauses)	Convert to dimacs
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.
abstract Interpretation<PlBeliefSet,PlFormula>	getWitness(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index, List<String> additional_clauses)	If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
abstract boolean	isInstalled()	Return whether the solve ris installed
boolean	isSatisfiable(Collection<PlFormula> formulas)	Checks whether the given set of formulas is satisfiable.
abstract boolean	isSatisfiable(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, List<String> additional_clauses)	Checks whether the given set of formulas is satisfiable.
static void	setTempFolder(File tempFolder)	Set the folder for temporary files created by SAT solver.

Methods inherited from class org.tweetyproject.logics.pl.sat.SatSolver

getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver

Methods inherited from class java.lang.Object

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

Constructor Details

DimacsSatSolver

public DimacsSatSolver()

Default Constructor

Method Details

setTempFolder

public static void setTempFolder(File tempFolder)

Set the folder for temporary files created by SAT solver.

Parameters:

tempFolder - some temp folder.

convertToDimacs

public static List<String> convertToDimacs(Collection<PlFormula> formulas)

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.

Parameters:

formulas - a collection of formulas

Returns:

a list of strings in Dimacs CNF.

convertToDimacs

public static List<String> convertToDimacs(Collection<PlFormula> formulas,
 Map<Proposition,Integer> prop_index,
 List<String> additional_clauses)

Convert to dimacs

Parameters:

formulas - a collection of formulas

prop_index - a map mapping propositions (=signature) to the indices that are used for writing the clauses.

additional_clauses - additional clauses to be considered

Returns:

a list of strings in Dimacs CNF.

getWitness

public 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>

Specified by:

getWitness in class SatSolver

Parameters:

formulas - a set of formulas

Returns:

some model of the formulas or null.

getWitness

public abstract Interpretation<PlBeliefSet,PlFormula> getWitness(Collection<PlFormula> formulas,
 Map<Proposition,Integer> prop_index,
 Map<Integer,Proposition> prop_inverted_index,
 List<String> additional_clauses)

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

Parameters:

formulas - a set of formulas

prop_index - mapping propositions to numbers used for representing the SAT instance

prop_inverted_index - inverted index of prop_index

additional_clauses - additional clauses in text form to be added (already correctly formatted in CNF!)

Returns:

some model of the formulas or null.

isSatisfiable

public boolean isSatisfiable(Collection<PlFormula> formulas)

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class SatSolver

Parameters:

formulas - a set of formulas.

Returns:

"true" if the set is consistent.

isSatisfiable

public abstract boolean isSatisfiable(Collection<PlFormula> formulas,
 Map<Proposition,Integer> prop_index,
 List<String> additional_clauses)

Checks whether the given set of formulas is satisfiable.

Parameters:

formulas - a set of formulas.

prop_index - maps propositions to the number that shall be used to represent it (a natural number > 0).

additional_clauses - additional clauses in text form to be added (already correctly formatted in CNF!)

Returns:

"true" if the set is consistent.

isInstalled

public abstract boolean isInstalled()

Description copied from class: SatSolver

Return whether the solve ris installed

Specified by:

isInstalled in class SatSolver

Returns:

whether the solve ris installed