added skeleton files

branchless_min.py

@@ -0,0 +1,19 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# Create an instance of a z3 solver
+solver = Solver()
+# Declare z3 variables for the needed BitVectors
+
+min_ite = BitVec(...)
+
+solver.add(min_ite == If(x < y, x, y))
+
+
+
+# Check and print the result.
+result = solver.check()
+print(result)
+if result == sat:
+    print(solver.model())

burglars.py

@@ -0,0 +1,31 @@
+# coding: utf-8
+from z3 import *
+
+################################# Burglars ##################################
+# create the solver
+solver = Solver()
+
+#############################################################################
+# (1) Ed: "Fred did it, and Ted is innocent".
+# (2) Fred: "If Ed is guilty , then so is Ted".
+# (3) Ted: "Im innocent, but at least one of the others is guilty".
+#############################################################################
+
+# TODO Create boolean variables for each of the culprits
+# TODO Add constraints to the solver representing the statements from above
+
+# Hint: The statement of a culprit should be true if and only if he is not guilty!
+
+
+
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+print(solver)
+m = solver.model()
+for d in m.decls():
+    print("%s -> %s" % (d, m[d]))
+
+print("\n" + str(m))

rpssl.py

@@ -0,0 +1,123 @@
+# coding: utf-8
+import os, sys, subprocess
+import time
+from z3 import *
+
+CHOICES = ["Rock", "Paper", "Scissors", "Spock", "Lizard"]
+
+def next_random_number(s_i):
+    return ((11 * s_i) + 12345) & 0x7fff
+
+class RPSSLComputer:
+    def __init__(self, s0):
+        self.previous_random_number = s0
+
+    def compute_choice(self):
+        random_number = next_random_number(self.previous_random_number)
+        self.previous_random_number = random_number
+        return random_number % 5, CHOICES[random_number % 5]
+
+
+# cf. https://bigbangtheory.fandom.com/wiki/Rock,_Paper,_Scissors,_Lizard,_Spock
+def winning_mapping(i):
+    if i == 0: return 1#"Paper"
+    if i == 1: return 2#"Scissors"
+    if i == 2: return 0#"Rock"
+    if i == 3: return 4#"Lizard"
+    if i == 4: return 0#"Rock"
+    return "Did you forget to compute the remainder modulo 5?"
+
+def compute_winner(computer, player):
+    if computer == player:
+        return "\tTie.", False
+    is_player_bigger = True if player > computer else False
+    absolute_difference = abs(computer - player)
+    if absolute_difference % 2 == 1:
+        if is_player_bigger:
+            return "\tPlayer wins.", True
+        else:
+            return "\tComputer wins.", False
+    else:
+        if is_player_bigger:
+            return "\tComputer wins.", False
+        else:
+            return "\tPlayer wins.", True
+
+solver = Solver()
+states = list()
+
+# We are adding the first state s_0 to the list of states
+states.append(BitVec("state0", 16))
+
+s0 = int(sys.argv[1])
+computer = RPSSLComputer(s0)
+
+preprocess_count = 5
+
+def add_constraint(solver, index, computers_choice):
+    # TODO create a BitVec and append it to the list of states
+    # You might want to call it state{index}
+
+    # TODO Enforce that the newly added BitVec-variable must evaluate to the result of the LCG computation using the previous result
+
+    # TODO Enforce that the unsigned remainder of the newly added BitVec-varialbe and 5 evaluates to the choice of the computer
+
+    pass
+
+def store_backtracking_point(solver):
+    solver.push()
+
+def restore_backtracking_point(solver):
+    solver.pop()
+
+def add_next_state_constraint(solver):
+    s_i_plus_1 = BitVec("s_i_plus_1", 16)
+    # TODO Enforce that the next state value is computed via the same computation as above
+
+    return s_i_plus_1
+
+def get_players_choice(solver, s_i_plus_1):
+    # TODO Get the value of next_state from the model and return it modulo 5
+    # Hint: winning_mapping(...) returns a good answer for the computer's choice
+    # Hint: use solver.model() like a python dict.
+    # Hint: use `.as_long()` to convert a z3 variable to a python integer value
+    return 0
+
+
+# Main loop:
+
+# We read preprocess_count many choices from the computer before we start to ask z3 for a solution
+# Note that for these preprocessing rounds we do not need to make a good guess and compute the winner
+# We are only interested in what the computer picks for the first few rounds
+for index in range(1,preprocess_count):
+    computer_choice, _ = computer.compute_choice()
+    player_choice = 0 # We always choose Rock since we cannot make good guesses in the beginning
+
+    add_constraint(solver,index,computer_choice)
+    output, won = compute_winner(computer_choice, player_choice)
+    print(output)
+    if won: print("Congratulations!")
+    else:   print("Try again.")
+
+
+# Now we start by adding a 'special' variable s_i_plus_1 and try to win
+index = preprocess_count
+while True:
+    store_backtracking_point(solver)
+    s_i_plus_1 = add_next_state_constraint(solver)
+    solver.check()
+
+    player_choice = get_players_choice(solver, s_i_plus_1)
+    computer_choice, _ = computer.compute_choice()
+    output, won = compute_winner(computer_choice, player_choice)
+
+    print(output)
+    if won: print("Congratulations!")
+    else:   print("Try again.")
+
+    restore_backtracking_point(solver)
+    add_constraint(solver, index, computer_choice)
+    # input("")
+    index += 1
+    if index >= 100:
+        break

