Z3Py中的K-out-of約束

Question

我正在使用Z3 theorem prover（Z3Py）的Python綁定。我有N個布爾變量，x1，..，xN。我想表達這樣一個約束，即它們中的N個應該是正確的。我該怎麼做，在Z3Py？有沒有內置的支持？我查看了在線文檔，但Z3Py docs沒有提及任何API。我知道我可以分別表示至少有一個是真的（assert Or（x1，..，xN）），並且至多有一個是真的（assert Not（And） （xi，xj）），對於所有i，j）。我也知道other ways手動表示N中的1和N中的約束。但是我有這樣的印象：當求解器內置對這個約束的支持時，它有時可能比手動表達它更有效。

Answer 1

是的，Z3Py內置了對此的支持。這裏有一個未公開的API，這在Z3Py文檔中沒有提到：使用PbEq。特別是，表達式

PbEq(((x1,1),(x2,1),..,(xN,1)),K) 

如果N個布爾變量中恰好有K個參數設置爲true，則該參數爲真。有some reports，這種編碼將比手動表達約束的天真方式更快。

要表達1-out-of-N約束，只需設置K = 1並使用PbEq即可。要表示最多約束的K-out-N約束，請使用PbLe。要表達一個至少爲K-out-N的約束條件，請使用PbGe。