org.sat4j.minisat.constraints.cnf
Class OriginalBinaryClause

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

All Implemented Interfaces:

Serializable, Constr, Propagatable, IConstr

public class OriginalBinaryClause
extends BinaryClause

Since:

2.1

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.minisat.constraints.cnf.BinaryClause

activity, head, tail

Constructor Summary

OriginalBinaryClause(IVecInt ps, ILits voc)

Method Summary

static OriginalBinaryClause	brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
void	forwardActivity(double claInc)
void	incActivity(double claInc) Increase the constraint activity.
boolean	learnt()
void	setActivity(double claInc) Set the activity at a specific value
void	setLearnt() Mark a constraint as learnt.

Methods inherited from class org.sat4j.minisat.constraints.cnf.BinaryClause

assertConstraint, calcReason, canBePropagatedMultipleTimes, equals, get, getActivity, getLits, getVocabulary, hashCode, locked, propagate, register, remove, rescaleBy, simplify, size, toConstraint, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

OriginalBinaryClause

public OriginalBinaryClause(IVecInt ps,
                            ILits voc)

Method Detail

setLearnt

public void setLearnt()

Description copied from interface: Constr

Mark a constraint as learnt.

learnt

public boolean learnt()

Returns:

true iff the clause was learnt during the search

brandNewClause

public static OriginalBinaryClause brandNewClause(UnitPropagationListener s,
                                                  ILits voc,
                                                  IVecInt literals)

Creates a brand new clause, presumably from external data.

Parameters:

s - the object responsible for unit propagation

voc - the vocabulary

literals - the literals to store in the clause

Returns:

the created clause or null if the clause should be ignored (tautology for example)

forwardActivity

public void forwardActivity(double claInc)

incActivity

public void incActivity(double claInc)

Description copied from interface: Constr

Increase the constraint activity.

Parameters:

claInc -

setActivity

public void setActivity(double claInc)

Description copied from interface: Constr

Set the activity at a specific value

Parameters:

claInc - the new activity