org.sat4j.maxsat

Class UnitWeightedClause

java.lang.Object

org.sat4j.maxsat.UnitWeightedClause

All Implemented Interfaces:

IConstr

public class UnitWeightedClause
extends Object
implements IConstr

Method Summary

Methods

Modifier and Type	Method and Description
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.
int	get(int i) returns the ith literal in the constraint
double	getActivity() To obtain the activity of the constraint.
static UnitWeightedClause	instance()
boolean	learnt()
int	size()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

instance

public static UnitWeightedClause instance()

learnt

public boolean learnt()

Specified by:

learnt in interface IConstr

Returns:

true iff the clause was learnt during the search

size

public int size()

Specified by:

size in interface IConstr

Returns:

the number of literals in the constraint.

get

public int get(int i)

Description copied from interface: IConstr

returns the ith literal in the constraint

Specified by:

get in interface IConstr

Parameters:

i - the index of the literal

Returns:

a literal

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.

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.