Question

Я хотел бы создать массив Z3 ( A ), элементы которого являются переменными Z3 Int, и каждый из этих элементов имеет фиксированный диапазон. Кроме того, я хотел инициализировать значения этих элементов с помощью 0. Теперь пусть есть простая функция x1 + x2 + x3 = 6, где 0 <= x1, x2, x3 <= 4, где x1 , x2, x3 - переменные Z3 Int. Затем я хочу увеличить значения в позициях индекса x1, x2 и x3 (со значениями x1, x2 и x3, которые определяются Z3) A на 1. </p>

Например:

Мой вопрос в том, как инициализировать переменную Z3 с наименьшим возможным значением и использовать ее в качестве переменной счетчика?

Примечание. . и мин. возможные значения x1, x2 и x3 всегда являются наименьшим и наибольшим индексом A соответственно.

Patrick Trentin · Answer 1 · 08 мая 2020

Общие соображения:

При присвоении значения (x1, x2, x3) = (v1, v2, v3) любая перестановка (v1, v2, v3) также является решением проблемы. В некоторых случаях может быть удобно нарушить симметрию в пространстве поиска, потребовав, например, ∀ i, j.((i < j) => (x_i <= x_j)).
Это гораздо проще придумать каждое местоположение A_i как номер всех x_j присвоено значение i.

Python + z3:

from z3 import *

def model_to_str(m):
    fmt = "\t A:= {}; x := {};"
    A_tuple = tuple([m.eval(el) for el in A_list])
    x_tuple = tuple([m.eval(el) for el in x_list])
    return fmt.format(A_tuple, x_tuple)

###########
# PROBLEM #
###########

s = Solver()

# declarations
A_length = 5
A_list = [Int('A_{0}'.format(idx)) for idx in range(0, A_length)]
x_list = [Int('x_{0}'.format(idx)) for idx in range(0, 3)]

# A's constraints
for i, A_i in enumerate(A_list):
    s.add(A_i == Sum([If(x_j == i, 1, 0) for x_j in x_list]))
    s.add(A_i <= 2)

# x's constraints
s.add(6 == Sum(x_list))
for x_i in x_list:
    s.add(0 <= x_i)
    s.add(x_i < A_length)

# Symmetry-breaking constraints:
# (remove symmetry solutions)
#s.add(x_list[0] <= x_list[1])
#s.add(x_list[0] <= x_list[2])
#s.add(x_list[1] <= x_list[2])

# Get one solution:
if s.check() == sat:
    print("Random Solution:")
    print(model_to_str(s.model()))

# Get all solutions:
s.push()
print("\nEnumerate All Solutions:")
while s.check() == sat:
    m = s.model()
    print(model_to_str(m))
    s.add(Or([x_j != m.eval(x_j) for x_j in x_list]))
s.pop()

# Enumerate all possible assignments
print("\nTry All Possible Assignments:")
for x_0_val in range(0, A_length):
    for x_1_val in range(0, A_length):
        for x_2_val in range(0, A_length):
            values = (x_0_val, x_1_val, x_2_val)

            s.push()
            s.add([x_j == x_j_val for x_j, x_j_val in zip(x_list, values)])

            if s.check() == sat:
                print(model_to_str(s.model()))
            else:
                print("\t\tx := {} is unsat!".format(values))

            s.pop()

Вывод:

Random Solution:
     A:= (1, 0, 1, 0, 1); x := (4, 0, 2);

Enumerate All Solutions:
     A:= (1, 0, 1, 0, 1); x := (2, 0, 4);
     A:= (1, 0, 1, 0, 1); x := (2, 4, 0);
     A:= (0, 1, 1, 1, 0); x := (2, 1, 3);
     A:= (0, 1, 1, 1, 0); x := (2, 3, 1);
     A:= (1, 0, 0, 2, 0); x := (3, 3, 0);
     A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
     A:= (0, 2, 0, 0, 1); x := (4, 1, 1);
     A:= (1, 0, 1, 0, 1); x := (4, 2, 0);
     A:= (0, 1, 1, 1, 0); x := (3, 2, 1);
     A:= (1, 0, 1, 0, 1); x := (0, 2, 4);
     A:= (0, 1, 1, 1, 0); x := (1, 2, 3);
     A:= (1, 0, 1, 0, 1); x := (0, 4, 2);
     A:= (0, 1, 1, 1, 0); x := (1, 3, 2);
     A:= (0, 2, 0, 0, 1); x := (1, 4, 1);
     A:= (1, 0, 0, 2, 0); x := (0, 3, 3);
     A:= (0, 2, 0, 0, 1); x := (1, 1, 4);
     A:= (1, 0, 0, 2, 0); x := (3, 0, 3);
     A:= (0, 1, 1, 1, 0); x := (3, 1, 2);

