org.sat4j.tools.encoding

Class Commander

java.lang.Object

org.sat4j.tools.encoding.EncodingStrategyAdapter

org.sat4j.tools.encoding.Commander

All Implemented Interfaces:

Serializable

public class Commander
extends EncodingStrategyAdapter

Commander encoding for "at most one" and "at most k" cases. The case "at most one" is introduced in W. Klieber and G. Kwon "Efficient CNF encoding for selecting 1 from N objects" in Fourth Workshop on Constraints in Formal Verification, 2007. The generalization to the "at most k" case is described 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
Commander()

Method Summary

Methods

Modifier and Type	Method and Description
IConstr	addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	addAtMostOne(ISolver solver, IVecInt literals) In this encoding, variables are partitioned in groups.
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

Commander

public Commander()

Method Detail

addAtMostOne

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

In this encoding, variables are partitioned in groups. Kwon and Klieber claim that the fewest clauses are produced when the size of the groups is 3, thus leading to 3.5 clauses and introducing n/2 variables.

Overrides:

addAtMostOne in class EncodingStrategyAdapter

Throws:

ContradictionException

addAtMost

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

Overrides:

addAtMost 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