org.sat4j.tools.encoding
Class Product

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

public class Product
extends EncodingStrategyAdapter

The encoding for "at most one" constraints was introduced by J. Chen in "A New SAT Encoding for the At-Most-One Constraint" in Proceedings of the Tenth International Workshop of Constraint Modeling and Reformulation, 2010 For the generalization to "at most k" constraint, we use the encoding introduced in 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

Since:

2.3.1

Author:

sroussel

Constructor Summary

Product()

Method Summary

IConstr	addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
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

Product

public Product()

Method Detail

addAtMostNonOpt

public IConstr addAtMostNonOpt(ISolver solver,
                               IVecInt literals,
                               int k)
                        throws ContradictionException

Throws:

ContradictionException

addAtMost

public IConstr addAtMost(ISolver solver,
                         IVecInt literals,
                         int k)
                  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