org.sat4j.tools.encoding

Class Product

java.lang.Object

org.sat4j.tools.encoding.EncodingStrategyAdapter

org.sat4j.tools.encoding.Product

All Implemented Interfaces:

Serializable

public class Product
extends EncodingStrategyAdapter

Implementation of product encoding for at most one and at most k constraints. 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

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
Product()

Method Summary

Methods

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

addAtLeast, addAtLeastOne, 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

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