org.sat4j.tools.encoding
Class Sequential

java.lang.Object
  extended by org.sat4j.tools.encoding.EncodingStrategyAdapter
      extended by 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


Copyright © 2011 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.