org.sat4j.minisat.constraints.cnf
Class HTClause

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.HTClause
All Implemented Interfaces:
java.io.Serializable, Constr, Propagatable, IConstr
Direct Known Subclasses:
LearntHTClause, OriginalHTClause

public abstract class HTClause
extends java.lang.Object
implements Constr, java.io.Serializable

Lazy data structure for clause using the Head Tail data structure from SATO, The original scheme is improved by avoiding moving pointers to literals but moving the literals themselves. We suppose here that the clause contains at least 3 literals. Use the BinaryClause or UnaryClause clause data structures to deal with binary and unit clauses.

Author:
leberre
See Also:
BinaryClause, UnitClause, Serialized Form

Field Summary
protected  int head
           
protected  int[] middleLits
           
protected  int tail
           
protected  ILits voc
           
 
Constructor Summary
HTClause(IVecInt ps, ILits voc)
          Creates a new basic clause
 
Method Summary
 void assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
 void calcReason(int p, IVecInt outReason)
          Compute the reason for a given assignment.
 boolean equals(java.lang.Object obj)
           
 int get(int i)
          Return the ith literal of the clause.
 double getActivity()
          To obtain the activity of the constraint.
 int[] getLits()
           
 ILits getVocabulary()
           
 int hashCode()
           
 void incActivity(double claInc)
          Increase the constraint activity.
 boolean locked()
          Indicate wether a constraint is responsible from an assignment.
 boolean propagate(UnitPropagationListener s, int p)
          Propagate the truth value of a literal in constraints in which that literal is falsified.
 void remove()
          Remove a constraint from the solver.
 void rescaleBy(double d)
          Rescale the clause activity by a value.
 boolean simplify()
          Simplifies a constraint, by removing top level falsified literals for instance.
 int size()
           
 java.lang.String toString()
           
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface org.sat4j.minisat.core.Constr
register, setLearnt
 
Methods inherited from interface org.sat4j.specs.IConstr
learnt
 

Field Detail

middleLits

protected final int[] middleLits

voc

protected final ILits voc

head

protected int head

tail

protected int tail
Constructor Detail

HTClause

public HTClause(IVecInt ps,
                ILits voc)
Creates a new basic clause

Parameters:
voc - the vocabulary of the formula
ps - A VecInt that WILL BE EMPTY after calling that method.
Method Detail

calcReason

public void calcReason(int p,
                       IVecInt outReason)
Description copied from interface: Constr
Compute the reason for a given assignment. If the constraint is a clause, it is supposed to be either a unit clause or a falsified one.

Specified by:
calcReason in interface Constr
Parameters:
p - a satisfied literal (or Lit.UNDEFINED)
outReason - the list of falsified literals whose negation is the reason of the assignment of p to true.

remove

public void remove()
Description copied from interface: Constr
Remove a constraint from the solver.

Specified by:
remove in interface Constr

simplify

public boolean simplify()
Description copied from interface: Constr
Simplifies a constraint, by removing top level falsified literals for instance.

Specified by:
simplify in interface Constr
Returns:
true iff the constraint is satisfied.

propagate

public boolean propagate(UnitPropagationListener s,
                         int p)
Description copied from interface: Propagatable
Propagate the truth value of a literal in constraints in which that literal is falsified.

Specified by:
propagate in interface Propagatable
Parameters:
s - something able to perform unit propagation
p - the literal being propagated. Its negation must appear in the constraint.
Returns:
false iff an inconsistency (a contradiction) is detected.

locked

public boolean locked()
Description copied from interface: Constr
Indicate wether a constraint is responsible from an assignment.

Specified by:
locked in interface Constr
Returns:
true if a constraint is a "reason" for an assignment.

getActivity

public double getActivity()
Description copied from interface: Constr
To obtain the activity of the constraint.

Specified by:
getActivity in interface Constr
Returns:
the activity of the clause

toString

public java.lang.String toString()
Overrides:
toString in class java.lang.Object

get

public int get(int i)
Return the ith literal of the clause. Note that the order of the literals does change during the search...

Specified by:
get in interface IConstr
Parameters:
i - the index of the literal
Returns:
the literal

incActivity

public void incActivity(double claInc)
Description copied from interface: Constr
Increase the constraint activity.

Specified by:
incActivity in interface Constr
Parameters:
claInc -

rescaleBy

public void rescaleBy(double d)
Description copied from interface: Constr
Rescale the clause activity by a value.

Specified by:
rescaleBy in interface Constr
Parameters:
d -

size

public int size()
Specified by:
size in interface IConstr
Returns:
the number of literals in the constraint.

assertConstraint

public void assertConstraint(UnitPropagationListener s)
Description copied from interface: Constr
Method called when the constraint is to be asserted. It means that the constraint was learnt during the search and it should now propagate some truth values. In the clausal case, only one literal should be propagated. In other cases, it might be different.

Specified by:
assertConstraint in interface Constr
Parameters:
s - a UnitPropagationListener to use for unit propagation.

getVocabulary

public ILits getVocabulary()

getLits

public int[] getLits()

equals

public boolean equals(java.lang.Object obj)
Overrides:
equals in class java.lang.Object

hashCode

public int hashCode()
Overrides:
hashCode in class java.lang.Object


Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.