Considere que temos 3 gabinetes e queremos distribuir 4 pessoas (Ana=1, Nuno=2, Pedro=3 e Maria=4) por esses gabinetes.

Considere ainda que foram estipuladas as seguintes regras de ocupação dos gabinetes:

1. Cada pessoa ocupa um único gabinete.
2. O Nuno e o Pedro não podem partilhar gabinete.
3. Se a Ana ficar sozinha num gabinete, então o Pedro também terá que ficar sozinho num gabinete.
4. Cada gabinete só pode acomodar, no máximo, 2 pessoas.

Pretende-se que escreva um programa Python que, usando o Z3 como SAT solver, faça a distribuição das pessoas pelos gabinetes.

Começe por instalar o Z3.

!pip install z3-solver

Para resolver o problema em Lógica Proposicional temos que

1. Declarar um conjunto de variáveis Boolenas 𝑥𝑝,𝑔 com a seguinte semântica:

   𝑥𝑝,𝑔 é verdade  sse a pessoa  𝑝 ocupa o gabinete 𝑔

2. De seguida, teremos que modelar cada uma das restrições, acrescentando as fórmulas lógicas correspondentes.

3. Finalmente testamos se o conjunto de restrições é satisfazível e extraimos a solução calculada.

from z3 import *

pessoas = ["Ana","Nuno","Pedro","Maria"]
gabs = [1,2,3]
x = {}
for p in pessoas:
    x[p] = {}
    for g in gabs:
        x[p][g] = Bool("%s,%d" % (p,g))

s = Solver()

# A melhor maneira para se fazer, é dividir a restrição "Cada pessoa ocupa um único gabinete." em duas:

	# 1) Cada pessoa ocupa pelo menos um gabinete.
	for p in pessoas:
	  s.add(Or([x[p][g] for g in gabs]))
	
	# 2) Cada pessoa ocupa no máximo um gabinete.
	for p in pessoas:
	  s.add(Implies(x[p][1], And(Not(x[p][2]),Not(x[p][3])) ))
	  s.add(Implies(x[p][2]),Not(x[p][3]))
	
		# OU DESTA MANEIRA
	for p in pessoas:
		for g in range[1,3]:
			s.add(Implies(x[p][g], And(Not (x[p][h]) for h in range(g+1,4)))) 

# O Nuno e o Pedro não podem partilhar gabinete.
for g in gabs:
  s.add(Implies(x["Pedro"][g], Not(x["Nuno"][g])))

# Se a Ana ficar sozinha num gabinete, então o Pedro também terá que ficar sozinho num gabinete.
anaSo = Or([ And(x["Ana"][g],Not(x["Pedro"][g]),
                 Not(x["Maria"][g]),Not(x["Nuno"][g]))  for g in gabs])

pedroSo = Or([ And(x["Pedro"][g],Not(x["Ana"][g]),
                 Not(x["Maria"][g]),Not(x["Nuno"][g]))  for g in gabs])

s.add(Implies(anaSo,pedroSo))

# Cada gabinete só pode acomodar, no máximo, 2 pessoas.
comb = [("Ana","Nuno","Pedro","Maria"),("Ana","Pedro","Nuno","Maria"),
        ("Ana","Maria","Nuno","Pedro"),("Nuno","Pedro","Ana","Maria"),
        ("Nuno","Maria","Ana","Pedro"),("Pedro","Maria","Nuno","Ana")]
for g in gabs:
  s.add(And([Implies(And(x[p1][g],x[p2][g]), And(Not(x[p3][g]),Not(x[p4][g])))
                for (p1,p2,p3,p4) in comb]))

s.push()

if s.check() == sat:
    m = s.model()
    for p in pessoas:
        for g in gabs:
            if is_true(m[x[p][g]]):
                print("%s fica no gabinete %s" % (p,g))
else:
  print("Não tem solução.")

Será que há várias alternativas para distribuir os gabinetes seguindo estas regras? Faça as alterações necessárias ao programa de modo a saber todas as distribuições possíveis.

s.push()
i=0

while s.check() == sat:
    i+=1
    m = s.model()
    f=[]
    for p in pessoas:
        for g in gabs:
            if is_true(m[x[p][g]]):
                print("%s fica no gabinete %s" % (p,g))
                f.append(Not(x[p][g]))
            else:
                f.append(x[p][g])
     s.add(Or(f)) # Guardamos, para usa-lo como restrição para que não se volte a encontrar a mesma solução
else:
  print("Não tem solução.")

Colab:

Google Colaboratory