使用Z3 python对整数列表进行排序

Question

我正在寻找使用Z3对整数列表进行排序的最快方法。到目前为止，我实现了两种不同的算法：第一种算法只能处理不包含任何重复值的列表。第二个是冒泡排序算法的实现，它可以对任何类型的整数列表进行排序，但如果列表长度增加，则速度会非常慢（算法是O（n**2），第一个算法不知道）。下面是测试和测试它们性能的代码

是否有人实现了更好的排序算法（合并/堆/快速排序）？对于提高性能（减少断言数量和/或减少计算时间），您有什么建议

from z3 import *
from time import perf_counter

def sort_list_of_z3_var(lst):
    """Sort a list of integers that have different values"""
    n = len(lst)
    # create the z3 IntSort list
    a = [FreshInt() for i in range(n)]
    asst = []
    # add the related assertions
    for i in range(n):
        asst.append(Or([a[i] == lst[j] for j in range(n)]))
    asst.append(And([a[i] < a[i + 1] for i in range(n - 1)]))
    return a, asst

def sort_bubble(lst):
    """Take a list of int variables, return the list of new variables
    sorted using the bubble recursive sort"""
    cstr = [] # list of assertions to be returned
    n = len(lst)
    # create the z3 IntSort list
    sorted_list = [FreshInt() for i in range(n)]
    # fill in the variable list
    i = 0
    for s in sorted_list:
        cstr.append(s == lst[i])
        i += 1

    def bubble_up(arr):
        new_asst = []
        for i in range(len(arr) - 1):
            x = arr[i]
            y = arr[i + 1]
            # compare and swap x and y
            x1, y1 = FreshInt(), FreshInt()
            c = If(x <= y, And(x1 == x, y1 == y), And(x1 == y, y1 == x))
            # store values
            arr[i] = x1
            arr[i + 1] = y1
            new_asst.append(c)
        return arr, new_asst

    # recursive call to bubble_up
    for _ in range(len(sorted_list)):
        sorted_list, cst = bubble_up(sorted_list)
        cstr.extend(cst)
    return sorted_list, cstr

# define 2 lists to be sorted
integer_list_distinct = [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
integer_list_not_distinct = [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

# first algorithm
z3_vars_1, z3_assertions_1 = sort_list_of_z3_var(integer_list_distinct)
s = Solver()
s.add(z3_assertions_1)
time_1 = perf_counter()
s.check()
time_2 = perf_counter()
solution_1 = s.model()
result_1 = [solution_1[v].as_long() for v in z3_vars_1]
print(result_1)
print("Time Alg.1:", time_2 - time_1)

# second algorithm
z3_vars_2, z3_assertions_2 = sort_bubble(integer_list_distinct)
s2 = Solver()
s2.add(z3_assertions_2)
time_3 = perf_counter()
s2.check()
time_4 = perf_counter()
solution_2 = s2.model()
result_2 = [solution_2[v].as_long() for v in z3_vars_2]
print(result_2)
print("Time Alg.2:", time_4 - time_3)

Answer 1

有了符号输入，我认为你没有比O(n^2)更好的了。总之，所有这些最终都将进行成对比较。如果您的列表中有常量值，有些可能会执行得更好；但这毕竟不是一个有趣的案例。这种性能度量是相当有问题的，因为您不知道这些约束将如何与系统中的所有其他约束交互；不同的算法可能会根据存在的其他约束执行不同的操作

话虽如此，我认为这是一个值得思考的有趣问题。我的直觉是做一个基数排序的变体可能是个好主意，尤其是在存在重复元素的情况下。其思想是将列表转换为整数数组，计算每个元素的存在情况。我称之为“Baggying”，虽然这个名字并不完美。然后，您断言原始版本和排序版本的“bagified”版本是相同的。以下是如何在z3py中编写代码：

def bagSort(s, lst):
    n = len(lst)

    bag = K(IntSort(), 0)
    for i in lst:
       bag = Store(bag, i, bag[i] + 1)

    result = [FreshInt() for i in range(n)]
    resultBag = K(IntSort(), 0)
    for i in result:
        resultBag = Store(resultBag, i, resultBag[i] + 1)

    for i in range(n-1):
        s.add(result[i] <= result[i+1])

    for i in lst:
        s.add(bag[i] == resultBag[i])   

    s.check()
    m = s.model()
    return [m[i] for i in result]

然后像这样使用它：

s = Solver()
print(bagSort(s, integer_list_not_distinct))

在一些简单的测试中，我发现冒泡排序的性能比bagSort好：所以我想创建和操作数组会带来无法避免的额外成本。但这可能是另一个技巧，如果输入有很多符号值和很多其他约束，可能会表现得更好（也许？）。当然，这是猜测

对于在具体值上运行的算法来说，度量性能是很困难的，而且在存在符号表达式的情况下，度量性能确实很棘手。除非这仅仅是好奇，否则我建议你在实际问题上尝试所有这些方法，并选择性能更好的方法；记住问题的不同实例可能受益于不同的算法