Try All Possible Assignments:
        x := (0, 0, 0) is unsat!
        x := (0, 0, 1) is unsat!
        x := (0, 0, 2) is unsat!
        x := (0, 0, 3) is unsat!
        x := (0, 0, 4) is unsat!
        x := (0, 1, 0) is unsat!
        x := (0, 1, 1) is unsat!
        x := (0, 1, 2) is unsat!
        x := (0, 1, 3) is unsat!
        x := (0, 1, 4) is unsat!
        x := (0, 2, 0) is unsat!
        x := (0, 2, 1) is unsat!
        x := (0, 2, 2) is unsat!
        x := (0, 2, 3) is unsat!
     A:= (1, 0, 1, 0, 1); x := (0, 2, 4);
        x := (0, 3, 0) is unsat!
        x := (0, 3, 1) is unsat!
        x := (0, 3, 2) is unsat!
     A:= (1, 0, 0, 2, 0); x := (0, 3, 3);
        x := (0, 3, 4) is unsat!
        x := (0, 4, 0) is unsat!
        x := (0, 4, 1) is unsat!
     A:= (1, 0, 1, 0, 1); x := (0, 4, 2);
        x := (0, 4, 3) is unsat!
        x := (0, 4, 4) is unsat!
        x := (1, 0, 0) is unsat!
        x := (1, 0, 1) is unsat!
        x := (1, 0, 2) is unsat!
        x := (1, 0, 3) is unsat!
        x := (1, 0, 4) is unsat!
        x := (1, 1, 0) is unsat!
        x := (1, 1, 1) is unsat!
        x := (1, 1, 2) is unsat!
        x := (1, 1, 3) is unsat!
     A:= (0, 2, 0, 0, 1); x := (1, 1, 4);
        x := (1, 2, 0) is unsat!
        x := (1, 2, 1) is unsat!
        x := (1, 2, 2) is unsat!
     A:= (0, 1, 1, 1, 0); x := (1, 2, 3);
        x := (1, 2, 4) is unsat!
        x := (1, 3, 0) is unsat!
        x := (1, 3, 1) is unsat!
     A:= (0, 1, 1, 1, 0); x := (1, 3, 2);
        x := (1, 3, 3) is unsat!
        x := (1, 3, 4) is unsat!
        x := (1, 4, 0) is unsat!
     A:= (0, 2, 0, 0, 1); x := (1, 4, 1);
        x := (1, 4, 2) is unsat!
        x := (1, 4, 3) is unsat!
        x := (1, 4, 4) is unsat!
        x := (2, 0, 0) is unsat!
        x := (2, 0, 1) is unsat!
        x := (2, 0, 2) is unsat!
        x := (2, 0, 3) is unsat!
     A:= (1, 0, 1, 0, 1); x := (2, 0, 4);
        x := (2, 1, 0) is unsat!
        x := (2, 1, 1) is unsat!
        x := (2, 1, 2) is unsat!
     A:= (0, 1, 1, 1, 0); x := (2, 1, 3);
        x := (2, 1, 4) is unsat!
        x := (2, 2, 0) is unsat!
        x := (2, 2, 1) is unsat!
        x := (2, 2, 2) is unsat!
        x := (2, 2, 3) is unsat!
        x := (2, 2, 4) is unsat!
        x := (2, 3, 0) is unsat!
     A:= (0, 1, 1, 1, 0); x := (2, 3, 1);
        x := (2, 3, 2) is unsat!
        x := (2, 3, 3) is unsat!
        x := (2, 3, 4) is unsat!
     A:= (1, 0, 1, 0, 1); x := (2, 4, 0);
        x := (2, 4, 1) is unsat!
        x := (2, 4, 2) is unsat!
        x := (2, 4, 3) is unsat!
        x := (2, 4, 4) is unsat!
        x := (3, 0, 0) is unsat!
        x := (3, 0, 1) is unsat!
        x := (3, 0, 2) is unsat!
     A:= (1, 0, 0, 2, 0); x := (3, 0, 3);
        x := (3, 0, 4) is unsat!
        x := (3, 1, 0) is unsat!
        x := (3, 1, 1) is unsat!
     A:= (0, 1, 1, 1, 0); x := (3, 1, 2);
        x := (3, 1, 3) is unsat!
        x := (3, 1, 4) is unsat!
        x := (3, 2, 0) is unsat!
     A:= (0, 1, 1, 1, 0); x := (3, 2, 1);
        x := (3, 2, 2) is unsat!
        x := (3, 2, 3) is unsat!
        x := (3, 2, 4) is unsat!
     A:= (1, 0, 0, 2, 0); x := (3, 3, 0);
        x := (3, 3, 1) is unsat!
        x := (3, 3, 2) is unsat!
        x := (3, 3, 3) is unsat!
        x := (3, 3, 4) is unsat!
        x := (3, 4, 0) is unsat!
        x := (3, 4, 1) is unsat!
        x := (3, 4, 2) is unsat!
        x := (3, 4, 3) is unsat!
        x := (3, 4, 4) is unsat!
        x := (4, 0, 0) is unsat!
        x := (4, 0, 1) is unsat!
     A:= (1, 0, 1, 0, 1); x := (4, 0, 2);
        x := (4, 0, 3) is unsat!
        x := (4, 0, 4) is unsat!
        x := (4, 1, 0) is unsat!
     A:= (0, 2, 0, 0, 1); x := (4, 1, 1);
        x := (4, 1, 2) is unsat!
        x := (4, 1, 3) is unsat!
        x := (4, 1, 4) is unsat!
     A:= (1, 0, 1, 0, 1); x := (4, 2, 0);
        x := (4, 2, 1) is unsat!
        x := (4, 2, 2) is unsat!
        x := (4, 2, 3) is unsat!
        x := (4, 2, 4) is unsat!
        x := (4, 3, 0) is unsat!
        x := (4, 3, 1) is unsat!
        x := (4, 3, 2) is unsat!
        x := (4, 3, 3) is unsat!
        x := (4, 3, 4) is unsat!
        x := (4, 4, 0) is unsat!
        x := (4, 4, 1) is unsat!
        x := (4, 4, 2) is unsat!
        x := (4, 4, 3) is unsat!
        x := (4, 4, 4) is unsat!