seating-arrangement.py

@@ -0,0 +1,146 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+from itertools import combinations
+
+pretty_print = True
+
+# get the playground information
+if len(sys.argv) != 2:
+    print("Usage: python3 seating-arrangement.py <wedding-file>")
+    sys.exit(0)
+
+def faulty_line(line, num):
+    print("Faulty input at line " + str(num) + ". Ignoring '" + line + "'")
+
+# data structures prepared for you
+guests = set()
+friends = []
+foes = []
+longest_name_len = 0
+
+def add_to_guest_list(a,b=None):
+    guests.add(a)
+    if b != None:
+        guests.add(b)
+
+def longest_name(a,b=None):
+    global longest_name_len
+    if len(a) > longest_name_len: longest_name_len = len(a)
+    if b != None and len(b) > longest_name_len : longest_name_len = len(b)
+
+solver = Solver()
+
+################################### Parse Guests and Constraints ####################################
+
+Guest = DeclareSort("Guest")
+
+with open(sys.argv[1]) as f:
+    wedding = f.read()
+    wedding = wedding.strip().split("\n")
+    linenum = 0
+    for line in wedding:
+        linenum += 1
+        if line[0] == '#':
+            continue
+        if line.rstrip():
+            info = line.split(" ")
+
+            if len(info) == 1:
+                guest = Const(info[0], Guest)
+                add_to_guest_list()
+                longest_name(info[0])
+                continue
+
+            if len(info) != 3:
+                faulty_line(line, linenum)
+                continue
+
+            longest_name(info[0], info[2])
+            if info[1] == "dislikes":
+                first_guest = Const(info[0], Guest)
+                second_guest = Const(info[2], Guest)
+                add_to_guest_list(first_guest, second_guest)
+                # TODO add the pair of guests as foes
+            elif info[1] == "likes":
+                first_guest = Const(info[0], Guest)
+                second_guest = Const(info[2], Guest)
+                add_to_guest_list(first_guest, second_guest)
+                # TODO add pair of guests as friends
+            else:
+                faulty_line(line, linenum)
+                continue
+
+################################### Wedding Guests ####################################
+
+
+def neigbours(a, b):
+    pass
+
+# all guests must be seated at the big table
+# no two guests should sit on the same position (hint: use combinations)
+# friends should be neigbours
+# foes should not be neigbours
+
+# check satisfiability
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+m = solver.model()
+
+################################################################################
+
+
+arrangement = ["" for guest in range(len(guests))]
+for guest in guests:
+    arrangement[m.evaluate(position(guest),model_completion=True).as_long()] = guest.decl().name()
+
+def print_table():
+    side_length = round(len(guests)/4)
+    top    = arrangement[0:side_length]
+    right  = arrangement[side_length:2*side_length]
+    bottom = arrangement[2*side_length:3*side_length]
+    left   = arrangement[3*side_length:]
+    while len(left) < len(right):
+        left.append("")
+    while len(right) < len(left):
+        right.append("")
+    table_line_length = longest_name_len + 1
+
+    print("\n")
+
+    top_row = ""
+    top_row += (longest_name_len + 1) * " "
+    for top_guest in top:
+        top_row += top_guest + " "
+        table_line_length += len(top_guest) + 1
+    print(top_row)
+    print((longest_name_len + 1) * " " + table_line_length * "-")
+
+    first_element = True
+    for left_guest, right_guest in zip(reversed(left), right):
+        row = ""
+        if not first_element:
+            row += longest_name_len * " "
+            row += "|" + ">"* (table_line_length) + "|"
+            print(row)
+            row = ""
+        else:
+            first_element = False
+        row += left_guest.rjust(longest_name_len) + "|" + "<"* (table_line_length) + "|" + right_guest
+        print(row)
+
+    print((longest_name_len + 1) * " " + table_line_length * "-")
+    bottom_row = ""
+    bottom_row += (longest_name_len + 1) * " "
+    for bottom_guest in reversed(bottom):
+        bottom_row += bottom_guest + " "
+    print(bottom_row)
+    print("\n")
+
+if(pretty_print):
+    print_table()
+print("Seating plan:")
+print(arrangement)

