org.sat4j.tools.encoding
Class Binary

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

public class Binary
extends EncodingStrategyAdapter

Binary encoding for the "at most one" and "at most k" cases. For the case "at most one", we can use the binary encoding (also called birwise encoding) first described in A. M. Frisch, T. J. Peugniez, A. J. Dogget and P. Nightingale, "Solving Non-Boolean Satisfiability Problems With Stochastic Local Search: A Comparison of Encodings" in Journal of Automated Reasoning, vol. 35, n 1-3, 2005. The approach is generalized for the "at most k" case 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

Binary()

Method Summary

IConstr	addAtLeast(ISolver solver, IVecInt literals, int k)
IConstr	addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	addAtMostOne(ISolver solver, IVecInt literals) p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.
IConstr	addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	addExactlyOne(ISolver solver, IVecInt literals)

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

addAtLeastOne, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

Binary

public Binary()

Method Detail

addAtMostOne

public IConstr addAtMostOne(ISolver solver,
                            IVecInt literals)
                     throws ContradictionException

p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.

Overrides:

addAtMostOne in class EncodingStrategyAdapter

Throws:

ContradictionException

addAtMost

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

Overrides:

addAtMost in class EncodingStrategyAdapter

Throws:

ContradictionException

addAtLeast

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

Overrides:

addAtLeast 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