Implémenter un superoptimiseur pour l'ajout

La tâche consiste à écrire du code qui peut trouver de petites formules logiques pour des sommes de bits.

Le défi global est que votre code trouve la plus petite formule logique propositionnelle possible pour vérifier si la somme de y variables binaires 0/1 est égale à une valeur x. Appelons les variables x1, x2, x3, x4 etc. Votre expression doit être équivalente à la somme. Autrement dit, la formule logique devrait être vraie si et seulement si la somme est égale à x.

Voici une façon naïve de le faire pour commencer. Dites y = 15 et x = 5. Choisissez les 3003 façons différentes de choisir 5 variables et faites pour chacune une nouvelle clause avec le ET de ces variables ET le ET de la négation des variables restantes. Vous vous retrouvez avec 3003 clauses chacune de longueur exactement 15 pour un coût total de 45054.

Votre réponse devrait être une expression logique de ce type qui peut simplement être collée en python, par exemple, afin que je puisse la tester. Si deux personnes obtiennent la même expression de taille, le code qui exécute le plus rapidement l'emporte.

Vous ÊTES autorisé à introduire de nouvelles variables dans votre solution. Donc, dans ce cas, votre formule logique se compose des y variables binaires, x et de quelques nouvelles variables. La formule entière serait satisfiable si et seulement si la somme des variables y était égale à x.

Comme exercice de départ, certaines personnes peuvent vouloir commencer par y = 5 variables en ajoutant à x = 2. La méthode naïve donnera alors un coût de 50.

Le code doit prendre deux valeurs y et x en entrée et afficher la formule et sa taille en sortie. Le coût d'une solution n'est que le nombre brut de variables dans sa sortie. Compte donc (a or b) and (!a or c) comme 4. Les seuls opérateurs autorisés sont and, oret not.

Mise à jour Il s'avère qu'il existe une méthode intelligente pour résoudre ce problème lorsque x = 1, du moins en théorie.

Python, 644

Un simple générateur d'équations récursives. Sgénère une équation satisfaite si la liste des varstotaux s'additionne total.

Il y a des améliorations évidentes à faire. Par exemple, de nombreuses sous-expressions courantes apparaissent dans la sortie 15/5.

def S(vars, total):
    # base case
    if total == 0:
        return "(" + " and ".join("not " + x for x in vars) + ")"
    if total == len(vars):
        return "(" + " and ".join(vars) + ")"

    # recursive case
    n = len(vars)/2
    clauses = []
    for s in xrange(total+1):
        if s > n or total-s > len(vars)-n: continue
        a = S(vars[:n], s)
        b = S(vars[n:], total-s)
        clauses += ["(" + a + " and " + b + ")"]
    return "(" + " or ".join(clauses) + ")"

def T(n, total):
    e = S(["x[%d]"%i for i in xrange(n)], total)
    print "equation", e
    print "score", e.count("[")

    # test it
    for i in xrange(2**n):
        x = [i/2**k%2 for k in xrange(n)]
        if eval(e) != (sum(x) == total):
            print "wrong", x

T(2, 1)
T(5, 2)
T(15, 5)

Génère:

equation (((not x[0]) and (x[1])) or ((x[0]) and (not x[1])))
score 4
equation (((not x[0] and not x[1]) and (((not x[2]) and (x[3] and x[4])) or ((x[2]) and (((not x[3]) and (x[4])) or ((x[3]) and (not x[4])))))) or ((((not x[0]) and (x[1])) or ((x[0]) and (not x[1]))) and (((not x[2]) and (((not x[3]) and (x[4])) or ((x[3]) and (not x[4])))) or ((x[2]) and (not x[3] and not x[4])))) or ((x[0] and x[1]) and (not x[2] and not x[3] and not x[4])))
score 27
equation (((not x[0] and not x[1] and not x[2] and not x[3] and not x[4] and not x[5] and not x[6]) and (((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (x[11] and x[12] and x[13] and x[14])) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (x[13] and x[14])) or ((x[11] and x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))))) or ((((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (x[9] and x[10])) or ((x[7] and x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10]))))) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((x[7] and x[8] and x[9] and x[10]) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))))) or ((((not x[0] and not x[1] and not x[2]) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6])))) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (not x[3] and not x[4] and not x[5] and not x[6]))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (x[11] and x[12] and x[13] and x[14])) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (x[13] and x[14])) or ((x[11] and x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))))) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (x[9] and x[10])) or ((x[7] and x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10]))))) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((x[7] and x[8] and x[9] and x[10]) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((not x[0] and not x[1] and not x[2]) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6])))) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6])))) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (not x[3] and not x[4] and not x[5] and not x[6]))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (x[13] and x[14])) or ((x[11] and x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))))) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (x[9] and x[10])) or ((x[7] and x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10]))))) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((not x[0] and not x[1] and not x[2]) and (((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (x[5] and x[6])) or ((x[3] and x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))))) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6])))) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6])))) or ((x[0] and x[1] and x[2]) and (not x[3] and not x[4] and not x[5] and not x[6]))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((not x[0] and not x[1] and not x[2]) and (x[3] and x[4] and x[5] and x[6])) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (x[5] and x[6])) or ((x[3] and x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))))) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6])))) or ((x[0] and x[1] and x[2]) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6]))))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (x[3] and x[4] and x[5] and x[6])) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (x[5] and x[6])) or ((x[3] and x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))))) or ((x[0] and x[1] and x[2]) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6]))))) and (not x[7] and not x[8] and not x[9] and not x[10] and not x[11] and not x[12] and not x[13] and not x[14])))
score 644

J'aurais fait un commentaire, mais je n'ai pas de réputation. Je voulais faire remarquer que les résultats de Kwon & Klieber (connus sous le nom d'encodage "Commander") pour k = 1 ont été généralisés pour k> = 2 par Frisch et al. "Encodages SAT de la contrainte At-Most-k." Ce que vous demandez, c'est un cas particulier de la contrainte AM-k, avec une clause supplémentaire pour garantir At-Least-k, ce qui est trivial, juste une disjonction de toutes les variables de la contrainte AM-k. Frisch est un chercheur de premier plan dans la modélisation des contraintes, donc je me sentirais à l'aise de suggérer que [(2k + 2 C k + 1) + (2k + 2 C k-1)] * n / 2 est la meilleure limite connue sur le nombre de clauses requises, et k * n / 2 pour le nombre de nouvelles variables à introduire. Les détails sont dans l'article cité, ainsi que les instructions sur la façon dont cet encodage doit être construit. Il' Il est assez simple d'écrire un programme pour générer cette formule, et je pense qu'une telle solution serait compétitive avec toutes les autres solutions que vous trouverez probablement pour l'instant. HTH.