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(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)	If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
boolean	isSatisfiable(Collection<PlFormula> formulas)	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.SatSolver

convertToDimacs, convertToDimacs, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder

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)

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 interface ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

Specified by:

getWitness in class SatSolver

Parameters:

formulas - a set of formulas

Returns:

some model of the formulas or null.

isSatisfiable

public boolean isSatisfiable(Collection<PlFormula> formulas)

Description copied from class: SatSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class SatSolver

Parameters:

formulas - a set of formulas.

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