aboutsummaryrefslogtreecommitdiffstats
path: root/libs
diff options
context:
space:
mode:
authorClaire Wolf <claire@symbioticeda.com>2020-04-02 12:22:28 +0200
committerClaire Wolf <claire@symbioticeda.com>2020-04-02 12:22:28 +0200
commit65a3ff69bdc7295fff5b806d8fdf424e0f77aae1 (patch)
tree6e300ffe2225f7f4a07bd3b6b5739cd7550e8484 /libs
parentf72b65b2a54be664f4ce95e0a8bdc68d09562bf1 (diff)
downloadyosys-65a3ff69bdc7295fff5b806d8fdf424e0f77aae1.tar.gz
yosys-65a3ff69bdc7295fff5b806d8fdf424e0f77aae1.tar.bz2
yosys-65a3ff69bdc7295fff5b806d8fdf424e0f77aae1.zip
Improve ezsat onehot encoding scheme
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/ezsat.cc42
1 files changed, 28 insertions, 14 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 47fdb8efe..8c666ca1f 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -1371,20 +1371,34 @@ int ezSAT::onehot(const std::vector<int> &vec, bool max_only)
if (max_only == false)
formula.push_back(expression(OpOr, vec));
- // create binary vector
- int num_bits = clog2(vec.size());
- std::vector<int> bits;
- for (int k = 0; k < num_bits; k++)
- bits.push_back(literal());
-
- // add at-most-one clauses using binary encoding
- for (size_t i = 0; i < vec.size(); i++)
- for (int k = 0; k < num_bits; k++) {
- std::vector<int> clause;
- clause.push_back(NOT(vec[i]));
- clause.push_back((i & (1 << k)) != 0 ? bits[k] : NOT(bits[k]));
- formula.push_back(expression(OpOr, clause));
- }
+ if (vec.size() < 8)
+ {
+ // fall-back to simple O(n^2) solution for small cases
+ for (size_t i = 0; i < vec.size(); i++)
+ for (size_t j = i+1; j < vec.size(); j++) {
+ std::vector<int> clause;
+ clause.push_back(NOT(vec[i]));
+ clause.push_back(NOT(vec[j]));
+ formula.push_back(expression(OpOr, clause));
+ }
+ }
+ else
+ {
+ // create binary vector
+ int num_bits = clog2(vec.size());
+ std::vector<int> bits;
+ for (int k = 0; k < num_bits; k++)
+ bits.push_back(literal());
+
+ // add at-most-one clauses using binary encoding
+ for (size_t i = 0; i < vec.size(); i++)
+ for (int k = 0; k < num_bits; k++) {
+ std::vector<int> clause;
+ clause.push_back(NOT(vec[i]));
+ clause.push_back((i & (1 << k)) != 0 ? bits[k] : NOT(bits[k]));
+ formula.push_back(expression(OpOr, clause));
+ }
+ }
return expression(OpAnd, formula);
}