org.sat4j.tools.encoding
Class Ladder

java.lang.Object
  org.sat4j.tools.encoding.EncodingStrategyAdapter
      org.sat4j.tools.encoding.Ladder

public class Ladder
extends EncodingStrategyAdapter

For the cases "at most one" and "exactly one", we can use 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

Constructor Summary

Ladder()

Method Summary

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