net.sf.javailp.minisat
Class MiniSat

java.lang.Object
  net.sf.javailp.minisat.MiniSat

public class MiniSat
extends Object

The MiniSat is the JNI class for the MiniSat+ solver.

The variables are integers starting from 0. A positive literal of the variable x is x+1, the negative literal is -(x+1).

See Also:

http://minisat.se/MiniSat+.html

Constructor Summary

MiniSat()
Construct a MiniSat instance.

Method Summary

boolean	addConstraint(int[] coeffs, int[] lits, String comp, int rhs) Adds a linear constraint.
boolean	okay() Returns true if no contradiction appeared so far.
void	reset() Resets the decision heuristic, i.e., the phases and activities of the variables.
void	setDecay(double value) Set the decay value
void	setInc(double value) Set the inc value
void	setObjective(int[] coeffs, int[] lits) Set the objective of the problem.
void	setVar(int var, boolean phase, double activity) Sets the initial phase and activity for a specified variable-
void	setVerbose(int level) Set the verbosity level (0=no output,1,2=most output).
void	solve() Solve the problem.
boolean	solveSingle() Solve the problem without optimizing.
String	toString()
boolean	valueOf(int var) Returns the value of the result of a specified variable.

Methods inherited from class java.lang.Object

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

Constructor Detail

MiniSat

public MiniSat()

Construct a MiniSat instance.

Method Detail

setObjective

public void setObjective(int[] coeffs,
                         int[] lits)

Set the objective of the problem. By default the objective is minimized. If you want the objective to be maximized negate the coefficients.

Parameters:

coeffs - the coefficients

lits - the literals

addConstraint

public boolean addConstraint(int[] coeffs,
                             int[] lits,
                             String comp,
                             int rhs)

Adds a linear constraint.

Parameters:

coeffs - the coefficients

lits - the literals

comp - the comparator ("<=","=",">=")

rhs - the right hand side value

Returns:

true if this constraint did not cause a contradiction

solve

public void solve()

Solve the problem.

solveSingle

public boolean solveSingle()

Solve the problem without optimizing.

Returns:

true if a feasible solution is found

valueOf

public boolean valueOf(int var)

Returns the value of the result of a specified variable. The method should be called after MiniSat#solve() or MiniSat#solveSingle().

Parameters:

var - the variable

Returns:

the boolean result value

setVar

public void setVar(int var,
                   boolean phase,
                   double activity)

Sets the initial phase and activity for a specified variable-

Parameters:

var - the variable

phase - the phase

activity - the activity

reset

public void reset()

Resets the decision heuristic, i.e., the phases and activities of the variables.

setInc

public void setInc(double value)

Set the inc value

Parameters:

value - the inc value to be set

setDecay

public void setDecay(double value)

Set the decay value

Parameters:

value - the decay value to be set

setVerbose

public void setVerbose(int level)

Set the verbosity level (0=no output,1,2=most output).

Parameters:

level - the level to be set

okay

public boolean okay()

Returns true if no contradiction appeared so far.

Returns:

true if no contradiction appeared so far

toString

public String toString()

Overrides:

toString in class Object