如何使用z3py设置“最多n次”之类的要求？

如何解决如何使用z3py设置“最多n次”之类的要求？

我是python的新手，还是z3的新手。我正在尝试通过z3py解决一些SMT问题。 现在我需要设置一个限制：array1（1,8）至少有5个零。但是我遇到了一些错误。

/// <summary> /// Extension methods to quickly convert byte array to string and back. /// </summary> public static class HexConverter { /// <summary> /// Map values to hex digits /// </summary> private static readonly char[] HexDigits = { '0','1','2','3','4','5','6','7','8','9','A','B','C','D','E','F' }; /// <summary> /// Map 56 characters between ['0','F'] to their hex equivalents,and set invalid characters /// such that they will overflow byte to fail conversion. /// </summary> private static readonly ushort[] HexValues = { 0x0000,0x0001,0x0002,0x0003,0x0004,0x0005,0x0006,0x0007,0x0008,0x0009,0x0100,0x000A,0x000B,0x000C,0x000D,0x000E,0x000F,0x000F }; /// <summary> /// Empty byte array /// </summary> private static readonly byte[] Empty = new byte[0]; /// <summary> /// Convert a byte array to a hexadecimal string. /// </summary> /// <param name="bytes"> /// The input byte array. /// </param> /// <returns> /// A string of hexadecimal digits. /// </returns> public static string ToHexString(this byte[] bytes) { var c = new char[bytes.Length * 2]; for (int i = 0,j = 0; i < bytes.Length; i++) { c[j++] = HexDigits[bytes[i] >> 4]; c[j++] = HexDigits[bytes[i] & 0x0F]; } return new string(c); } /// <summary> /// Parse a string of hexadecimal digits into a byte array. /// </summary> /// <param name="hexadecimalString"> /// The hexadecimal string. /// </param> /// <returns> /// The parsed <see cref="byte[]"/> array. /// </returns> /// <exception cref="ArgumentException"> /// The input string either contained invalid characters,or was of an odd length. /// </exception> public static byte[] ToByteArray(string hexadecimalString) { if (!TryParse(hexadecimalString,out var value)) { throw new ArgumentException("Invalid hexadecimal string",nameof(hexadecimalString)); } return value; } /// <summary> /// Parse a hexadecimal string to bytes /// </summary> /// <param name="hexadecimalString"> /// The hexadecimal string,which must be an even number of characters. /// </param> /// <param name="value"> /// The parsed value if successful. /// </param> /// <returns> /// True if successful. /// </returns> public static bool TryParse(string hexadecimalString,out byte[] value) { if (hexadecimalString.Length == 0) { value = Empty; return true; } if (hexadecimalString.Length % 2 != 0) { value = Empty; return false; } try { value = new byte[hexadecimalString.Length / 2]; for (int i = 0,j = 0; j < hexadecimalString.Length; i++) { value[i] = (byte)((HexValues[hexadecimalString[j++] - '0'] << 4) | HexValues[hexadecimalString[j++] - '0']); } return true; } catch (OverflowException) { value = Empty; return false; } } }

这是我声明的内容，当我想使用al1,al2,al3,al4,al5,al6,al7,al8=Ints('al1 al2 al3 al4 al5 al6 al7 al8')时，会出现错误消息，提示al1=If(be1*wi1,1,0) 或Z3Exception: Value cannot be converted into a Z3 Boolean value

我想知道如何计算这些元素中有多少个零？，我不确定是否可以更改此声明...我只是从示例中复制了这一部分。 >

解决方法

始终最好张贴完整的代码，以便人们可以看到并评论您的尝试。

在任何一种情况下，要表达这种最少/最多种类的约束，都应使用所谓的“伪布尔”约束。例如，要说这些元素中至少有5个是0，您可以说：

from z3 import *

al1,al2,al3,al4,al5,al6,al7,al8 = Ints('al1 al2 al3 al4 al5 al6 al7 al8')

s = Solver()

s.add(AtLeast(al1 == 0,al2 == 0,al3 == 0,al4 == 0,al5 == 0,al6 == 0,al7 == 0,al8 == 0,5))

print(s.check())
print(s.model())

运行此命令时，我得到：

sat
[al8 = 1,al7 = 1,al6 = 1,al5 = 0,al4 = 0,al3 = 0,al2 = 0,al1 = 0]

您看到5个变量为0。（显然，这不是唯一的模型，但z3为您找到了一个模型。您显然可以添加其他约束。）

有关伪布尔约束的详细信息，请参见：https://z3prover.github.io/api/html/namespacez3py.html#a8575bdeb9d1b8feac119aa162b5acfa6

您要研究的功能称为：AtMost，AtLeast，PbLe，PbGe和PbEq。