Package net.sf.tweety.logics.pl.sat
Class Sat4jSolver
- java.lang.Object
-
- net.sf.tweety.logics.pl.sat.SatSolver
-
- net.sf.tweety.logics.pl.sat.Sat4jSolver
-
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,?>>
,ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
public class Sat4jSolver extends SatSolver
Uses the Sat4j library for SAT solving (note that currently only the light version is used).- Author:
- Matthias Thimm
-
-
Field Summary
Fields Modifier and Type Field Description private int
maxvar
Max number of variables for this solver.private static int
MAXVAR
Default value for max number of variables for asolver.private int
nbclauses
Max number of expected clauses for this solver.private static int
NBCLAUSES
Default value for max number of expected clauses for a solver.
-
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(java.util.Collection<PlFormula> formulas)
If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.boolean
isSatisfiable(java.util.Collection<PlFormula> formulas)
Checks whether the given set of formulas is satisfiable.-
Methods inherited from class net.sf.tweety.logics.pl.sat.SatSolver
convertToDimacs, convertToDimacs, createTmpDimacsFile, createTmpDimacsFile, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder
-
-
-
-
Field Detail
-
MAXVAR
private static final int MAXVAR
Default value for max number of variables for asolver.- See Also:
- Constant Field Values
-
NBCLAUSES
private static final int NBCLAUSES
Default value for max number of expected clauses for a solver.- See Also:
- Constant Field Values
-
maxvar
private int maxvar
Max number of variables for this solver.
-
nbclauses
private int nbclauses
Max number of expected clauses for this solver.
-
-
Constructor Detail
-
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 Detail
-
isSatisfiable
public boolean isSatisfiable(java.util.Collection<PlFormula> formulas)
Description copied from class:SatSolver
Checks whether the given set of formulas is satisfiable.- Specified by:
isSatisfiable
in classSatSolver
- Parameters:
formulas
- a set of formulas.- Returns:
- "true" if the set is consistent.
-
getWitness
public Interpretation<PlBeliefSet,PlFormula> getWitness(java.util.Collection<PlFormula> formulas)
Description copied from class:SatSolver
If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.- Specified by:
getWitness
in interfaceConsistencyWitnessProvider<PlBeliefSet,PlFormula>
- Specified by:
getWitness
in classSatSolver
- Parameters:
formulas
- a set of formulas- Returns:
- some model of the formulas or null.
-
-