org.sat4j.tools.encoding

Class Ladder

java.lang.Object

org.sat4j.tools.encoding.EncodingStrategyAdapter

org.sat4j.tools.encoding.Ladder

All Implemented Interfaces:

java.io.Serializable

public class Ladder
extends EncodingStrategyAdapter

Ladder encoding for the "at most one" and "exactly one" cases. The ladder encoding described in: I. P. Gent and P. Nightingale, "A new encoding for AllDifferent into SAT", in International Workshop on Modeling and Reformulating Constraint Satisfaction Problems, 2004

Since:

2.3.1

Author:

sroussel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
Ladder()

Method Summary

Modifier and Type	Method and Description
IConstr	addAtMostOne(ISolver solver, IVecInt literals)
IConstr	addExactlyOne(ISolver solver, IVecInt literals)

Methods inherited from class org.sat4j.tools.encoding.EncodingStrategyAdapter

addAtLeast, addAtLeastOne, addAtMost, addExactly, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

Ladder

public Ladder()

Method Detail

addAtMostOne

public IConstr addAtMostOne(ISolver solver,
                            IVecInt literals)
                     throws ContradictionException

Overrides:

addAtMostOne in class EncodingStrategyAdapter

Throws:

ContradictionException

addExactlyOne

public IConstr addExactlyOne(ISolver solver,
                             IVecInt literals)
                      throws ContradictionException

Overrides:

addExactlyOne in class EncodingStrategyAdapter

Throws:

ContradictionException