Package org.tweetyproject.logics.pl.sat

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, String additional_clauses, int num_additional_clauses)	If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
boolean	isInstalled()
boolean	isSatisfiable(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, String additional_clauses, int num_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,
 String additional_clauses,
 int num_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!)

num_additional_clauses - the number of additional_clauses

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,
 String additional_clauses,
 int num_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!)

num_additional_clauses - the number of additional_clauses

Returns:

some model of the formulas or null.

isInstalled

public boolean isInstalled()

Specified by:

isInstalled in class DimacsSatSolver

Returns:

whether the solve ris installed