kodkod.engine.satlab
Class MiniSat

java.lang.Object
  kodkod.engine.satlab.MiniSat

All Implemented Interfaces:

OrderableSolver, kodkod.engine.satlab.SATSolver

final class MiniSat
extends java.lang.Object
implements OrderableSolver

Java wrapper for the MiniSat solver by Niklas Eén and Niklas Sörensson.

Author:

Emina Torlak

Field Summary

protected long

peer The memory address of the native instance wrapped by this wrapper.

Constructor Summary

MiniSat()
Constructs a new MiniSAT wrapper.

Method Summary

boolean	addClause(int[] lits) Ensures that this solver logically contains the given clause, and returns true if this.clauses changed as a result of the call.
(package private) boolean	addClause(long peer, int[] lits) Ensures that the given native peer logically contains the specified clause and returns true if the solver's clause database changed as a result of the call.
void	addVariables(int numVars) Adds the specified number of new variables to the solver's vocabulary.
(package private) void	addVariables(long peer, int numVariables) Adds the specified number of variables to the given native peer.
(package private) void	adjustClauseCount(int clauseCount) Adjusts the internal clause count so that the next call to numberOfClauses() will return the given value.
protected void	finalize() Releases the resources used by this native solver.
void	free() Frees the memory used by this solver.
(package private) void	free(long peer) Releases the resources associated with the native solver at the given memory address.
(package private) boolean	initializeActivity(long peer, int var, double priority) Initialize MiniSAT's internal score used to order variables (highest first)
void	initializeOrder(int var, double order) Initializes MiniSAT's internal ordering for the specified variable
(package private) static void	loadLibrary(java.lang.Class<? extends kodkod.engine.satlab.NativeSolver> library) Loads the JNI library for the given class.
int	numberOfClauses() Returns the number of clauses in this solver.
int	numberOfVariables() Returns the size of this solver's vocabulary.
(package private) boolean	overrideActivity(long peer, int var, int priority) Statically override MiniSAT's internal score by external priorities (highest first)
void	overrideOrder(int var, int order) Overrides MiniSAT's internal ordering for the specified variable
(package private) long	peer() Returns a pointer to the C++ peer class (the native instance wrapped by this object).
boolean	solve() Returns true if there is a satisfying assignment for this.clauses.
(package private) boolean	solve(long peer) Calls the solve method on the given native peer.
(package private) java.lang.Boolean	status() Returns the current sat of the solver.
java.lang.String	toString()
(package private) void	validateVariable(int variable) Throws an IllegalArgumentException if variable !
boolean	valueOf(int variable) Returns the boolean value assigned to the given variable by the last successful call to SATSolver.solve().
(package private) boolean	valueOf(long peer, int literal) Returns the assignment for the given literal by the specified native peer

Methods inherited from class java.lang.Object

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

Field Detail

peer

protected long peer

The memory address of the native instance wrapped by this wrapper.

Constructor Detail

MiniSat

public MiniSat()

Constructs a new MiniSAT wrapper.

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

See Also:

Object.toString()

free

void free(long peer)

Releases the resources associated with the native solver at the given memory address. This method must be called when the object holding the given reference goes out of scope to avoid memory leaks.

See Also:

NativeSolver.free(long)

addVariables

void addVariables(long peer,
                  int numVariables)

Adds the specified number of variables to the given native peer.

See Also:

NativeSolver.addVariables(long, int)

addClause

boolean addClause(long peer,
                  int[] lits)

Ensures that the given native peer logically contains the specified clause and returns true if the solver's clause database changed as a result of the call.

Returns:

true if the peer's clause database changed as a result of the call; a negative integer if not.

See Also:

NativeSolver.addClause(long, int[])

solve

boolean solve(long peer)

Calls the solve method on the given native peer.

Returns:

true if the clauses in the solver are SAT; otherwise returns false.

See Also:

NativeSolver.solve(long)

valueOf

boolean valueOf(long peer,
                int literal)

Returns the assignment for the given literal by the specified native peer

Returns:

the assignment for the given literal

See Also:

NativeSolver.valueOf(long, int)

initializeOrder

public void initializeOrder(int var,
                            double order)

Initializes MiniSAT's internal ordering for the specified variable

Specified by:

initializeOrder in interface OrderableSolver

overrideOrder

public void overrideOrder(int var,
                          int order)

