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<PropositionalFormula>, ConsistencyTester<BeliefSet<PropositionalFormula>>, ConsistencyWitnessProvider<PropositionalFormula>

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 and 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 and 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 and Description
Interpretation	getWitness(java.util.Collection<PropositionalFormula> 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<PropositionalFormula> 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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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<PropositionalFormula> 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.

getWitness

public Interpretation getWitness(java.util.Collection<PropositionalFormula> 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<PropositionalFormula>

Specified by:

getWitness in class SatSolver

Returns:

some model of the formulas or null.