Package org.tweetyproject.logics.pl.sat

Class CmdLineSatSolver

java.lang.Object

org.tweetyproject.logics.pl.sat.SatSolver

org.tweetyproject.logics.pl.sat.DimacsSatSolver

org.tweetyproject.logics.pl.sat.CmdLineSatSolver

All Implemented Interfaces:

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

public class CmdLineSatSolver
extends DimacsSatSolver

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(String binaryLocation)	Creates a new SAT solver based on the given binary location.

Method Summary

Modifier and Type	Method	Description
void	addOption(String option)	Adds a single command line parameter.
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.
void	setOptions(String options)	Sets the options parameter of the sat solver.

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

CmdLineSatSolver

public CmdLineSatSolver(String binaryLocation)

Creates a new SAT solver based on the given binary location.

Parameters:

binaryLocation - the location of the binary

Method Details

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.

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.

addOption

public void addOption(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(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

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