mirror of
https://github.com/larstvei/SMT-for-IN3070.git
synced 2024-11-26 03:28:31 +00:00
Change heading level for introduction
This commit is contained in:
parent
1d4d507a1f
commit
48c20b294e
@ -1,51 +1,50 @@
|
|||||||
|
#+TITLE: SMT for IN3170
|
||||||
#+AUTHOR: Lars Tveito
|
#+AUTHOR: Lars Tveito
|
||||||
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="Rethink/rethink.css" />
|
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="Rethink/rethink.css" />
|
||||||
#+OPTIONS: toc:nil num:nil html-style:nil
|
#+OPTIONS: toc:nil num:nil html-style:nil
|
||||||
|
|
||||||
* Introduction
|
At the Department of Informatics (University of Oslo), all exams are
|
||||||
|
corrected by a committee consisting of two examiners. For large courses,
|
||||||
|
there are often many examiners where some wants to correct more than others.
|
||||||
|
The administration is responsible for forming these committees. Sometimes
|
||||||
|
there are additional constraints on what examiners can form a committee (the
|
||||||
|
typical example being that two examiners are professors and two are master
|
||||||
|
students).
|
||||||
|
|
||||||
At the Department of Informatics (University of Oslo), all exams are
|
Before digitizing exams at the department, the administration would have
|
||||||
corrected by a committee consisting of two examiners. For large courses,
|
physical copies of the exam to distribute. This would actually make it easier
|
||||||
there are often many examiners where some wants to correct more than others.
|
to form the committees, because the constraints could be handled on the fly.
|
||||||
The administration is responsible for forming these committees. Sometimes
|
When digitized, the problem would essentially turn into a math problem which
|
||||||
there are additional constraints on what examiners can form a committee (the
|
is not particularly easy to solve.
|
||||||
typical example being that two examiners are professors and two are master
|
|
||||||
students).
|
|
||||||
|
|
||||||
Before digitizing exams at the department, the administration would have
|
This is an actual email (in Norwegian) forwarded to me from someone in the
|
||||||
physical copies of the exam to distribute. This would actually make it easier
|
administration:
|
||||||
to form the committees, because the constraints could be handled on the fly.
|
|
||||||
When digitized, the problem would essentially turn into a math problem which
|
|
||||||
is not particularly easy to solve.
|
|
||||||
|
|
||||||
This is an actual email (in Norwegian) forwarded to me from someone in the
|
#+BEGIN_QUOTE
|
||||||
administration:
|
Mine mattekunnskaper er tydeligvis fraværende. Jeg klarer ikke finne en
|
||||||
|
fornuftig løsning på dette:
|
||||||
|
|
||||||
#+BEGIN_QUOTE
|
| A: | 160 |
|
||||||
Mine mattekunnskaper er tydeligvis fraværende. Jeg klarer ikke finne en
|
| B: | 150 |
|
||||||
fornuftig løsning på dette:
|
| C: | 110 |
|
||||||
|
| D: | 60 |
|
||||||
|
| E: | 60 |
|
||||||
|
| F: | 30 |
|
||||||
|
|
||||||
| A: | 160 |
|
Det er snakk om sensur i inf1300 med 283 besvarelser. D og E kan ikke rette
|
||||||
| B: | 150 |
|
mot hverandre. De bør helst rette mot B eller C.
|
||||||
| C: | 110 |
|
|
||||||
| D: | 60 |
|
|
||||||
| E: | 60 |
|
|
||||||
| F: | 30 |
|
|
||||||
|
|
||||||
Det er snakk om sensur i inf1300 med 283 besvarelser. D og E kan ikke rette
|
Har du et bra forslag til meg? Jeg blir GAL. Det var bedre før, da jeg hadde
|
||||||
mot hverandre. De bør helst rette mot B eller C.
|
besvarelsene fysisk å kunne telle ark.
|
||||||
|
|
||||||
Har du et bra forslag til meg? Jeg blir GAL. Det var bedre før, da jeg hadde
|
Har du mulighet til å hjelpe en stakkar?
|
||||||
besvarelsene fysisk å kunne telle ark.
|
|
||||||
|
|
||||||
Har du mulighet til å hjelpe en stakkar?
|
Takk
|
||||||
|
#+END_QUOTE
|
||||||
|
|
||||||
Takk
|
Being programmers who have recently heard of this thing called SMT-solving,
|
||||||
#+END_QUOTE
|
we happily research the subject in trying to find a general solution to this
|
||||||
|
cry for help.
|
||||||
Being programmers who have recently heard of this thing called SMT-solving,
|
|
||||||
we happily research the subject in trying to find a general solution to this
|
|
||||||
cry for help.
|
|
||||||
|
|
||||||
* Satisfiability modulo theories (SMT)
|
* Satisfiability modulo theories (SMT)
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user