Asignar elementos a grupos con funciones

Question

Tengo un problema en el que debo asignar variables a conjuntos. Cada conjunto tiene un límite de variables que se le pueden asignar y cada variable se puede asignar a algún subconjunto de los conjuntos totales.

Ejemplo:

• apuede estar en conjuntos AoB
• b puede estar en conjuntos B
• cpuede estar en conjuntos AoB
• d puede estar en conjuntos A

Por lo tanto, podemos tener A: a, d; B: b, co A: c, d; B: a,b(el orden de las variables dentro del conjunto no importa).

Actualmente estoy haciendo lo siguiente usando z3 (escrito usando solve aquí, también se puede representar usando Solver). Por el siguiente código, si a_in_A = Trueentonces la variable aestá en set A.

solve(If(a_in_B, 1, 0) + If(b_in_B, 1, 0) + If(c_in_B, 1, 0) <= 2,
      If(a_in_A, 1, 0) + If(c_in_A, 1, 0) + If(d_in_A, 1, 0) <= 2, 
      If(a_in_A, 1, 0) + If(a_in_B, 1, 0) == 1, 
      If(b_in_B, 1, 0) == 1, 
      If(c_in_A, 1, 0) + If(c_in_B, 1, 0) == 1, 
      If(d_in_A, 1, 0) == 1)

Puedo ponderar las variables dentro del conjunto, como a continuación. En este caso, nos quedaríamos solo A: a, d; B: b, ccomo solución, aunque esto se puede ampliar.

solve(If(a_in_B, 4, 0) + If(b_in_B, 3, 0) + If(c_in_B, 3, 0) <= 6,
      If(a_in_A, 4, 0) + If(c_in_A, 3, 0) + If(d_in_A, 3, 0) <= 7, 
      If(a_in_A, 4, 0) + If(a_in_B, 4, 0) == 4, 
      If(b_in_B, 3, 0) == 3, 
      If(c_in_A, 3, 0) + If(c_in_B, 3, 0) == 3, 
      If(d_in_A, 3, 0) == 3)

Sin embargo, también me gustaría ingresar otras características como cdebe venir en un conjunto después a. Por lo tanto, quedaríamos reducidos solo a la solución de A: a, d; B: b, c. ¿Cómo agregaría estos requisitos a la expresión del solucionador z3 (o de otra manera)?

Answer 1

Como ocurre con cualquier tarea de programación, podría haber muchas formas de resolver este problema. Creo que la siguiente sería la forma más idiomática de hacerlo en z3py. Tenga en cuenta el uso del Settipo interno , que se modela internamente mediante matrices. Elijo números enteros como elementos de los conjuntos, aunque puede hacer que este sea un tipo enumerado (o algún otro tipo base) si lo desea:

from z3 import *

s = Solver()

a, b, c, d = Ints('a b c d')
allElems = [a, b, c, d]
s.add(Distinct(allElems))

# We have 2 sets
A, B = Consts ('A B', SetSort(IntSort()))
allSets = [A, B]

# Generic requirement: Every element belongs to some set:
for e in allElems:
    belongs = False;
    for x in allSets:
        belongs = Or(belongs, IsMember(e, x))
    s.add(belongs)

# Capacity requirements
sizeA, sizeB = Ints('sizeA sizeB')
s.add(SetHasSize(A, sizeA))
s.add(SetHasSize(B, sizeB))
s.add(sizeA <= 2)
s.add(sizeB <= 2)

# Problem specific requirements:
s.add(Or(IsMember(a, A), IsMember(a, B)))
s.add(IsMember(b, B))
s.add(Or(IsMember(c, A), IsMember(c, B)))
s.add(IsMember(d, A))

# c must be in a set that's after a's set
s.add(Implies(IsMember(a, A), IsMember(c, B)))
s.add(Not(IsMember(a, B))) # otherwise there wouldn't be a place to put c!

r = s.check()
if r == sat:
    print(s.model())
else:
    print("Solver said: " + r)

Nótese cómo los requisitos de cardinalidad / capacidad se indican usando sizeA, sizeBvariables. Puede generalizar y escribir sus funciones auxiliares para automatizar la mayoría de estas cosas.

La definición original de su problema era bastante ambigua, pero espero que lo anterior le dé una idea de cómo proceder. En particular, podemos expresar fácilmente el requisito que cpertenece a un conjunto "después" aya que solo tenemos dos conjuntos alrededor:

s.add(Implies(IsMember(a, A), IsMember(c, B)))
s.add(Not(IsMember(a, B))) # otherwise there wouldn't be a place to put c!

pero si tiene más de dos conjuntos, es posible que desee escribir una función auxiliar que recorra los conjuntos (al igual que hice en la parte "Requisito genérico") para automatizar esto también. (Básicamente, diría que si Aestá en un conjunto específico, luego cestá en uno de los conjuntos "posteriores". Cuando llegue al último conjunto, deberá decir aque no está en él, ya que de lo contrario no habría lugar para poner c.)

Cuando ejecuto el programa anterior, imprime:

[A = Lambda(k!0, Or(k!0 == 1, k!0 == 4)),
 b = 5,
 a = 1,
 d = 4,
 sizeB = 2,
 c = 3,
 sizeA = 2,
 B = Lambda(k!0, Or(k!0 == 3, k!0 == 5)),
 Ext = [else -> 5]]

Esto puede ser un poco difícil de leer, ¡pero te acostumbrarás en poco tiempo! Las partes importantes son:

a = 1
b = 5
c = 3
d = 4

Lo anterior debería ser autoexplicativo. Como queríamos representar elementos con números enteros, z3 eligió estos. (Tenga en cuenta que dijimos Distinctque nos aseguremos de que no fueran iguales). Puede usar una ordenación enum aquí si lo desea.

La siguiente parte es la representación de los conjuntos Ay B:

A = Lambda(k!0, Or(k!0 == 1, k!0 == 4)),
B = Lambda(k!0, Or(k!0 == 3, k!0 == 5)),

Lo que esto está diciendo es que Acontiene los elementos 1y 4(es decir, ay d), mientras que Bcontiene los elementos 3y 5(es decir, by c). En su mayoría, puede ignorar la Lambdaparte y el k!0símbolo de aspecto divertido y leerlo de la siguiente manera: Cualquier valor al que 1 OR 4pertenezca A. Y de manera similar para B.

Las variables sizeAy sizeBdeben ser autoexplicativas.

Puede ignorar el Extvalor. Se utiliza para fines internos por z3.

Espero que esto le muestre cómo puede estructurar restricciones aún más complejas de forma declarativa utilizando el soporte integrado para Sets.