Practicum 2

In de 2e practicumopgave bouwen we voort op de eerste. De opgave bestaat uit verschillende delen. Deze pagina beschrijft het 1e deel. Opnieuw gaan we een vertex cover probleem oplossen; deze keer gaan we echter gebruik maken van CP solvers en SAT solvers, in plaats van zelf depth-first search te implementeren. Hieronder worden de verschillende stappen beschreven die je dient te nemen.

Downloaden en installeren solvers

We gaan gebruik maken van een Python interface naar verschillende solvers, genaamd Numberjack.

Volg hiertoe de volgende stappen op de machines van het LIACS.

  1. Download de interface hier
  2. Unzip het gedownloade bestand
  3. Ga de folder in en type make local_install
  4. De laatste regels zien er ongeveer zo uit:
    Remember to add the following lines to your .profile or .bashrc:
    export PYTHONPATH=~/Numberjack-master/local_lib:$PYTHONPATH
    export PATH=~/Numberjack-master/local_lib:$PATH
    then run "source ~/.profile" or "source ~/.bashrc"

    De precieze paden zijn afhankelijk van de plaats waar je het ZIP bestand hebt uitgepakt. Neem de juiste paden inderdaad in je .bashrc bestand op.

  5. Probeer een voorbeeld programma in te typen en uit te voeren: 
    from Numberjack import *
import Mistral

a,b,c = (Variable() for val in range(3))
model = Model( [ ( ( a == True ) | ( b == True ) ) , ( a==False ) , ( c==True ), Minimise(a+b+c)] ) 
solver = model.load('Mistral')

print solver.solve()
print solver.printStatistics()
print a,b,c

    Wat doet dit programma?

Op een MacOS machine kun je de volgende instructies volgen:

  1. Download Numberjack van de homepage
  2. Installeer homebrew met het volgende commando:

    ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
    homebrew doctor
    homebrew install

  3. Installeer SWIG en libxml2:
    brew install swig
    brew install libxml2
  4. Installeer Numberjack met:
    python setup.py build
    sudo python ./setup.py install

Constraint Programming

Het doel van het eerste deel van de opgave is simpel: implementeer dezelfde taak als van het eerste practicum door gebruik te maken de Mistral CP solver die opgenomen is in Numberjack. Je dient hiertoe het probleem te definieren door gebruik te maken van constraints opgenomen in Numberjack. Tip: bekijk ook de voorbeelden en de documentatie van Numberjack.

Evalueer je code op niet al te grote grafen die je willekeurig genereert door middel van de generator die je in de eerste opgave gemaakt hebt.

SAT solving

Numberjack ondersteunt de MiniSAT SAT solver. Pas het Mistral model aan zodanig dat je alleen CNF constraints gebruikt; pas MiniSAT op dit model toe, gebruikmakend van dezelfde voorbeelden als die je voor Mistral gebruikte. Welke van de methoden is sneller?

De belangrijkste technische uitdaging in deze opgave is dat een SAT solver geen ingebouwde ondersteuning kent voor het tellen van het aantal variabelen dat de waarde true aanneemt, of om een minimalisatieprobleem op te lossen. Je kunt echter via een omweg toch minimalisatieproblemen oplossen. Dit is een voorbeeld van zo'n omweg:

  • los herhaaldelijk het volgende constraint satisfaction probleem op: is er een vertex cover van grootte maximaal n? Start hierbij met de kleinst mogelijke waarde van n en hoog n telkens met 1 op.
  • het volgende voorbeeld illustreert hoe je kunt afdwingen dat maximaal 3 van 4 variabelen p1, ..., p4 true zijn:

    p1 → q11 ∨ q12 ∨ q13
    p2 → q21 ∨ q22 ∨ q23
    p3 → q31 ∨ q32 ∨ q33
    p4 → q41 ∨ q42 ∨ q43
    ¬ q11 ∨ ¬ q21
    ¬ q11 ∨ ¬ q31
    ¬ q11 ∨ ¬ q41
    ¬ q21 ∨ ¬ q31
    ...
    ¬ q33 ∨ ¬ q43

Merk op 1: Numberjack staat ook het gebruik toe van andere constraints dan CNF constraints in combinatie met MiniSAT. Numberjack vertaalt deze constraints dan zelf in CNF constraints. Het is niet de bedoeling dat deze automatische omzetting in deze opgave gebruikt wordt.

Merk op 2: De omzetting hierboven vraagt een groot aantal paarsgewijze constraints. Er zijn formaliseringen denkbaar die minder constraints vragen. In het college is een methode besproken die minder ruimte vraagt.

Instructies

Houd er bij de uitwerking rekening mee dat ook de leesbaarheid van je code beoordeeld zal worden: het is belangrijk dat je commentaar opneemt, waar nuttig, en namen voor je variabelen kiest die informatief zijn. Functies moeten overzichtelijk zijn en niet te lang.