MiniZin c + z3:

Я также хочу поделиться этим подходом, потому что мне потребовалось буквально всего 5 минут , чтобы решить эту проблему в MiniZin c, намного меньше, чем с z3py.

[ Примечание: для этой задачи я использую сценарий fzn2z3.py из проекта fzn2omt .]

Файл counter.mzn: (общая структура проблемы)

include "globals.mzn";

% PARAMETERS

set of int: DOMAIN_A;
set of int: INDEX_SET_A;

set of int: DOMAIN_X = INDEX_SET_A;
set of int: INDEX_SET_X;

% VARIABLES

array [INDEX_SET_A] of var DOMAIN_A: A;
array [INDEX_SET_X] of var DOMAIN_X: x;

% CONSTRAINTS

constraint sum(x) == 6;
constraint forall(i in INDEX_SET_A) (
    A[i] = sum(j in INDEX_SET_X)(x[j] == i)
);

% SYMMETRY BREAKING CONTRAINT
constraint increasing(x);

solve satisfy;

( Примечание: У меня есть включил ограничение нарушение симметрии для этой проблемы, чтобы уменьшить количество решений, напечатанных ниже.)

File counter.dzn: (instance-specifici c data )

DOMAIN_A = 0..2;
INDEX_SET_A = 0..4;

INDEX_SET_X = 1..3;

Найдите одно решение с помощью z3:

~$ mzn2fzn counter.mzn counter.dzn
~$ fzn2z3.py counter.fzn 
x = array1d(1..3, [1, 1, 4]);
A = array1d(0..4, [0, 2, 0, 0, 1]);
----------

Найдите все возможные решения (только с optimathsat):

~$ mzn2fzn counter.mzn counter.dzn
~$ fzn2optimathsat.py --all-solutions counter.fzn
% allsat model
x = array1d(1..3, [1, 1, 4]);
A = array1d(0..4, [0, 2, 0, 0, 1]);
----------
% allsat model
x = array1d(1..3, [0, 2, 4]);
A = array1d(0..4, [1, 0, 1, 0, 1]);
----------
% allsat model
x = array1d(1..3, [0, 3, 3]);
A = array1d(0..4, [1, 0, 0, 2, 0]);
----------
% allsat model
x = array1d(1..3, [1, 2, 3]);
A = array1d(0..4, [0, 1, 1, 1, 0]);
----------
==========

Массив переменных счетчика Z3 в Python

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Массив переменных счетчика Z3 в Python

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Похожие темы