org.sat4j.minisat.constraints.cnf

Class HTClause

java.lang.Object

org.sat4j.minisat.constraints.cnf.HTClause

All Implemented Interfaces:

Serializable, Constr, Propagatable, IConstr

Direct Known Subclasses:

LearntHTClause, OriginalHTClause

public abstract class HTClause
extends Object
implements Propagatable, Constr, 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.

Since:

2.1

Author:

leberre

See Also:

BinaryClause, UnitClause, Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
protected double	activity
protected int	head
protected int[]	middleLits
protected int	tail
protected ILits	voc

Constructor Summary

Constructors

Constructor and Description
HTClause(IVecInt ps, ILits voc) Creates a new basic clause

Method Summary

Methods

Modifier and Type	Method and Description
void	assertConstraint(UnitPropagationListener s) Method called when the constraint is to be asserted.
void	assertConstraintIfNeeded(UnitPropagationListener s) Method called when the constraint is added to the solver "on the fly".
void	calcReason(int p, IVecInt outReason) Compute the reason for a given assignment.
void	calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) Compute the reason for a given assignment in a the constraint created on the fly in the solver.
boolean	canBePropagatedMultipleTimes() Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g.
boolean	equals(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()
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(UnitPropagationListener upl) 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()
Constr	toConstraint() Allow to access a constraint view of the propagatable to avoid casting.
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

forwardActivity, incActivity, register, setActivity, setLearnt

Methods inherited from interface org.sat4j.specs.IConstr

learnt

Field Detail

activity

protected double activity

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. It is expected that the falsification of the constraint has been detected as soon at is occurs (e.g. using Propagatable.propagate(UnitPropagationListener, int).

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(UnitPropagationListener upl)

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 and can be removed from the database.

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: IConstr

To obtain the activity of the constraint.

Specified by:

getActivity in interface IConstr

Returns:

the activity of the clause

toString

public String toString()

Overrides:

toString in class 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

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 learned 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.

assertConstraintIfNeeded

public void assertConstraintIfNeeded(UnitPropagationListener s)

Description copied from interface: Constr

Method called when the constraint is added to the solver "on the fly". In that case, the constraint may or may not have to propagate some literals, unlike the Constr.assertConstraint(UnitPropagationListener) method.

Specified by:

assertConstraintIfNeeded in interface Constr

Parameters:

s - a UnitPropagationListener to use for unit propagation.

getVocabulary

public ILits getVocabulary()

getLits

public int[] getLits()

equals

public boolean equals(Object obj)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

canBePropagatedMultipleTimes

public boolean canBePropagatedMultipleTimes()

Description copied from interface: IConstr

Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g. cardinality constraints and pseudo-boolean constraints).

Specified by:

canBePropagatedMultipleTimes in interface IConstr

Returns:

true if the constraint can be used several times as a reason to propagate a literal.

toConstraint

public Constr toConstraint()

Description copied from interface: Propagatable

Allow to access a constraint view of the propagatable to avoid casting. In most cases, the constraint will implement directly propagatable thus will return itself. It will also also the implementation of more sophisticated watching strategy.

Specified by:

toConstraint in interface Propagatable

Returns:

the constraint associated to that propagatable.

calcReasonOnTheFly

public void calcReasonOnTheFly(int p,
                      IVecInt trail,
                      IVecInt outReason)

Description copied from interface: Constr

Compute the reason for a given assignment in a the constraint created on the fly in the solver. Compared to the method Constr.calcReason(int, IVecInt), the falsification may not have been detected as soon as possible. As such, it is necessary to take into account the order of the literals in the trail.

Specified by:

calcReasonOnTheFly in interface Constr

Parameters:

p - a satisfied literal (or Lit.UNDEFINED)

trail - all the literals satisfied in the solvers, should not be modified.

outReason - a list of falsified literals whose negation is the reason of the assignment of p to true.