org.sat4j.tools.encoding

Class Sequential

java.lang.Object

org.sat4j.tools.encoding.EncodingStrategyAdapter

org.sat4j.tools.encoding.Sequential

All Implemented Interfaces:

Serializable

public class Sequential
extends EncodingStrategyAdapter

Implementation of the sequential encoding for the at most k constraint. For the cases "at most k", we can use the sequential encoding described in: C. Sinz, "Towards an Optimal CNF Encoding of Boolean Cardinality Constraints", in International Conference on Principles and Practices of Constraint Programming , 2005

Since:

2.3.1

Author:

sroussel

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
Sequential()

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addAtMost(ISolver solver, IVecInt literals, int k) This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.
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

Sequential

public Sequential()

Method Detail

addAtMost

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

This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.

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