square.py

@@ -0,0 +1,53 @@
+# coding: utf-8
+import os, sys
+from z3 import *
+
+# get the playground information
+if len(sys.argv) != 2:
+    print("Usage: python3 square.py <test-file>")
+    sys.exit(0)
+
+with open(sys.argv[1]) as f:
+    playground = f.read()
+rows = playground.strip().split("\n")
+playground = [[None if x == "_" else int(x) for x in r.split()] for r in rows]
+
+# get the playground size
+size_y = len(playground)
+assert(size_y != 0)
+size_x = len(playground[0])
+assert(size_x != 0)
+assert(size_x == size_y)
+
+#################################### Square ####################################
+
+# create the solver
+solver = Solver()
+
+numbers = [[None for _j in range(size_x)] for _j in range(size_y)]
+
+# TODO: create an integer variable for each playground cell
+# hint: use something like the coordinates as part of the variable name
+# TODO: assign each known number the corresponding value from playground
+# TODO: declare a variable for the sum of all columns, rows and diagonals
+# TODO: enforce that each column sums up to the declared variable
+# TODO: enforce that each row sums up to the declared variable
+# TODO enforce that both diagonals sum up to the declared variable
+
+
+# call the solver and check satisfiability
+res = solver.check()
+if res != sat:
+    print("unsat")
+    sys.exit(1)
+
+# print the model
+m = solver.model()
+for i in range(size_y):
+    results = []
+    for j in range(size_x):
+        num = numbers[i][j]
+        results.append("_" if num is None else m[num].as_long())
+    print(("%4s" * len(results)) % tuple(results))
+
+################################################################################

square0.txt

@@ -0,0 +1,3 @@
+_ _ 28
+_ 35 21
+_ 7 _

wedding-25s.txt

