org.sat4j.tools.encoding
Class Binomial

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

public class Binomial
extends EncodingStrategyAdapter

For the "at most one" case, this encoding is equivalent to the one referred to in the literature as the pair-wise or naive encoding. For the "at most k" case, the previous encoding is generalized with binomial selection.

Since:

2.3.1

Author:

stephanieroussel

Constructor Summary

Binomial()

Method Summary

IConstr	addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	addAtMostOne(ISolver solver, IVecInt literals)

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

addAtLeast, addAtLeastOne, addExactly, addExactlyOne, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

Binomial

public Binomial()

Method Detail

addAtMost

public IConstr addAtMost(ISolver solver,
                         IVecInt literals,
                         int degree)
                  throws ContradictionException

Overrides:

addAtMost in class EncodingStrategyAdapter

Throws:

ContradictionException

addAtMostOne

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

Overrides:

addAtMostOne in class EncodingStrategyAdapter

Throws:

ContradictionException