From: Claire Wolf <claire@symbioticeda.com>
Date: Thu, 2 Apr 2020 10:22:28 +0000 (+0200)
Subject: Improve ezsat onehot encoding scheme
X-Git-Tag: working-ls180~706^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=65a3ff69bdc7295fff5b806d8fdf424e0f77aae1;p=yosys.git

Improve ezsat onehot encoding scheme

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
---

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);
 }