org.sat4j.minisat.core

Interface Constr

All Superinterfaces:

IConstr

All Known Implementing Classes:

AtLeast, BinaryClause, HTClause, LearntBinaryClause, LearntHTClause, LearntWLClause, MaxWatchCard, MinWatchCard, OriginalBinaryClause, OriginalHTClause, OriginalWLClause, UnitClause, UnitClauses, WLClause

public interface Constr
extends IConstr

Basic constraint abstraction used in Solver. Any new constraint type should implement that interface.

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
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.
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.
void	forwardActivity(double claInc) Deprecated.
void	incActivity(double claInc) Increase the constraint activity.
boolean	locked() Indicate wether a constraint is responsible from an assignment.
void	register() Register the constraint to the solver.
void	remove(UnitPropagationListener upl) Remove a constraint from the solver.
void	rescaleBy(double d) Rescale the clause activity by a value.
void	setActivity(double d) Set the activity at a specific value
void	setLearnt() Mark a constraint as learnt.
boolean	simplify() Simplifies a constraint, by removing top level falsified literals for instance.

Methods inherited from interface org.sat4j.specs.IConstr

canBePropagatedMultipleTimes, get, getActivity, learnt, size

Method Detail

remove

void remove(UnitPropagationListener upl)

Remove a constraint from the solver.

Parameters:

upl -

Since:

2.1

simplify

boolean simplify()

Simplifies a constraint, by removing top level falsified literals for instance.

Returns:

true iff the constraint is satisfied and can be removed from the database.

calcReason

void calcReason(int p,
              IVecInt outReason)

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

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.

calcReasonOnTheFly

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. Compared to the method 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.

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.

Since:

2.3.3

incActivity

void incActivity(double claInc)

Increase the constraint activity.

Parameters:

claInc - the value to increase the activity with

forwardActivity

@Deprecated
void forwardActivity(double claInc)

Deprecated.

Parameters:

claInc -

Since:

2.1

locked

boolean locked()

Indicate wether a constraint is responsible from an assignment.

Returns:

true if a constraint is a "reason" for an assignment.

setLearnt

void setLearnt()

Mark a constraint as learnt.

register

void register()

Register the constraint to the solver.

rescaleBy

void rescaleBy(double d)

Rescale the clause activity by a value.

Parameters:

d - the value to rescale the clause activity with.

setActivity

void setActivity(double d)

Set the activity at a specific value

Parameters:

d - the new activity

Since:

2.3.1

assertConstraint

void assertConstraint(UnitPropagationListener s)

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.

Parameters:

s - a UnitPropagationListener to use for unit propagation.