org.kahina.logic.sat.insertionmus.algorithms

Class BasicAlgorithm

java.lang.Object

org.kahina.logic.sat.insertionmus.algorithms.AbstractAlgorithm

org.kahina.logic.sat.insertionmus.algorithms.BasicAlgorithm

public class BasicAlgorithm
extends AbstractAlgorithm

Implementation of the insertion algorithm of J.K. de Siqueira N. and J.-F. Puget "Explanation-based generalisation of failures"

Author:

Seitz

Field Summary

Fields

Modifier and Type	Field and Description
protected boolean	finished

Constructor Summary

Constructors

Constructor and Description
BasicAlgorithm()

Method Summary

Methods

Modifier and Type	Method and Description
CnfSatInstance	findAMuse(AlgorithmData data)
boolean	isFinished() is the MUS calculated?
static void	main(java.lang.String[] arg0) Simple testfunction for this algorithm.
boolean	nextStep(int clauseIndex, AlgorithmData data)
boolean	selectNext(int clauseID, AlgorithmData data) runs the next step of this algorithm precondition: this.instance.getSize() > 0

Methods inherited from class org.kahina.logic.sat.insertionmus.algorithms.AbstractAlgorithm

nextStep, solve, solve, solve

Methods inherited from class java.lang.Object

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

Field Detail

finished

protected boolean finished

Constructor Detail

BasicAlgorithm

public BasicAlgorithm()

Method Detail

isFinished

public boolean isFinished()

is the MUS calculated?

Returns:

true if there is a MUS calculated

selectNext

public boolean selectNext(int clauseID,
                 AlgorithmData data)
                   throws java.util.concurrent.TimeoutException,
                          java.io.IOException

runs the next step of this algorithm precondition: this.instance.getSize() > 0

Parameters:

clauseIndex - the index of the clause that should be handled next.

Returns:

true if an MUS is found.

Throws:

java.io.IOException

java.lang.InterruptedException

java.util.concurrent.TimeoutException

main

public static void main(java.lang.String[] arg0)
                 throws java.util.concurrent.TimeoutException,
                        java.lang.InterruptedException,
                        java.io.IOException

Simple testfunction for this algorithm.

Throws:

java.io.IOException

java.lang.InterruptedException

java.util.concurrent.TimeoutException

findAMuse

public CnfSatInstance findAMuse(AlgorithmData data)

Overrides:

findAMuse in class AbstractAlgorithm

nextStep

public boolean nextStep(int clauseIndex,
               AlgorithmData data)

Specified by:

nextStep in class AbstractAlgorithm

Returns:

true if a new Step is reached.