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

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.

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.


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