org.sat4j.tools.encoding
Class Product
java.lang.Object
org.sat4j.tools.encoding.EncodingStrategyAdapter
org.sat4j.tools.encoding.Product
public class Product
- extends EncodingStrategyAdapter
Implementation of product encoding for at most one and at most k constraints.
The encoding for "at most one" constraints was introduced by J. Chen in
"A New SAT Encoding for the At-Most-One Constraint" in Proceedings of the
Tenth International Workshop of Constraint Modeling and Reformulation, 2010
For the generalization to "at most k" constraint, we use the encoding
introduced 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
Method Summary |
IConstr |
addAtLeast(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
addAtMost(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
addAtMostNonOpt(ISolver solver,
IVecInt literals,
int k)
|
IConstr |
addAtMostOne(ISolver solver,
IVecInt literals)
|
IConstr |
addExactly(ISolver solver,
IVecInt literals,
int degree)
|
IConstr |
addExactlyOne(ISolver solver,
IVecInt literals)
|
Product
public Product()
addAtMostNonOpt
public IConstr addAtMostNonOpt(ISolver solver,
IVecInt literals,
int k)
throws ContradictionException
- Throws:
ContradictionException
addAtMost
public IConstr addAtMost(ISolver solver,
IVecInt literals,
int k)
throws ContradictionException
- Overrides:
addAtMost
in class EncodingStrategyAdapter
- Throws:
ContradictionException
addAtMostOne
public IConstr addAtMostOne(ISolver solver,
IVecInt literals)
throws ContradictionException
- Overrides:
addAtMostOne
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
Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.