edu.kit.iti.formal.lights.sat

Class SATSolver

java.lang.Object

edu.kit.iti.formal.lights.sat.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

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.

Author:

Mattias Ulbrich, David Farago

See Also:

Clause

Constructor Summary

Constructors

Constructor and Description
SATSolver()

Method Summary

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.
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

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

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(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 org.sat4j.specs.TimeoutException

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:

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

org.sat4j.specs.TimeoutException