Sat4jSolver

java.lang.Object

org.tweetyproject.logics.pl.sat.SatSolver

org.tweetyproject.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

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

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