org.sat4j.minisat.constraints.cnf
Class BinaryClause

java.lang.Object
  org.sat4j.minisat.constraints.cnf.BinaryClause

All Implemented Interfaces:

java.io.Serializable, Constr, Propagatable, IConstr

Direct Known Subclasses:

LearntBinaryClause, OriginalBinaryClause

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

Data structure for binary clause.

Author:

leberre

See Also:

Serialized Form

Constructor Summary

BinaryClause(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) Retourne le ieme literal de la 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	register() Register the constraint to the solver.
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

setLearnt

Methods inherited from interface org.sat4j.specs.IConstr

learnt

Constructor Detail

BinaryClause

public BinaryClause(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)

Retourne le ieme literal de la clause. Attention, cet ordre change durant la recherche.

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

register

public void register()

Description copied from interface: Constr

Register the constraint to the solver.

Specified by:

register in interface Constr