argutia.logic.resolution
Class Resolution

java.lang.Object
  extended by argutia.logic.resolution.Resolution
public class Resolution
extends Object
Nested Class Summary
static class Resolution.Etat
          Un contexte est SATISFIABLE lorsqu'une affectation des littéraux des clauses a été trouvée, INSATISFIABLE sinon.
static class Resolution.EtatApresSimplification
           
 
Field Summary
protected LinkedList<Maillon> affectations
           
protected Contexte contexte
           
protected int resolutionEnclenchee
           
 
Constructor Summary
Resolution()
           
 
Method Summary
protected void addAffectation(MaillonLitteral mL)
           
 void backtrack(int pointDeBacktrack)
          Rétablit le contexte associé au point de restauration passé en paramètre : O(n*m).
protected MaillonLitteral getNextMLInconnu()
           
 int getPointDeBacktrack()
          Fournit un point de restauration permettant via un appel à la méthode backtrack(int) de retrouver le contexte présent : O(1).
 void injecterClause(Clause c)
          On suppose qu'on injecte des clauses uniquement avant un appel à resoudre().
 void injecterEnsembleDeFormules(SetOfFormulas e)
           
 void injecterFormule(Formula f)
           
 void memoriser()
           
protected void removeAffectation()
           
 Resolution.Etat resoudre()
          Davis et Putnam
 Resolution.EtatApresSimplification simplifier()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Field Detail

affectations

protected final LinkedList<Maillon> affectations

contexte

protected Contexte contexte

resolutionEnclenchee

protected int resolutionEnclenchee
Constructor Detail

Resolution

public Resolution()
Method Detail

addAffectation

protected void addAffectation(MaillonLitteral mL)

backtrack

public void backtrack(int pointDeBacktrack)
Rétablit le contexte associé au point de restauration passé en paramètre : O(n*m).
Complexité =
où n est le nombre de .

Parameters:
pointDeBacktrack - point de restauration obtenu via la méthode getPointDeBacktrack()

getNextMLInconnu

protected MaillonLitteral getNextMLInconnu()
Returns:
un maillon littéral à l'état INCONNU, ou null s'il n'y en a plus

getPointDeBacktrack

public int getPointDeBacktrack()
Fournit un point de restauration permettant via un appel à la méthode backtrack(int) de retrouver le contexte présent : O(1).

See Also:
backtrack(int)
Returns:
un point de restauration sous forme d'entier

injecterClause

public void injecterClause(Clause c)
                    throws IllegalStateException
On suppose qu'on injecte des clauses uniquement avant un appel à resoudre(). Sinon une exception ResolutionException est levée.

Parameters:
c - Clause à injecter
Throws:
IllegalStateException - si on tente d'injecter une clause après un appel à resoudre().

injecterEnsembleDeFormules

public void injecterEnsembleDeFormules(SetOfFormulas e)
                                throws IllegalStateException
Throws:
IllegalStateException

injecterFormule

public void injecterFormule(Formula f)
                     throws IllegalStateException
Throws:
IllegalStateException

removeAffectation

protected void removeAffectation()

resoudre

public Resolution.Etat resoudre()
Davis et Putnam

Returns:
l'état de l'ensemble de clauses après résolution

simplifier

public Resolution.EtatApresSimplification simplifier()

memoriser

public void memoriser()
Argutia JavaDoc
23 décembre 2007