Package org.tweetyproject.sat.lingeling

Class LingelingSatSolver

java.lang.Object

org.tweetyproject.sat.lingeling.LingelingSatSolver

All Implemented Interfaces:

AutoCloseable, SatSolver

public final class LingelingSatSolver
extends Object
implements SatSolver

This class provides an implementation of the `SatSolver` interface using the Lingeling SAT solver. The Lingeling SAT solver is a state-of-the-art solver for boolean satisfiability problems.

This class handles the interaction with the native Lingeling solver via bindings, allowing for the creation of variables, addition of clauses, and checking satisfiability under assumptions.

Author: [Your Name]

Constructor Summary

Constructors

Constructor	Description
LingelingSatSolver()	Initializes a new instance of the Lingeling SAT solver.

Method Summary

Modifier and Type	Method	Description
void	add(int[] clause)	Adds a clause to the current formula in the Lingeling solver.
void	close()	Releases resources associated with the Lingeling solver instance.
int	newVar()	Creates and returns a new variable in the Lingeling solver.
boolean	satisfiable(int[] assumptions)	Checks if the current formula is satisfiable under the given assumptions.
boolean[]	witness(int[] literals, int[] assumptions)	Returns a witness (truth assignment) for the given literals under the given 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()

Initializes a new instance of the Lingeling SAT solver.

This constructor initializes the Lingeling solver instance by calling the native `init` method through the `Binding` class. The handle to the Lingeling instance is stored in the `handle` field.

Method Details

satisfiable

public boolean satisfiable(int[] assumptions)

Checks if the current formula is satisfiable under the given assumptions.

Specified by:

satisfiable in interface SatSolver

Parameters:

assumptions - an array of literals that are assumed to be true

Returns:

`true` if the formula is satisfiable under the given assumptions, `false` otherwise

witness

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

Returns a witness (truth assignment) for the given literals under the given assumptions.

This method checks if the formula is satisfiable under the given assumptions, and if it is, returns a witness that represents the truth values of the specified literals.

Specified by:

witness in interface SatSolver

Parameters:

literals - an array of literals for which the truth assignment is requested

assumptions - an array of literals that are assumed to be true

Returns:

a boolean array representing the truth assignment of the given literals, or an empty array if unsatisfiable

add

public void add(int[] clause)

Adds a clause to the current formula in the Lingeling solver.

Specified by:

add in interface SatSolver

Parameters:

clause - an array of literals that form the clause

newVar

public int newVar()

Creates and returns a new variable in the Lingeling solver.

This method increments the internal variable counter and returns the new variable index. This ensures that each variable created by the solver is unique.

Specified by:

newVar in interface SatSolver

Returns:

the index of the newly created variable

close

public void close()

Releases resources associated with the Lingeling solver instance.

This method calls the native `release` method to free the resources held by the Lingeling instance associated with the `handle`.

Specified by:

close in interface AutoCloseable

Specified by:

close in interface SatSolver