Мультисетевое разбиение с использованием линейной арифметики и Z3

Question

Я должен разделить мультимножество на два набора, суммы которых равны.Например, с учетом мультимножества:

1 3 5 1 3 -1 2 0

я бы вывел два набора:

1) 1 3 3
2) 5 -1 2 1 0

, оба из которых равны 7.

Мне нужно это сделатьиспользуя Z3 (формат ввода smt2) и «линейную арифметическую логику», которая определяется как:

formula : formula /\ formula | (formula) | atom
   atom : sum op sum
     op : = | <= | <
    sum : term | sum + term
   term : identifier | constant | constant identifier

Я, честно говоря, не знаю, с чего начать, и любые советы будут приветствоваться.

С уважением.

Answer 1

Несмотря на то, что SMT-Lib2 достаточно выразителен, он не самый простой язык для программирования. Если у вас нет жестких требований к тому, что вам придется кодировать непосредственно в SMTLib2, я бы порекомендовал поискать другие языки с высокоуровневыми привязками кSMT решатели.Например, и в Haskell, и в Scala есть библиотеки, которые позволяют создавать сценарии для SMT-решателей на более высоком уровне.Вот как решить вашу проблему с помощью Haskell, например: https://gist.github.com/1701881.

Идея состоит в том, что эти библиотеки позволяют вам кодировать на гораздо более высоком уровне, а затем выполнять необходимый перевод и запросы SMT-решателя.для вас за кадром.(Если вам действительно нужно разобраться с кодировкой SMTLib вашей проблемы, вы также можете использовать эти библиотеки, поскольку они обычно поставляются с необходимым API для создания дампов SMTLib, которые они генерируют перед запросом решателя.)

Хотя эти библиотеки могут не предлагать все, что Z3 дает вам доступ через SMTLib, их гораздо проще использовать для решения большинства практических задач.

Answer 2

Вот идея:

1- Создайте целочисленную переменную 0-1 c_i для каждого элемента.Идея в том, что c_i равно нулю, если элемент находится в первом наборе, и 1, если он находится во втором наборе.Вы можете сделать это, сказав, что 0 <= c_i и c_i <= 1.

2 - сумма элементов в первом наборе может быть записана как 1*(1 - c_1) + 3*(1 - c_2) + ... +

3 - суммаэлементы во втором наборе могут быть записаны как 1*c1 + 3*c2 + ...