Package org.tweetyproject.logics.pl.sat
Class CmdLineSatSolver
- java.lang.Object
-
- org.tweetyproject.logics.pl.sat.SatSolver
-
- org.tweetyproject.logics.pl.sat.CmdLineSatSolver
-
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,?>>
,ConsistencyWitnessProvider<PlBeliefSet,PlFormula>
public class CmdLineSatSolver extends SatSolver
This class offers a generic wrapper for command line based SAT solvers. It is likely to work for most solvers that use the Dimacs format, e.g. most solvers presented at SAT solver competitions. Tested with the following solvers:- CaDiCal 1.3.1 http://fmv.jku.at/cadical
- Kissat 1.0.3 http://fmv.jku.at/kissat
- Lingeling bcp href="http://fmv.jku.at/lingeling
- Slime 3.1.1 https://github.com/maxtuno/slime-sat-solver
- Author:
- Anna Gessler
-
-
Constructor Summary
Constructors Constructor Description CmdLineSatSolver(java.lang.String binaryLocation)
Creates a new SAT solver based on the given binary location.
-
Method Summary
Modifier and Type Method Description void
addOption(java.lang.String option)
Adds a single command line parameter.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.void
setOptions(java.lang.String options)
Sets the options parameter of the sat solver.-
Methods inherited from class org.tweetyproject.logics.pl.sat.SatSolver
convertToDimacs, convertToDimacs, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder
-
-
-
-
Method Detail
-
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.
-
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.
-
addOption
public void addOption(java.lang.String option)
Adds a single command line parameter. Needs to be in the correct format, usually in the form "--opt". Note: Available options can be found in the manuals of the respective solvers.- Parameters:
option
- string
-
setOptions
public void setOptions(java.lang.String options)
Sets the options parameter of the sat solver. Needs to be in the correct format, usually in the form "--opt1 --opt2", with spaces between different options. This replaces the whole options string, replacing any previously added parameters or default parameters. Note: Available options can be found in the manuals of the respective solvers.- Parameters:
options
- string of options
-
-