Overrides MiniSAT's internal ordering for the specified variable

Specified by:

overrideOrder in interface OrderableSolver

initializeActivity

boolean initializeActivity(long peer,
                           int var,
                           double priority)

Initialize MiniSAT's internal score used to order variables (highest first)

overrideActivity

boolean overrideActivity(long peer,
                         int var,
                         int priority)

Statically override MiniSAT's internal score by external priorities (highest first)

loadLibrary

static void loadLibrary(java.lang.Class<? extends kodkod.engine.satlab.NativeSolver> library)

Loads the JNI library for the given class. It first attempts to load the library named library.getSimpleName().toLowerCase(). If that fails, it attempts to load library.getSimpleName().toLowerCase()+suffix where suffix ranges over the path-separator delimited list obtained by calling System.getProperty("kodkod." + library.getSimpleName().toLowerCase()).

numberOfVariables

public final int numberOfVariables()

Returns the size of this solver's vocabulary.

Specified by:

numberOfVariables in interface kodkod.engine.satlab.SATSolver

Returns:

#this.variables

See Also:

SATSolver.numberOfVariables()

numberOfClauses

public final int numberOfClauses()

Returns the number of clauses in this solver.

Specified by:

numberOfClauses in interface kodkod.engine.satlab.SATSolver

Returns:

#this.clauses

See Also:

SATSolver.numberOfClauses()

adjustClauseCount

void adjustClauseCount(int clauseCount)

Adjusts the internal clause count so that the next call to numberOfClauses() will return the given value.

addVariables

public void addVariables(int numVars)

Adds the specified number of new variables to the solver's vocabulary. The behavior of this method is undefined if it is called after this.solve() has returned false.

Specified by:

addVariables in interface kodkod.engine.satlab.SATSolver

See Also:

SATSolver.addVariables(int), addVariables(long, int)

addClause

public final boolean addClause(int[] lits)

Ensures that this solver logically contains the given clause, and returns true if this.clauses changed as a result of the call. No reference to the specified array is kept, so it can be reused. The contents of the array may, however, be modified. It is the client's responsibility to ensure that no literals in the given array are repeated, or that both a literal and its negation are present. The behavior of this method is undefined if it is called after this.solve() has returned false.

Specified by:

addClause in interface kodkod.engine.satlab.SATSolver

Returns:

#this.clauses' > #this.clauses

See Also:

SATSolver.addClause(int[]), addClause(long, int[])

peer

final long peer()

Returns a pointer to the C++ peer class (the native instance wrapped by this object).

Returns:

a pointer to the C++ peer class (the native instance wrapped by this object).

status

final java.lang.Boolean status()

Returns the current sat of the solver.

Returns:

null if the sat is unknown, TRUE if the last call to solve() yielded SAT, and FALSE if the last call to solve() yielded UNSAT.

solve

public final boolean solve()

Returns true if there is a satisfying assignment for this.clauses. Otherwise returns false. If this.clauses are satisfiable, the satisfying assignment for a given variable can be obtained by calling SATSolver.valueOf(int). If the satisfiability of this.clauses cannot be determined within the given number of seconds, a TimeoutException is thrown.

Specified by:

solve in interface kodkod.engine.satlab.SATSolver

Returns:

true if this.clauses are satisfiable; otherwise false.

See Also:

SATSolver.solve(), solve(long)

validateVariable

final void validateVariable(int variable)

Throws an IllegalArgumentException if variable !in this.variables. Otherwise does nothing.

Throws:

java.lang.IllegalArgumentException - variable !in this.variables

valueOf

public final boolean valueOf(int variable)

Returns the boolean value assigned to the given variable by the last successful call to SATSolver.solve().

Specified by:

valueOf in interface kodkod.engine.satlab.SATSolver

Returns:

the boolean value assigned to the given variable by the last successful call to SATSolver.solve().

See Also:

SATSolver.valueOf(int)

free

public final void free()

Frees the memory used by this solver. Once free() is called, all subsequent calls to methods other than free() may fail.

Specified by:

free in interface kodkod.engine.satlab.SATSolver

See Also:

SATSolver.free()

finalize

protected final void finalize()
                       throws java.lang.Throwable

Releases the resources used by this native solver.

Overrides:

finalize in class java.lang.Object

Throws:

java.lang.Throwable