org.sat4j.tools.encoding
Class Sequential

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

public class Sequential
extends EncodingStrategyAdapter

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

Constructor Summary

Sequential()

Method Summary

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.

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

addAtLeast, addAtLeastOne, addAtMostOne, addExactly, addExactlyOne, 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