edu.kit.iti.lfm.spotlight

Class SATSolver

java.lang.Object

edu.kit.iti.lfm.spotlight.SATSolver

public class SATSolver
extends Object

The class SATSolver provides an interface to a satisfiability solver.

Internally, the class Clause is used to store clauses.

Prototypical usage

 SATSolver solver = new SATSolver();
 
 // adding DIMACS clauses
 solver.addClause(42, -23, 7);
 // ...
 
 // trigger invocation of the underlying solver
 int[] result = solver.solve();
 

Configuration

By default, the framework sat4j is used as solver. Sat4j is a java library for solving boolean satisfaction and optimization problems. It is native Java and can, hence, be well integrated. However, it is slower than native implementations. This framework supports also MiniSat. You need to configure it however.

You can choose the SAT solver to be used by configuring the solver:

System property	Static variable	Description	Default
spotlight.minisat	USE_MINISAT	switch between SAT4J and MiniSat	false
spotlight.minisat.keep	MINISAT_KEEP	for debug: keep the input/output files from minisat. Their location is printed to the terminal.	false
spotlight.minisat.executable	MINISAT_EXECUTABLE	If the MiniSat executable is not your search path for executables, you can specify its absolute location here	"minisat"

Author:

Mattias Ulbrich, David Farago

See Also:

Clause

Field Summary

Fields

Modifier and Type	Field and Description
static String	MINISAT_EXECUTABLE If the MiniSat executable is not your search path for executables, you can specify its absolute location here.
static boolean	MINISAT_KEEP for debug: keep the input/output files from minisat.
static boolean	USE_MINISAT switch between sat4j and minisat.

Constructor Summary

Constructors

Constructor and Description
SATSolver()

Method Summary

Methods

Modifier and Type	Method and Description
void	addClause(Clause clause) Add a single clause to the solver.
void	addClause(int... literals) Add a single clause to the solver.
void	addClause(int[] array, int start, int len) Add a single clause constructed from a part of an array to the solver.
List<Clause>	getClauses() Get the list of all clauses added to the solver.
int	getMaximumVariable() Get the highest variable index amongst all clauses in the solver.
int[]	solve() Invoke the SAT solver and return a satisfying variable assignment if one has been found.

Methods inherited from class java.lang.Object

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

Field Detail

USE_MINISAT

public static final boolean USE_MINISAT

switch between sat4j and minisat. true means minisat, false means sat4j.

MINISAT_KEEP

public static final boolean MINISAT_KEEP

for debug: keep the input/output files from minisat. Their location is printed to the terminal if set to true

MINISAT_EXECUTABLE

public static final String MINISAT_EXECUTABLE

If the MiniSat executable is not your search path for executables, you can specify its absolute location here.

Constructor Detail

SATSolver

public SATSolver()

Method Detail

addClause

public void addClause(int... literals)

Add a single clause to the solver.

The list of arguments is treated as a single clause and added to solver.

Parameters:

literals - a list of zero or more literal values.

Throws:

IllegalArgumentException - if a literal is 0.

addClause

public void addClause(int[] array,
             int start,
             int len)

Add a single clause constructed from a part of an array to the solver.

The system constructs a clause from the argument array beginning at index start, taking len many values.

Parameters:

array - the non-null array to take the literals from

start - the first index in array to take literals from

len - the number of literals to take from the array

Throws:

IndexOutOfBoundsException - if start is outside the array index range or if start+len is outside.

IllegalArgumentException - if 0 is contained in the array or if len < 0.

NullPointerException - if array is null

addClause

public void addClause(Clause clause)

Add a single clause to the solver.

Parameters:

clause - a non-null reference to a clause.

Throws:

NullPointerException - if the argument is null.

getClauses

public List<Clause> getClauses()

Get the list of all clauses added to the solver.

The returned reference cannot be modified but keeps track of changes to the solver.

Returns:

an unmodifiable view to the list of clauses.

getMaximumVariable

public int getMaximumVariable()

Get the highest variable index amongst all clauses in the solver.

For example, the empty solver would return 0. After adding the clause {-1,5} it would return 5. After adding {-7,6} it returns 7.

Returns:

a non-negative integer. 0 only there are no clauses (or only empty clauses)

solve

public int[] solve()
            throws SpotlightException

Invoke the SAT solver and return a satisfying variable assignment if one has been found.

The clauses remain in the solver and will be sent again if this method is invoked a second time.

If set of clauses has no satisfying assignment (UNSAT), null is returned. Otherwise a variable assignment is returned. This array contains literals for the variables between 1 and getMaximumVariable(). Every variable appears either positive or negative. The clause set is satisfied if variable with positive occurrence are set to true and the others to false.

MiniSat and sat4j are supported. See the top of the page on how to change the used sat solver.

Returns:

either null or a list of integers different from 0.

Throws:

SpotlightException - if any exception was raised during the satsolving process.