Class Sat4jSolver

java.lang.Object

org.tweetyproject.logics.pl.sat.SatSolver

org.tweetyproject.logics.pl.sat.DimacsSatSolver

org.tweetyproject.logics.pl.sat.Sat4jSolver

All Implemented Interfaces:

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

public class Sat4jSolver
extends DimacsSatSolver

Uses the Sat4j library for SAT solving (note that currently only the light version is used).

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor	Description
Sat4jSolver()	Creates a new solver with default parameters (maxvar=1000000, nbclauses=500000).
Sat4jSolver(int maxvar, int nbclauses)	Creates a new solver with the given parameters.

Method Summary

Modifier and Type	Method	Description
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.
boolean	isInstalled()	Return whether the solve ris installed
boolean	isSatisfiable(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, List<String> additional_clauses)	Checks whether the given set of formulas is satisfiable.

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

convertToDimacs, convertToDimacs, getWitness, isSatisfiable, setTempFolder

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

Sat4jSolver

public Sat4jSolver(int maxvar,
 int nbclauses)

Creates a new solver with the given parameters.

Parameters:

maxvar - Max number of variables for this solver.

nbclauses - Max number of expected clauses for this solver.

Sat4jSolver

public Sat4jSolver()

Creates a new solver with default parameters (maxvar=1000000, nbclauses=500000).

Method Details

isSatisfiable

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

Description copied from class: DimacsSatSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class DimacsSatSolver

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.

getWitness

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

Description copied from class: DimacsSatSolver

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

Specified by:

getWitness in class DimacsSatSolver

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.

isInstalled

public boolean isInstalled()

Description copied from class: SatSolver

Return whether the solve ris installed

Specified by:

isInstalled in class DimacsSatSolver

Returns:

whether the solve ris installed