From 324fb51fe3e30941581b8cec692c1cf4a0f255c7 Mon Sep 17 00:00:00 2001
From: Lars Tveito <larstvei@ifi.uio.no>
Date: Tue, 19 Nov 2019 20:11:28 +0100
Subject: [PATCH] Update examples

---
 committees.org | 89 +++++++++++++++++++++++++++++++-------------------
 1 file changed, 56 insertions(+), 33 deletions(-)

diff --git a/committees.org b/committees.org
index 121aa52..7cd6095 100644
--- a/committees.org
+++ b/committees.org
@@ -54,7 +54,9 @@ cry for help.
   $\mathcal{M}$ such that $\mathcal{M} \models \phi$. In general, this is an
   undecidable problem. However, there are theories within first order logic
   that are decidable. SMT solvers can produce models that satisfy a set of
-  formulas for many useful theories, some of which are satisfiable.
+  formulas for many useful theories, some of which are satisfiable. It is
+  natural to think of SMT as a generalization of SAT, which is satisfiability
+  for propositional logic.
 
   The solver we will be using is [[https://github.com/Z3Prover/z3][Z3]].
 
@@ -159,8 +161,8 @@ cry for help.
    - $P_{Int} = \{<, =\}$ where the predicate symbols $<, =$ has type signature
      $Int \times Int$.
 
-   In Z3, the type signature function- and predicate symbols informs Z3 of what
-   theory it should apply.
+   In Z3, the type signature of function- and predicate symbols informs Z3 of
+   what theory it should apply.
 
 * Back to the problem
 
@@ -318,20 +320,20 @@ cry for help.
    Calling ~check_instance(example_instance())~ returns a model:
 
    #+BEGIN_EXAMPLE
-   [frozenset({0, 1}) = 83,
-    frozenset({0, 2}) = 47,
-    frozenset({0, 5}) = 30,
-    frozenset({2, 3}) = 0,
-    frozenset({1, 2}) = 3,
-    frozenset({1, 3}) = 60,
-    frozenset({2, 5}) = 0,
-    frozenset({1, 5}) = 0,
-    frozenset({2, 4}) = 60,
-    frozenset({4, 5}) = 0,
-    frozenset({0, 4}) = 0,
+   [frozenset({0, 1}) = 150,
+    frozenset({0, 2}) = 10,
+    frozenset({2, 3}) = 56,
+    frozenset({1, 3}) = 0,
+    frozenset({2, 5}) = 7,
     frozenset({3, 5}) = 0,
-    frozenset({3, 4}) = 0,
+    frozenset({0, 5}) = 0,
+    frozenset({1, 2}) = 0,
+    frozenset({4, 5}) = 23,
+    frozenset({1, 5}) = 0,
     frozenset({0, 3}) = 0,
+    frozenset({0, 4}) = 0,
+    frozenset({2, 4}) = 37,
+    frozenset({3, 4}) = 0,
     frozenset({1, 4}) = 0]
    #+END_EXAMPLE
 
@@ -355,12 +357,19 @@ cry for help.
    This outputs the something like:
 
    #+BEGIN_EXAMPLE
-   {0, 1}: 23
-   {0, 2}: 110
-   {0, 5}: 23
-   {1, 3}: 60
-   {1, 5}: 7
-   {1, 4}: 60
+   0: 160/160
+   1: 150/150
+   2: 110/110
+   3: 56/60
+   4: 60/60
+   5: 30/30
+
+   0, 1: 150
+   0, 2: 10
+   2, 3: 56
+   2, 4: 37
+   2, 5: 7
+   4, 5: 23
    #+END_EXAMPLE
 
    Note the /something like/. There are multiple ways to satisfy this set of
@@ -410,12 +419,19 @@ cry for help.
    example).
 
    #+BEGIN_EXAMPLE
-   {2, 3}: 56
-   {0, 1}: 137
-   {2, 5}: 7
-   {0, 5}: 23
-   {2, 4}: 47
-   {1, 4}: 13
+   0: 160/160
+   1: 150/150
+   2: 110/110
+   3: 60/60
+   4: 60/60
+   5: 26/30
+
+   0, 1: 137
+   0, 5: 23
+   1, 4: 13
+   2, 3: 60
+   2, 4: 47
+   2, 5: 3
    #+END_EXAMPLE
 
 ** Dealing with /should/
@@ -459,12 +475,19 @@ cry for help.
    #+END_SRC
 
    #+BEGIN_EXAMPLE
-   {0, 2}: 50
-   {1, 3}: 60
-   {1, 5}: 7
-   {2, 4}: 60
-   {0, 5}: 23
-   {0, 1}: 83
+   0: 160/160
+   1: 150/150
+   2: 106/110
+   3: 60/60
+   4: 60/60
+   5: 30/30
+
+   0, 1: 87
+   0, 2: 43
+   0, 5: 30
+   1, 2: 3
+   1, 3: 60
+   2, 4: 60
    #+END_EXAMPLE
 
 ** Optimize for capacities