kodkod.engine.satlab

Interface SATSolver

All Known Subinterfaces:

SATProver

public interface SATSolver

Provides an interface to a SAT solver.

Author:

Emina Torlak

Specfields:

variables: set [1..)

clauses: set Clause

Invariants:

all i: [2..) | i in variables => i-1 in variables

all c: clauses | all lit: c.literals | lit in variables || -lit in variables

all c: clauses | all disj i,j: c.literals | abs(i) != abs(j)

Method Summary

Modifier and Type	Method and Description
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.
void	addVariables(int numVars) Adds the specified number of new variables to the solver's vocabulary.
void	free() Frees the memory used by this solver.
int	numberOfClauses() Returns the number of clauses in this solver.
int	numberOfVariables() Returns the size of this solver's vocabulary.
boolean	solve() Returns true if there is a satisfying assignment for this.clauses.
boolean	valueOf(int variable) Returns the boolean value assigned to the given variable by the last successful call to solve().

Method Detail

addClause

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.

Requires:

all i: [0..lits.length) | abs(lits[i]) in this.variables

all disj i,j: [0..lits.length) | abs(lits[i]) != abs(lits[j])

Ensures:

[[this.clauses']] = ([[this.clauses]] and [[lits]])

Returns:

#this.clauses' > #this.clauses

Throws:

NullPointerException - lits = null

addVariables

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.

Requires:

numVars >= 0

Ensures:

this.variables' = [1..#this.variables + numVars]

Throws:

IllegalArgumentException - numVars < 0

free

void free()

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

Ensures:

frees the memory used by this solver

numberOfClauses

int numberOfClauses()

Returns the number of clauses in this solver.

Returns:

#this.clauses

numberOfVariables

int numberOfVariables()

Returns the size of this solver's vocabulary.

Returns:

#this.variables

solve

boolean solve()
       throws SATAbortedException

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 valueOf(int). If the satisfiability of this.clauses cannot be determined within the given number of seconds, a TimeoutException is thrown.

Returns:

true if this.clauses are satisfiable; otherwise false.

Throws:

SATAbortedException - - the call to solve was cancelled or could not terminate normally.

valueOf

boolean valueOf(int variable)

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

Requires:

solve() has been called and the outcome of the last call was true.

Returns:

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

Throws:

IllegalArgumentException - variable !in this.variables

IllegalStateException - solve() has not been called or the outcome of the last call was not true.