Class Msat

java.lang.Object
  Msat

public class Msat
extends java.lang.Object

Constructor Summary

Msat(int numProcessors)
Constructor for Msat

Msat(int numProcessors, java.lang.String filename)
Constructor for Msat

Method Summary

Formula	getFormula() Returns the formula
SubProblem	getSubProblem() Returns the next subproblem that needs to be solved if one exists and removes the subproblem from the list of subproblems that needs solving
void	setFormula(Formula formula) Sets the formula
void	setNumSubProb(int n) Sets the number of subproblems
void	solve() Calls the split method to split the formula and then starts the solvers
java.util.HashSet<SubProblem>	split(Formula f) Splits a complete problem into numSubProb subproblems
void	workCompleted(Solver solver) When a solver is completed solving a subproblem, it removes the subproblem from the list of subproblems that are in progress, prints out that the thread has completed its task and also the outcome of the threads task (whether a satisfying assignment was found).

Methods inherited from class java.lang.Object

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

Constructor Detail

Msat

public Msat(int numProcessors)

Constructor for Msat

Parameters:

numProcessors - the number of processors

Msat

public Msat(int numProcessors,
            java.lang.String filename)
     throws java.io.FileNotFoundException

Constructor for Msat

Parameters:

numProcessors - the number of processors

filename - the file that contains the formula

Throws:

java.io.FileNotFoundException

Method Detail

setFormula

public void setFormula(Formula formula)

Sets the formula

Parameters:

formula - the formula

getFormula

public Formula 
getFormula()

Returns the formula

Returns:

formula

setNumSubProb

public void setNumSubProb(int n)

Sets the number of subproblems

Parameters:

n - the number of subproblems

workCompleted

public void workCompleted(Solver solver)

When a solver is completed solving a subproblem, it removes the subproblem from the list of subproblems that are in progress, prints out that the thread has completed its task and also the outcome of the threads task (whether a satisfying assignment was found). *

Parameters:

solver - the current solver that has completed its task

solve

public void solve()

Calls the split method to split the formula and then starts the solvers

getSubProblem

public SubProblem getSubProblem()

Returns the next subproblem that needs to be solved if one exists and removes the subproblem from the list of subproblems that needs solving

Returns:

Subproblem subproblem in the form of a partial assignment that needs to be solved

split

public java.util.HashSet<SubProblem> split(Formula f)

Splits a complete problem into numSubProb subproblems

Parameters:

f - the formula that needs to be split

Returns:

a set of subproblems that need solving