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

Question

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

有没有人实现了更好的排序算法（Merge/Heap/QuickSort）？您对提高性能（减少断言数量和/或减少计算时间）有何建议？

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) 做得更好的了。最重要的是，所有这些最终都会进行成对比较。如果您的列表中包含恒定值，有些可能会表现更好；但这毕竟不是真正有趣的案例。而且这种性能测量是相当有问题的，因为您并不真正知道这些约束将如何与系统中的所有其他约束相互作用；并且不同的算法可能会根据存在的其他约束条件执行不同的操作。

话虽如此，我认为这是一个值得思考的有趣问题。我的直觉是进行基数排序的变体可能是个好主意，尤其是在存在重复元素的情况下。这个想法是你把列表变成一个整数数组，计算每个元素的存在。我称之为“bagifying”，虽然这个名字并不完美。然后，您断言原始版本的“袋装”版本和排序版本是相同的。以下是您在 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 表现更好：所以我猜创建和操作数组有无法避免的额外成本。但这可能是另一个技巧，如果输入有很多符号值和很多其他约束，可能会表现得更好（也许？）。当然，这是猜测。

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