LingelingSatSolver

java.lang.Object

org.tweetyproject.sat.lingeling.LingelingSatSolver

All Implemented Interfaces:: AutoCloseable, SatSolver

public final class LingelingSatSolver extends Object implements SatSolver

Constructor Summary

Constructors

Constructor

Description

LingelingSatSolver()
Method Summary

Modifier and Type

Method

Description

void

add(int[] clause)

Adds the given clause to the SAT solver state.

void

close()

int

newVar()

Creates and returns the integer representation of a fresh propositional variable.

boolean

satisfiable(int[] assumptions)

boolean[]

witness(int[] literals, int[] assumptions)

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.tweetyproject.sat.SatSolver
satisfiable, witness

Constructor Details
- LingelingSatSolver
  
  public LingelingSatSolver()
Method Details
- satisfiable
  
  public boolean satisfiable(int[] assumptions)
  
  Specified by:
  
  satisfiable in interface SatSolver
- witness
  
  public boolean[] witness(int[] literals, int[] assumptions)
  
  Specified by:
  
  witness in interface SatSolver
- add
  
  public void add(int[] clause)
  
  Description copied from interface: SatSolver
  
  Adds the given clause to the SAT solver state.
  Note that contrary to DIMACS format, a trailing '0' is not required!
  
  Specified by:
  
  add in interface SatSolver
  
  Parameters:
  
  clause - the clause to add
- newVar
  
  public int newVar()
  
  Description copied from interface: SatSolver
  
  Creates and returns the integer representation of a fresh propositional variable.
  It is necessary to only use variables returned by this method, since some solvers require to first allocate and maintain a data structure of the variables before they can be used in clauses. Hence, using integers not returned by this method may work for some solvers, but not for others.
  
  Specified by:
  
  newVar in interface SatSolver
  
  Returns:
- close
  
  public void close()
  
  Specified by:
  
  close in interface AutoCloseable
  
  Specified by:
  
  close in interface SatSolver