org.sat4j.minisat.core
Interface Constr

All Superinterfaces:
IConstr, Propagatable
All Known Subinterfaces:
PBConstr
All Known Implementing Classes:
AtLeast, AtLeastPB, BinaryClauses, CBClause, DefaultWLClause, LearntWLClause, MaxWatchCard, MaxWatchPb, MinWatchCard, MinWatchCardPB, MinWatchPb, MixableCBClause, MixableCBClausePB, OriginalWLClause, PuebloMinWatchPb, TernaryClauses, WatchPb, WLClause, WLClausePB

public interface Constr
extends Propagatable, 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.
 double getActivity()
          To obtain the activity of the constraint.
 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()
          Remove a constraint from the solver.
 void rescaleBy(double d)
          Rescale the clause activity by a 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.minisat.core.Propagatable
propagate
 
Methods inherited from interface org.sat4j.specs.IConstr
get, learnt, size
 

Method Detail

remove

void remove()
Remove a constraint from the solver.


simplify

boolean simplify()
Simplifies a constraint, by removing top level falsified literals for instance.

Returns:
true iff the constraint is satisfied.

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

getActivity

double getActivity()
To obtain the activity of the constraint.

Returns:
the activity of the clause.

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.

assertConstraint

void assertConstraint(UnitPropagationListener s)
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.

Parameters:
s - a UnitPropagationListener to use for unit propagation.


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