org.sat4j.tools.encoding
Class Binomial

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

public class Binomial
extends EncodingStrategyAdapter

Binomial encoding for the "at most one" and "at most k" cases. 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 (see A. M. Frisch and P. A. Giannaros, "SAT Encodings of the At-Most-k Constraint", in International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2010 for details).

Since:

2.3.1

Author:

stephanieroussel

Constructor Summary

Binomial()

Method Summary

IConstr	addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	addAtLeastOne(ISolver solver, IVecInt literals)
IConstr	addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	addAtMostOne(ISolver solver, IVecInt literals)
IConstr	addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	addExactlyOne(ISolver solver, IVecInt literals)

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

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

addExactlyOne

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

Overrides:

addExactlyOne in class EncodingStrategyAdapter

Throws:

ContradictionException

addExactly

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

Overrides:

addExactly in class EncodingStrategyAdapter

Throws:

ContradictionException

addAtLeast

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

Overrides:

addAtLeast in class EncodingStrategyAdapter

Throws:

ContradictionException

addAtLeastOne

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

Overrides:

addAtLeastOne in class EncodingStrategyAdapter

Throws:

ContradictionException