@@ -0,0 +1,628 @@
+Amanda dislikes Tamara
+William dislikes Heather
+Christopher dislikes Barbara
+Dorothy dislikes Evan
+Elizabeth dislikes Thomas
+Thomas dislikes Barbara
+Douglas dislikes Jason
+Destiny dislikes Barbara
+Mallory dislikes Tamara
+Alexandra dislikes Kristen
+Pedro dislikes Adam
+Tyler dislikes Heather
+Barbara dislikes Dorothy
+Tamara dislikes Elizabeth
+Benjamin dislikes Jason
+Mark dislikes Kristen
+Patrick dislikes Pedro
+Jacqueline dislikes Michelle
+Heather dislikes Mallory
+Susan dislikes Elizabeth
+Amanda dislikes Linda
+William dislikes Brenda
+Christopher dislikes Barbara
+Elizabeth dislikes Pedro
+Timothy dislikes Miranda
+Thomas dislikes Destiny
+Douglas dislikes Miranda
+Destiny dislikes Mark
+Miranda dislikes Pedro
+Mallory dislikes Thomas
+Jason dislikes Susan
+Alexandra dislikes Mallory
+Pedro dislikes Dorothy
+Tyler dislikes Tamara
+Barbara dislikes William
+Tamara dislikes Kristen
+Benjamin dislikes Pedro
+Mark dislikes Tamara
+Patrick dislikes Mallory
+Jacqueline dislikes Susan
+Heather dislikes Christopher
+Susan dislikes Alexandra
+Amanda dislikes Benjamin
+Christopher dislikes Tamara
+Dorothy dislikes Brenda
+Elizabeth dislikes Patrick
+Timothy dislikes Mallory
+Douglas dislikes Barbara
+Destiny dislikes Christopher
+Miranda dislikes Heather
+Mallory dislikes Kristen
+Jason dislikes Linda
+Alexandra dislikes Mark
+Tyler dislikes Kristen
+Barbara dislikes Dorothy
+Tamara dislikes Michelle
+Mark dislikes Jacqueline
+Patrick dislikes Christopher
+Jacqueline dislikes Benjamin
+Susan dislikes Brenda
+Amanda dislikes Brenda
+William dislikes Mallory
+Dorothy dislikes Thomas
+Elizabeth dislikes Miranda
+Thomas dislikes Tyler
+Douglas dislikes Michelle
+Destiny dislikes Linda
+Miranda dislikes Thomas
+Mallory dislikes Elizabeth
+Jason dislikes William
+Alexandra dislikes Timothy
+Pedro dislikes Jason
+Tyler dislikes Patrick
+Barbara dislikes Heather
+Tamara dislikes Mark
+Benjamin dislikes Christopher
+Mark dislikes Timothy
+Patrick dislikes Thomas
+Jacqueline dislikes Douglas
+Heather dislikes Elizabeth
+Susan dislikes Benjamin
+Amanda dislikes Timothy
+William dislikes Dorothy
+Christopher dislikes Douglas
+Dorothy dislikes Jason
+Elizabeth dislikes Thomas
+Timothy dislikes Tyler
+Douglas dislikes Pedro
+Destiny dislikes Christopher
+Miranda dislikes Adam
+Mallory dislikes Benjamin
+Jason dislikes Mark
+Alexandra dislikes Patrick
+Pedro dislikes William
+Tyler dislikes Dorothy
+Barbara dislikes Christopher
+Tamara dislikes Mallory
+Benjamin dislikes Timothy
+Mark dislikes Douglas
+Jacqueline dislikes Benjamin
+Heather dislikes Thomas
+Susan dislikes Christopher
+Amanda dislikes Pedro
+William dislikes Patrick
+Christopher dislikes Kristen
+Dorothy dislikes Brenda
+Elizabeth dislikes Mallory
+Timothy dislikes Destiny
+Thomas dislikes Evan
+Douglas dislikes Linda
+Destiny dislikes Mallory
+Miranda dislikes Michelle
+Mallory dislikes Douglas
+Jason dislikes Benjamin
+Alexandra dislikes Mallory
+Pedro dislikes Elizabeth
+Tyler dislikes Adam
+Barbara dislikes Kristen
+Tamara dislikes Adam
+Benjamin dislikes Mallory
+Mark dislikes Linda
+Patrick dislikes Tamara
+Jacqueline dislikes Tamara
+Heather dislikes Tyler
+Susan dislikes Linda
+Amanda dislikes Miranda
+William dislikes Heather
+Christopher dislikes Mark
+Elizabeth dislikes Barbara
+Timothy dislikes Mark
+Douglas dislikes Susan
+Destiny dislikes Alexandra
+Miranda dislikes Barbara
+Mallory dislikes Heather
+Jason dislikes Kristen
+Alexandra dislikes Dorothy
+Pedro dislikes Mark
+Tyler dislikes Heather
+Barbara dislikes Pedro
+Tamara dislikes William
+Benjamin dislikes Heather
+Mark dislikes William
+Patrick dislikes Brenda
+Jacqueline dislikes Elizabeth
+Heather dislikes Michelle
+Amanda dislikes Tamara
+William dislikes Brenda
+Christopher dislikes Jason
+Dorothy dislikes Alexandra
+Elizabeth dislikes Susan
+Timothy dislikes Christopher
+Thomas dislikes Tyler
+Douglas dislikes Mark
+Destiny dislikes Jacqueline
+Miranda dislikes Jason
+Mallory dislikes Timothy
+Jason dislikes Kristen
+Alexandra dislikes Susan
+Pedro dislikes Michelle
+Tyler dislikes Benjamin
+Barbara dislikes Pedro
+Benjamin dislikes William
+Mark dislikes Douglas
+Patrick dislikes Christopher
+Jacqueline dislikes Thomas
+Susan dislikes Tyler
+William dislikes Thomas
+Christopher dislikes Michelle
+Dorothy dislikes Alexandra
+Elizabeth dislikes Jacqueline
+Timothy dislikes Adam
+Thomas dislikes Susan
+Douglas dislikes Christopher
+Destiny dislikes Brenda
+Mallory dislikes Jacqueline
+Jason dislikes Dorothy
+Alexandra dislikes Adam
+Pedro dislikes Evan
+Tyler dislikes Alexandra
+Barbara dislikes Mark
+Tamara dislikes Mark
+Benjamin dislikes Tyler
+Mark dislikes Tamara
+Patrick dislikes Adam
+Jacqueline dislikes Adam
+Susan dislikes Miranda
+Amanda dislikes Christopher
+William dislikes Linda
+Christopher dislikes Linda
+Dorothy dislikes Miranda
+Elizabeth dislikes Jacqueline
+Timothy dislikes Brenda
+Thomas dislikes Elizabeth
+Douglas dislikes William
+Miranda dislikes Christopher
+Mallory dislikes Thomas
+Jason dislikes Destiny
+Alexandra dislikes Tamara
+Pedro dislikes Douglas
+Tyler dislikes Thomas
+Barbara dislikes Linda
+Tamara dislikes Brenda
+Benjamin dislikes Evan
+Patrick dislikes Linda
+Heather dislikes Mallory
+Susan dislikes William
+Amanda dislikes Michelle
+William dislikes Barbara
+Christopher dislikes Barbara
+Elizabeth dislikes Miranda
+Timothy dislikes Barbara
+Douglas dislikes Michelle
+Destiny dislikes Brenda
+Mallory dislikes Patrick
+Jason dislikes William
+Alexandra dislikes Brenda
+Pedro dislikes Tamara
+Tyler dislikes Elizabeth
+Barbara dislikes Mallory
+Tamara dislikes Linda
+Benjamin dislikes Brenda
+Mark dislikes Douglas
+Patrick dislikes Barbara
+Jacqueline dislikes Michelle
+Heather dislikes Mark
+Susan dislikes Dorothy
+Amanda dislikes Mark
+William dislikes Dorothy
+Christopher dislikes Mallory
+Dorothy dislikes Mark
+Elizabeth dislikes Tyler
+Timothy dislikes Michelle
+Thomas dislikes Mallory
+Douglas dislikes Timothy
+Destiny dislikes Susan
+Miranda dislikes Christopher
+Jason dislikes William
+Alexandra dislikes Evan
+Pedro dislikes Evan
+Barbara dislikes Thomas
+Tamara dislikes Thomas
+Benjamin dislikes Elizabeth
+Mark dislikes Barbara
+Patrick dislikes Heather
+Jacqueline dislikes Kristen
+Heather dislikes Thomas
+Susan dislikes Tyler
+Amanda dislikes Benjamin
+William dislikes Michelle
+Christopher dislikes Heather
+Dorothy dislikes Timothy
+Elizabeth dislikes Kristen
+Timothy dislikes Benjamin
+Thomas dislikes Linda
+Douglas dislikes Mallory
+Destiny dislikes Jason
+Miranda dislikes Kristen
+Jason dislikes Michelle
+Pedro dislikes Destiny
+Barbara dislikes Susan
+Tamara dislikes Elizabeth
+Benjamin dislikes Mallory
+Mark dislikes Dorothy
+Patrick dislikes Michelle
+Jacqueline dislikes Susan
+Heather dislikes Douglas
+Susan dislikes Barbara
+Amanda dislikes Alexandra
+William dislikes Miranda
+Christopher dislikes Heather
+Dorothy dislikes Jason
+Elizabeth dislikes Adam
+Timothy dislikes Evan
+Douglas dislikes Linda
+Destiny dislikes Susan
+Miranda dislikes Tyler
+Mallory dislikes Pedro
+Jason dislikes Mark
+Alexandra dislikes Brenda
+Pedro dislikes Kristen
+Tyler dislikes Mark
+Barbara dislikes Christopher
+Tamara dislikes Heather
+Benjamin dislikes Pedro
+Mark dislikes William
+Patrick dislikes Tamara
+Jacqueline dislikes Michelle
+Heather dislikes Mallory
+Susan dislikes Benjamin
+William dislikes Linda
+Christopher dislikes Heather
+Timothy dislikes Mallory
+Thomas dislikes Adam
+Douglas dislikes Kristen
+Destiny dislikes Timothy
+Miranda dislikes Jason
+Mallory dislikes Tamara
+Jason dislikes Tamara
+Alexandra dislikes Heather
+Pedro dislikes Jason
+Tyler dislikes Jacqueline
+Barbara dislikes Benjamin
+Tamara dislikes William
+Benjamin dislikes Miranda
+Mark dislikes Alexandra
+Patrick dislikes Mallory
+Jacqueline dislikes Tamara
+Heather dislikes Pedro
+Susan dislikes Patrick
+Amanda dislikes Christopher
+Christopher dislikes Tyler
+Dorothy dislikes Michelle
+Elizabeth dislikes Mark
+Timothy dislikes Brenda
+Thomas dislikes Barbara
+Douglas dislikes Evan
+Destiny dislikes Mark
+Miranda dislikes Tamara
+Jason dislikes Benjamin
+Alexandra dislikes Michelle
+Pedro dislikes Destiny
+Tyler dislikes Kristen
+Barbara dislikes Dorothy
+Tamara dislikes Alexandra
+Benjamin dislikes Miranda
+Mark dislikes William
+Patrick dislikes Adam
+Jacqueline dislikes Kristen
+Heather dislikes Mark
+Susan dislikes Patrick
+Amanda dislikes Alexandra
+William dislikes Pedro
+Christopher dislikes Douglas
+Dorothy dislikes Tyler
+Timothy dislikes Susan
+Thomas dislikes Tamara
+Douglas dislikes Mark
+Destiny dislikes Mallory
+Miranda dislikes Mark
+Mallory dislikes Pedro
+Alexandra dislikes Dorothy
+Pedro dislikes William
+Tyler dislikes Jacqueline
+Barbara dislikes Elizabeth
+Benjamin dislikes Thomas
+Mark dislikes Adam
+Patrick dislikes Tyler
+Heather dislikes Tyler
+Susan dislikes Barbara
+Amanda dislikes Miranda
+William dislikes Evan
+Christopher dislikes Alexandra
+Dorothy dislikes Tyler
+Elizabeth dislikes Mallory
+Timothy dislikes Dorothy
+Thomas dislikes Mark
+Douglas dislikes Kristen
+Destiny dislikes Mark
+Miranda dislikes Heather
+Jason dislikes Jacqueline
+Alexandra dislikes Heather
+Pedro dislikes Brenda
+Tyler dislikes Mallory
+Barbara dislikes Christopher
+Tamara dislikes Jacqueline
+Mark dislikes Dorothy
+Patrick dislikes Kristen
+Jacqueline dislikes Michelle
+Heather dislikes William
+Susan dislikes Patrick
+Amanda dislikes Brenda
+William dislikes Evan
+Christopher dislikes Mark
+Dorothy dislikes Barbara
+Elizabeth dislikes Heather
+Timothy dislikes Adam
+Thomas dislikes Destiny
+Douglas dislikes Mark
+Destiny dislikes Kristen
+Mallory dislikes Pedro
+Jason dislikes Susan
+Alexandra dislikes Dorothy
+Pedro dislikes Barbara
+Tyler dislikes Heather
+Barbara dislikes Miranda
+Tamara dislikes Evan
+Benjamin dislikes Miranda
+Mark dislikes Michelle
+Jacqueline dislikes William
+Heather dislikes Timothy
+Susan dislikes Tyler
+Amanda dislikes Linda
+William dislikes Mallory
+Christopher dislikes Adam
+Dorothy dislikes Miranda
+Timothy dislikes William
+Thomas dislikes Barbara
+Destiny dislikes Pedro
+Mallory dislikes Kristen
+Alexandra dislikes Timothy
+Pedro dislikes Evan
+Tyler dislikes Timothy
+Barbara dislikes Linda
+Tamara dislikes Mallory
+Benjamin dislikes Evan
+Mark dislikes Tyler
+Patrick dislikes Thomas
+Jacqueline dislikes Dorothy
+Heather dislikes Timothy
+Susan dislikes Pedro
+Amanda dislikes Evan
+William dislikes Jason
+Christopher dislikes Michelle
+Dorothy dislikes Barbara
+Elizabeth dislikes Michelle
+Timothy dislikes Pedro
+Thomas dislikes Adam
+Douglas dislikes Pedro
+Destiny dislikes Jason
+Miranda dislikes Adam
+Mallory dislikes Michelle
+Jason dislikes Christopher
+Alexandra dislikes Jacqueline
+Tyler dislikes Mallory
+Barbara dislikes Pedro
+Tamara dislikes Adam
+Benjamin dislikes Tyler
+Patrick dislikes Thomas
+Jacqueline dislikes William
+Heather dislikes Michelle
+Susan dislikes Thomas
+Amanda dislikes Miranda
+William dislikes Tamara
+Christopher dislikes Linda
+Dorothy dislikes Susan
+Elizabeth dislikes Kristen
+Timothy dislikes Douglas
+Thomas dislikes Christopher
+Douglas dislikes Evan
+Destiny dislikes Thomas
+Miranda dislikes Tamara
+Mallory dislikes Alexandra
+Alexandra dislikes Elizabeth
+Tyler dislikes Heather
+Barbara dislikes Adam
+Tamara dislikes Kristen
+Benjamin dislikes Kristen
+Mark dislikes Pedro
+Patrick dislikes Elizabeth
+Jacqueline dislikes Destiny
+Heather dislikes William
+Susan dislikes Adam
+Amanda dislikes Dorothy
+William dislikes Brenda
+Christopher dislikes Kristen
+Dorothy dislikes Susan
+Elizabeth dislikes Miranda
+Timothy dislikes Jacqueline
+Thomas dislikes Mallory
+Douglas dislikes Tyler
+Destiny dislikes Dorothy
+Miranda dislikes William
+Mallory dislikes Heather
+Jason dislikes Patrick
+Alexandra dislikes Mark
+Pedro dislikes Douglas
+Barbara dislikes Timothy
+Tamara dislikes Mallory
+Benjamin dislikes Patrick
+Mark dislikes Brenda
+Patrick dislikes Linda
+Jacqueline dislikes Susan
+Heather dislikes Tyler
+Susan dislikes Michelle
+Amanda dislikes Evan
+William dislikes Mallory
+Christopher dislikes Evan
+Dorothy dislikes Patrick
+Elizabeth dislikes Barbara
+Timothy dislikes William
+Thomas dislikes Miranda
+Destiny dislikes Mark
+Miranda dislikes Alexandra
+Mallory dislikes Pedro
+Jason dislikes William
+Alexandra dislikes Mark
+Pedro dislikes Susan
+Barbara dislikes Thomas
+Tamara dislikes William
+Benjamin dislikes Jason
+Mark dislikes Susan
+Patrick dislikes Miranda
+Jacqueline dislikes Evan
+Heather dislikes Mallory
+Susan dislikes Dorothy
+Amanda dislikes Evan
+William dislikes Barbara
+Christopher dislikes Barbara
+Dorothy dislikes Mark
+Elizabeth dislikes Mark
+Timothy dislikes William
+Thomas dislikes Linda
+Destiny dislikes Mark
+Miranda dislikes Kristen
+Mallory dislikes William
+Jason dislikes Brenda
+Alexandra dislikes Miranda
+Pedro dislikes Linda
+Tyler dislikes Thomas
+Tamara dislikes Christopher
+Benjamin dislikes Miranda
+Mark dislikes Christopher
+Patrick dislikes Michelle
+Jacqueline dislikes Tyler
+Heather dislikes Tyler
+Amanda dislikes Alexandra
+William dislikes Mallory
+Christopher dislikes Alexandra
+Dorothy dislikes Pedro
+Elizabeth dislikes Mallory
+Timothy dislikes Evan
+Thomas dislikes Dorothy
+Douglas dislikes Heather
+Destiny dislikes Dorothy
+Miranda dislikes Pedro
+Mallory dislikes Timothy
+Jason dislikes William
+Alexandra dislikes Elizabeth
+Pedro dislikes Patrick
+Tyler dislikes Heather
+Barbara dislikes William
+Benjamin dislikes Mallory
+Mark dislikes Tamara
+Heather dislikes Benjamin
+Susan dislikes Douglas
+Amanda dislikes Tamara
+William dislikes Mark
+Christopher dislikes Miranda
+Dorothy dislikes Pedro
+Elizabeth dislikes Barbara
+Timothy dislikes Tyler
+Thomas dislikes Pedro
+Douglas dislikes Barbara
+Destiny dislikes Heather
+Miranda dislikes Barbara
+Mallory dislikes Dorothy
+Jason dislikes Barbara
+Alexandra dislikes Brenda
+Pedro dislikes Mallory
+Tyler dislikes Destiny
+Barbara dislikes Mallory
+Tamara dislikes Jacqueline
+Benjamin dislikes Pedro
+Mark dislikes Michelle
+Patrick dislikes Kristen
+Jacqueline dislikes Thomas
+Heather dislikes Brenda
+Susan dislikes Timothy
+Amanda dislikes Kristen
+William dislikes Linda
+Christopher dislikes Alexandra
+Timothy dislikes Barbara
+Thomas dislikes Linda
+Douglas dislikes Jason
+Destiny dislikes Benjamin
+Miranda dislikes Susan
+Mallory dislikes Linda
+Alexandra dislikes Susan
+Pedro dislikes Susan
+Tyler dislikes Tamara
+Barbara dislikes Timothy
+Mark dislikes Thomas
+Patrick dislikes William
+Heather dislikes Benjamin
+Susan dislikes Evan
+Amanda dislikes Barbara
+William dislikes Kristen
+Christopher dislikes Mark
+Dorothy dislikes William
+Elizabeth dislikes Heather
+Timothy dislikes Alexandra
+Thomas dislikes Benjamin
+Douglas dislikes Barbara
+Destiny dislikes William
+Mallory dislikes Adam
+Jason dislikes Christopher
+Alexandra dislikes Kristen
+Pedro dislikes Michelle
+Tyler dislikes William
+Barbara dislikes Michelle
+Tamara dislikes Destiny
+Benjamin dislikes Linda
+Mark dislikes Linda
+Patrick dislikes Miranda
+Heather dislikes Brenda
+Susan dislikes Christopher
+Amanda dislikes Jason
+William dislikes Dorothy
+Christopher dislikes Mallory
+Dorothy dislikes Alexandra
+Elizabeth dislikes Patrick
+Timothy dislikes Pedro
+Thomas dislikes Mallory
+Douglas dislikes Michelle
+Destiny dislikes Mallory
+Mallory dislikes Tyler
+Jason dislikes Douglas
+Alexandra dislikes Michelle
+Pedro dislikes Adam
+Tyler dislikes Evan
+Barbara dislikes Jason
+Tamara dislikes Alexandra
+Benjamin dislikes Alexandra
+Mark dislikes Evan
+Patrick dislikes Alexandra
+Jacqueline dislikes Dorothy
+Heather dislikes Jason
+Susan dislikes William
+Christopher likes Dorothy
+Mallory likes Jason
+Mallory likes Jason
+Elizabeth likes Timothy
+Jacqueline likes Heather
+Evan likes Linda
+Miranda likes Mallory
+Thomas likes Douglas
+Destiny likes Miranda
+Kristen likes Brenda

wedding0.txt

@@ -0,0 +1,11 @@
+Patric dislikes Ada
+Patric dislikes Katie
+Patric dislikes Bob
+Ada
+John likes Alice
+Bob likes Andrea
+Andrea
+Alice
+Ada likes Julia
+Ada likes Katie
+Robert