larstvei/SMT-for-IN3070
1
0
Fork 0
mirror of https://github.com/larstvei/SMT-for-IN3070.git synced 2024-11-26 03:28:31 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Update examples

Browse Source
This commit is contained in:
Lars Tveito 2019-11-19 20:11:28 +01:00
parent fb82ad5467
commit 324fb51fe3
1 changed files with 56 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

89
committees.org
View File

@ -54,7 +54,9 @@ cry for help.
$\mathcal{M}$ such that $\mathcal{M} \models \phi$. In general, this is an $\mathcal{M}$ such that $\mathcal{M} \models \phi$. In general, this is an
undecidable problem. However, there are theories within first order logic undecidable problem. However, there are theories within first order logic
that are decidable. SMT solvers can produce models that satisfy a set of 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]]. 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 - $P_{Int} = \{<, =\}$ where the predicate symbols $<, =$ has type signature
$Int \times Int$. $Int \times Int$.
In Z3, the type signature function- and predicate symbols informs Z3 of what In Z3, the type signature of function- and predicate symbols informs Z3 of
theory it should apply. what theory it should apply.
* Back to the problem * Back to the problem
@ -318,20 +320,20 @@ cry for help.
Calling ~check_instance(example_instance())~ returns a model: Calling ~check_instance(example_instance())~ returns a model:
#+BEGIN_EXAMPLE #+BEGIN_EXAMPLE
[frozenset({0, 1}) = 83, [frozenset({0, 1}) = 150,
frozenset({0, 2}) = 47, frozenset({0, 2}) = 10,
frozenset({0, 5}) = 30, frozenset({2, 3}) = 56,
frozenset({2, 3}) = 0, frozenset({1, 3}) = 0,
frozenset({1, 2}) = 3, frozenset({2, 5}) = 7,
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({3, 5}) = 0, 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, 3}) = 0,
frozenset({0, 4}) = 0,
frozenset({2, 4}) = 37,
frozenset({3, 4}) = 0,
frozenset({1, 4}) = 0] frozenset({1, 4}) = 0]
#+END_EXAMPLE #+END_EXAMPLE
@ -355,12 +357,19 @@ cry for help.
This outputs the something like: This outputs the something like:
#+BEGIN_EXAMPLE #+BEGIN_EXAMPLE
{0, 1}: 23 0: 160/160
{0, 2}: 110 1: 150/150
{0, 5}: 23 2: 110/110
{1, 3}: 60 3: 56/60
{1, 5}: 7 4: 60/60
{1, 4}: 60 5: 30/30
0, 1: 150
0, 2: 10
2, 3: 56
2, 4: 37
2, 5: 7
4, 5: 23
#+END_EXAMPLE #+END_EXAMPLE
Note the /something like/. There are multiple ways to satisfy this set of Note the /something like/. There are multiple ways to satisfy this set of
@ -410,12 +419,19 @@ cry for help.
example). example).
#+BEGIN_EXAMPLE #+BEGIN_EXAMPLE
{2, 3}: 56 0: 160/160
{0, 1}: 137 1: 150/150
{2, 5}: 7 2: 110/110
{0, 5}: 23 3: 60/60
{2, 4}: 47 4: 60/60
{1, 4}: 13 5: 26/30
0, 1: 137
0, 5: 23
1, 4: 13
2, 3: 60
2, 4: 47
2, 5: 3
#+END_EXAMPLE #+END_EXAMPLE
** Dealing with /should/ ** Dealing with /should/
@ -459,12 +475,19 @@ cry for help.
#+END_SRC #+END_SRC
#+BEGIN_EXAMPLE #+BEGIN_EXAMPLE
{0, 2}: 50 0: 160/160
{1, 3}: 60 1: 150/150
{1, 5}: 7 2: 106/110
{2, 4}: 60 3: 60/60
{0, 5}: 23 4: 60/60
{0, 1}: 83 5: 30/30
0, 1: 87
0, 2: 43
0, 5: 30
1, 2: 3
1, 3: 60
2, 4: 60
#+END_EXAMPLE #+END_EXAMPLE
** Optimize for capacities ** Optimize for capacities