Computerpracticum Logische Structuren 11-12

Op het computerpracticum oefenen we met de SAT-solver SAT4J.
Het vindt plaats in de computerzalen S-101 (groep A) en P-323 (groep B),
woensdag 7 en 14 december, 15:30 - 17:15
Let op: gewijzigde tijd!

De resultaten van het practicum moeten electronisch worden ingeleverd om mee te tellen voor de bonus. Nadere instructies volgen.

Satisfiability problemen kunnen worden opgelost met de SAT-solver Sat4J.
Dat kan op twee manieren:

• Via clauses in het standaard cnf-format, dat direct kan worden gebruikt als invoer voor Sat4J. Via de command line geef je het volgende commando:

  java -jar sat4j.jar input.txt

  Hier is input.txt een pure tekstfile, volgens het standaard cnf-format, zoals in de voorbeeldfile roof1-cnf.txt.
  
  
• Met formules van de propositielogica in prefix-format, via de automatische formulevertaler, met commando:

  java -cp main.jar my.FormulaReader input.txt

  Of in een Windows-omgeving het kortere:

  start.bat input.txt

  Nu bevat input.txt de formules in prefixnotatie zoals in de voorbeeldfile roof1.txt.

Van beide methoden zijn verschillende voorbeelden gegeven tijdens het college. Alle files (en ook de satsolver Sat4J) zitten in de zip van sat, die je kunt downloaden. Je kunt die voorbeelden allemaal nog eens bekijken en proberen. Om de vertaler te gebruiken moet je het commando geven vanuit de directory vertaler.

Je kunt ook gebruikmaken van de

Webinterface voor de satsolver

In het verleden waren er op sommige computers in de practicumzalen problemen met de satsolver. Daarom hebben we een webinterface gemaakt voor Sat4J en de formulevertaler op onze eigen server:

http://infinity.few.vu.nl/ls

Dit biedt een platformonafhankelijke manier om de opdrachten te maken en zelf de voorbeelden te proberen.

Het gebruik spreekt voor zich. Je kunt je invoer in het invoerscherm pasten, op start drukken, en dan vind je de uitvoer in het uitvoerscherm (naar beneden scrollen). In het drop-down menu staan de invoerfiles van de practicumopdrachten en ook de voorbeelden van het college. Je kunt hier mee experimenteren door er zelf in te editen.

Vooraf
Experimenteer met de voorbeeldfiles van het college (ook in het menu van de web interface). Je kunt ze vrijelijk bewerken, de originalen blijven bewaard.

Dan nu de practicumopdrachten
Probeer deze week tot opdracht 5 of 6 te komen.
Voor volgende week kan er nog iets bijkomen

Los de volgende satisfiability problemen op met Sat4J. Gebruik de formulevertaler, tenzij expliciet wordt gevraagd wordt om het cnf-format.

1. Satisfiability (consistentie) van de verzameling van vier formules:

   {(p -> q) -> -r, r v s, s -> (-p v q), r -> p}

   Doe dit op de twee aangegeven manieren: in het cnf-format en via de formulevertaler.
   
   
2. Los opgave 1.51(b) uit Mendelson p 29 op met Sat4J.
   Doe ook deze opgave zowel in het cnf-format als via de formulevertaler.
   
   
3. Bepaal m.b.v. Sat4J van de volgende twee formules of ze een tautologie, een contradictie of een contingentie zijn:
   • [1]: ((p -> (p & q) /\ -q)) -> -p
   • [2]: (-p /\ (p -> q)) -> q
   
   
4. Hoe kun je via satsolving de geldigheid van een semantische implicatie bepalen?
   Pas dit toe in de volgende twee gevallen:
   • [1]: (p -> q) -> p |= p ?
   • [2]: p -> r, q v -r |= -(q /\ -p) ?
   
   
5. Op het eiland van leugenaars en waarheidssprekers worden drie inwoners, a, b  en c, ondervraagd:

   • eilandbewoner a  zegt: "we zijn alledrie leugenaars."
   • eilandbewoner b  zegt: "precies één van ons drieën is een waarheidsspreker"

   Bepaal van elk van a, b  en c  of ze waarheidspreker dan wel leugenaar zijn.

   NB:
   - Geef eerst de gegevens aan de satsolver, om een oplossing te bepalen.
   - test vervolgens met de satsolver of de gevonden oplossing uniek is.
   

6. The case of McGregor's Shop (uit het werkcollege van deze week)
   
   
7. Het kleuren van een landkaart met de landen Nederland, België, Luxemburg, Duitsland met drie kleuren (aangrenzende landen moeten verschillend gekleurd worden)
   
   
8. Het optellen van een 2- en een 1-bits binair getal, in het bijzonder 10 en 1.
   Gebruik in deze opgave naar keuze het cnf-format of de formulevertaler.

   NB: de voorbereide inputfile is voor cnf, pas die zelf aan als je de formulevertaler gebruikt.
   [De filenaam is foutievelijk opdracht7_INPUT_8.txt dat zou 8 moeten zijn]

Inleveren van de opdrachten

Lever de opdrachten in door de bijbehorende inputfiles uit het dropdownmenu van de webinterface te

1. completeren
2. runnen
3. desgevraagd van commentaar voorzien
4. saven
5. samenvoegen in een zip bestand
6. NB: samenvoegen in een enkele tekstfile of word document mag bij nader inzien ook
7. mailen naar tcs@cs.vu.nl, met als subject "ls practicum sat"

Zorg dat de gesavede files goed runnen. Controleer dit door ze een voor een in het iputvenster van de webinterface te pasten en te testen.

Deadline inleveren practicumopdrachten: vrijdag 16 december, 13:00 uur

uitwerkingen computeropdracht (gezipt)