International Center for Computational Logic - Benutzerbeiträge [de]

Knowledge Representation and Reasoning Seminar (WS2016)

2017-01-19T07:16:11Z

Peter Steinke:

{{Vorlesung
|Title=Knowledge Representation and Reasoning Seminar
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler; Peter Steinke;
|Term=WS
|Year=2016
|Module=INF-04-HS,INF-AQUA,INF-BAS2,INF-D-940,MCL-KR,MCL-PI,MCL-PCS,EMCL-A-KR,EMCL-PI,EMCL-PCS
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Exam type=mündliche Prüfung, Referat
|Description===Satisfiability Testing (SAT)==

The seminar meetings take place on Mondays, from 16.40 to 18.10 (DS 6) in room E05.
The initial meeting will take place on Monday 17.10. 

This years seminar is all about recent research related to SAT solving.

The student has to select a topic from the ones listed below. He has to study the respective literature.
The students are expected to participate in the seminar, write a short report of the assigned topic, and give a presentation in the end of the summer term.
The presentation should have a length of 30 minutes, followed by a 15 minutes discussion.

German students can give the presentation also in German.

For the students who want to participate at the KRR Seminar it is mandatory to attend '''all''' talks during the term.
The report (five pages) and the slides have to be send one week before the presentation to Peter Steinke.



==Schedule==
* 17.10. initial meeting
* 24.10. Formalization and Certification of Parallel SAT Solvers by Tobias Philipp
* 31.10. Reformationstag (official holiday)
* 7.11. Encoding Pseudo-Boolean Constraints into CNF by Peter Steinke
* 14.11. Response Patterns in the Wason Selection Task and the Special Case of Uncertainty by Emmanuelle Dietz (joint work with Marco Ragni)
* 21.11. Boolean Equation Solving Revisited on the Basis of First-Order Logic in Connection with Interpolation and Second-Order Quantifier Elimination by Christoph Wernhard
* 28.11. Model Counting by Sibylle Möhle
* 05.12. Artificial intelligence outperforms humans in board games by Anna Tigunova
* 12.12. Weak Completion Semantics and Abduction by Steffen Hölldobler
* 19.12. Contextual Abduction by Emmanuelle Dietz
* 09.01. State of the Art Pseudo Boolean Encodings by Peter Steinke
* 16.01. A Formal Framework for #SAT by Sibylle Möhle
* 23.01. Side-effects and Consequences in Contextual Reasoningby Emmanuelle Dietz
}}

Knowledge Representation and Reasoning Seminar (WS2016)

2017-01-13T18:29:13Z

Peter Steinke:

2016-08-31T10:00:45Z

Datei:Weak Completion Semantics 3.pdf

2016-07-27T07:28:56Z

Peter Steinke:

SummerSchool2016/en

2016-07-26T08:26:49Z

Peter Steinke:

{{DISPLAYTITLE:8th South-East Asian Summer School on Computational Logic }}

<center><code> The lecture slides will be online. You can find them under 'lecturers and lectures'.
 </code></center>
 

From July 16 to July 30, 2016, we organize the 8th ICCL summer school. The summer school will be held in in Rayong, Thailand and is supported by the
[http://www.daad.de Gefrman Academic Exchange Service (DAAD)]. The summer school is done in cooperation with the cluster 'semantic technologies' of the Erasmus Mundus Action 2 project [http://www.swap-transfer.eu swap and transfer].

The first summer school has been held 2005 in HUT, Vietnam and the second summer school has been held 2006 in UI Jakarta, Indonesia. The summer schools in 2007 and 2014 have been held in Vietnam and the summer schools in 2008, 2010 and 2012 have been held in Indonesia again.

[[Datei:Group-2.jpg|800px|upright|center|alt=Summer School.|8th South-East Asian Summer School on Computational Logic in Rayong, Thailand]]

The summer school is a platform for knowledge transfer within a very rapid increasing research community in the field of "Computational Logic". We will offer introductory courses covering the fundamentals of reasoning, courses at advanced levels, as well as applied courses and workshops dedicated to specialized topics and the state of the art.

A limited number of scholarships for bachelor, master and phd students will be available!

{{#maketabs:|Info and Venue=

''' Dates '''

* Arrival: 16th of July
* Departure: 30th of July

''' Venue '''

The summer school is held at the [http://rayong.makmai.com/en Makmai Villa Resort].

[[Datei:Beach3.JPG|400px|upright|center|alt=Beach.|Beach.]]



|Lecturers and Lectures=

''' Tableau Calculi and Applications '''
by [http://www.furbach.de/uli/ Prof. rer. nat. habil. Ulrich Furbach] (Universität Koblenz-Landau, Germany)

This course will cover first order tableau calculi with a focus on hyper tableaux. The calculus rules together with a comparison to other logical systems are introduced and an extension for an efficient handling of equality is given. Various applications for a Hyper-tableau-System are discussed and in particular the Loganswer-System [www.loganswer.de www.loganswer.de] as an example of the cognitive computing paradigm is introduced. Based on these applications some extensions and requirements for a proof-system are explained; in particular handling of large knowledge bases (like Cyc), webservices and abductive answers.

''' Abstract Argumentation - Reasoning, Expressiveness and its Connection to Answer Set Programming '''
by [https://ddll.inf.tu-dresden.de/web/Sarah_Alice_Gaggl/en Dr. techn. Sarah Gaggl] (Technische Universität Dresden, Germany)

Argumentation is one of the major fields in Artificial Intelligence (AI) and Non-Monotonic Reasoning (NMR). Nowadays, the concept of abstract Argumentation frameworks (AFs) is one of the most popular approaches to capture certain aspects of argumentation. This very simple yet expressive model has been introduced by Phan Minh Dung in 1995. Arguments and a binary ``attack'' relation between them, denoting conflicts, are the only components one needs for the representation of a wide range of problems and the reasoning therein. Nowadays numerous semantics exist to solve the inherent conflicts between the arguments by selecting sets of ``acceptable'' arguments. Depending on the application, acceptability is defined in different ways. Some semantics are based on the idea to defend arguments against attacks, while others treat arguments like different choices and the solutions stand for consistent sets of arguments. In this course we will first focus on the expressiveness of AFs, in particular we will study if, and under which conditions, a given set of arguments can be accepted at all in an AF under a given semantics. Furthermore, we will analyze different notions of equivalences for AFs, for example when two different AFs posses the same solutions under a semantics, even if we apply modifications to them. Finally we will observe the connection between answer set programming (ASP) and AFs.
* [[Media: slides_sem1.pdf | Introduction to Formal Argumentation I]]
* [[Media: slides_sem2.pdf | Introduction to Formal Argumentation II]]
* [[Media: slides_sem3.pdf | Complexity and Equivalences]]
* [[Media: slides_sem4.pdf | ASP Encodings for AFs]]

 
''' A New Cognitive Theory: Weak Completion Semantics '''
by [https://ddll.inf.tu-dresden.de/web/Steffen_Hölldobler/en Prof. Dr. rer. nat. habil. Steffen Hölldobler], [https://ddll.inf.tu-dresden.de/web/Emmanuelle_Dietz/en Emmanuelle Dietz, MSc] (Technische Universität Dresden, Germany)

In the last 8 years we have developed a new cognitive theory. It is based on the weak completion of logic programs, the three-valued Lukasiewizc logic, abduction and revision, and has been successfully applied to adequately model various human reasoning tasks like the suppression task, the selection task, the belief bias effect, spatial
reasoning as well as reasoning about conditionals. In the course we will give an in-depth introduction into the new theory as well to its applications to different human reasoning tasks. In addition we will do experiments in order to evaluate certain reasoning tasks, in particular, how humans reason with conditionals.

* Lecture 1-4, Introduction to Logic
** [https://iccl.inf.tu-dresden.de/w/images/b/bc/Littlelogic.pdf Introduction to Logic]
** Sudoku Tutorial
*** [https://iccl.inf.tu-dresden.de/w/images/5/58/Sudokus.zip Sudoku Puzzles],
*** [http://tools.computational-logic.org/content/riss.php SAT Solver Riss] or [http://www.labri.fr/perso/lsimon/glucose/#glucose-3.0 SAT Solver Glucose] (how to use it, is written on the bottom of the page)
*** [https://www.cs.ox.ac.uk/joel.ouaknine/publications/sudoku05.pdf Sudoku as a SAT Problem] by Inês Lynce and Joël Ouaknine

* Lecture 5-10, Weak Completion Semantics
** [https://iccl.inf.tu-dresden.de/w/images/9/9b/Humanreasoning.pdf Weak Completion Semantics]
*** [https://iccl.inf.tu-dresden.de/w/images/f/f2/Svloperator.zip SvL Operator]
** [https://iccl.inf.tu-dresden.de/w/images/b/bb/Completion_Semantics_2.pdf Weak Completion Semantics 2]
** Human Reasoning
*** [https://iccl.inf.tu-dresden.de/w/images/7/77/BST.pdf Byrne's Suppression Task]
*** [https://mindmodeling.org/cogsci2012/papers/0266/paper0266.pdf A Computational Logic Approach to the Suppression Task] by Emmanuelle Dietz, Steffen Hölldobler and Marco Ragni
*** [https://iccl.inf.tu-dresden.de/w/images/5/57/Syll.pdf Syllogistic Reasoning]
 

''' Existential Rules '''
by [https://ddll.inf.tu-dresden.de/web/Sebastian_Rudolph/en Prof. Dr. rer. nat. habil. Sebastian Rudolph] (Technische Universität Dresden, Germany)

The course deals with a problem called ontological query answering, which consists in querying data while taking general domain knowledge, encoded in some ontology, into account. The ontology is assumed to be expressed via a set of existential rules (which have been known under many different names like tuple-generating dependencies, Datalog+/-, and forall-exists-rules). As the general problem is undecidable, restrictions need to be imposed to guarantee decidability. Over the last years, a lot of ever more expressive such decidable existential rule fragments have been identified. We will provide an overview of these fragments, relate them to general priciples of decidability, and discuss the different algorithmic approaches to query answering that they give rise to.

* [[Media: slides_er_rayong1.pdf | Existantial Rules I]]

''' Combining Transformational and Logic Programming '''
by [https://www.th-deg.de/en/bwl-wi/contacts/professors/4010-prof-dr-ing-josef-schneeberger-en Prof. Dr.-Ing. habil. Josef Schneeberger] (Fachhochschule Deggendorf, Germany)

XML is a standard for encoding all kinds of information on the Internet and within networked systems. Together with XML, a programming language (XSLT) for transforming XML sources has been developed. XSLT offers an elegant and declarative approach to transform and manipulate arbitrary kinds information. Combining XSLT
transformations with logic programs provides even more expressive power. The course gives an introduction to XSLT, the respective programming model, and application examples. Furthermore, combinations of transformational and logic programs are explored and applied to various application examples.

''' A Relaxed Introduction to Description Logics '''
by [https://ddll.inf.tu-dresden.de/web/Anni-Yasmin_Turhan/en PD Dr.-Ing. habil. Anni Yasmin Turhan] (Technische Universität Dresden, Germany)

In recent years Description Logics (DLs) have gained a lot of attention. On the one hand, DLs have formal semantics, which allow to define a variety of inferences and to prove formal properties such as soundness and correctness or computational complexity of inference procedures for these logics. On the other hand, the ontology language for the web recommended by the W3C, OWL2, is based on Description logics and makes logic-based knowledge representation formalisms available for applications. In this course we will introduce the basic notions of DL concepts and knowledeg bases. We will investigate the standard inferences implemented in most OWL reasoners and also some infernce that allow for relaxed forms of reasoning.

|Registration=

''' Registration '''

The registration for the summer school is open now. You can register online [http://www.computational-logic.org/content/events/iccl-ss-2016/register/general.php?id=0 here].

''' Admission Requirements '''

The summer school is for master and phd students who work in a discipline which is relevant for the summer school. However, excellent bachelor students are also approved.

''' Fees '''

The Participation costs are 480 EUR. This includes accommodation for 12 nights in double-bed rooms, breakfast, lunch, dinner, reception and closing banquette as well as the excursions to the BMW-factory in Rayong and to the island Ko Samed.

The participation costs need to be paid in cash in EUR or THB at the beginning of the summer school during the registration.



''' Scholarships '''

We offer two kinds of scholarships for bachelor, master and phd students: scholarships of 400 EUR (category A) and scholarships of 200 EUR (category B).

The selection will be based on the qualification and the financial needs.

Please indicate in your application if you want to apply for a scholarship and for which one you want to apply.



The deadline for the application for the scholarships is extended until 12.06.2016.

|Timetable=

The registration is prior to the welcome session, on Monday, 18th of July, starting at 8:30.



<h4>First Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  July 17 </th>
<th> Monday 
  July 18 </th>
<th> Tuesday 
  July 19 </th>
<th> Wednesday 
  July 20 </th>
<th> Thursday 
  July 21 </th>
<th> Friday 
  July 22 </th>
<th> Saturday 
  July 23 </th>
</tr>
<tr>
<th>   9:00 - 09:45</th>
<td> </td>
<td> Welcome </td>
<td> Rudolph</td>
<td> Rudolph</td>
<td> Rudolph</td>
<td> Rudolph</td>
<td> </td>
</tr>
<tr>
<th>10:15 - 11:00</th>
<td> </td>
<td> Intro to Logic</td>
<td> Rudolph</td>
<td> Gaggl</td>
<td> Gaggl</td>
<td> Rudolph</td>
<td> Excursion</td>
</tr>
<tr>
<th>11:30 - 12:15</th>
<td> </td>
<td> Intro to Logic</td>
<td> Hölldobler</td>
<td> Gaggl</td>
<td> Gaggl</td>
<td> Dietz</td>
<td> to</td>
</tr>
<tr>
<th>14:00 - 14:45</th>
<td> </td>
<td> Dietz</td>
<td> Hölldobler</td>
<td> Dietz</td>
<td> Excursion</td>
<td> Gaggl</td>
<td> Samed</td>
</tr>
<tr>
<th>15:15 - 16:00</th>
<td> </td>
<td> Dietz</td>
<td> Dietz</td>
<td> Dietz</td>
<td> to BMW</td>
<td> Gaggl</td>
<td> </td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> Reception</td>
<td> </td>
<td> </td>
<td> Dinner</td>
<td> </td>
<td></td>
</tr>
</table>
 

<h4>Second Week</h4>

<table style="text-align: center" border="1">
<tr>
<th> </th>
<th> Sunday 
  July 24 </th>
<th> Monday 
  July 25 </th>
<th> Tuesday 
  July 26 </th>
<th> Wednesday 
  July 27 </th>
<th> Thursday 
  July 28 </th>
<th> Friday 
  July 29 </th>
<th> Saturday 
  July 30 </th>
</tr>
<tr>
<th>   9:00 - 09:45</th>
<td> </td>
<td> Furbach</td>
<td> Furbach</td>
<td> Furbach</td>
<td> Furbach</td>
<td> Furbach</td>
<td> </td>
</tr>
<tr>
<th>10:15 - 11:00</th>
<td> </td>
<td> Furbach</td>
<td> Schneeberger</td>
<td> Schneeberger</td>
<td> Schneeberger</td>
<td> Schneeberger</td>
<td> </td>
</tr>
<tr>
<th>11:30 - 12:15</th>
<td> </td>
<td> Schneeberger</td>
<td> Schneeberger</td>
<td> Turhan</td>
<td> Turhan</td>
<td> Turhan</td>
<td> </td>
</tr>
<tr>
<th>14:00 - 14:45</th>
<td> </td>
<td> Turhan</td>
<td> Turhan</td>
<td> Hölldobler</td>
<td> DAAD</td>
<td> Evaluation</td>
<td> </td>
</tr>
<tr>
<th>15:15 - 16:00</th>
<td> </td>
<td> Turhan</td>
<td> Hölldobler</td>
<td> Study Opport.</td>
<td> DAAD</td>
<td> Farewell</td>
<td> </td>
</tr>
<tr>
<th>Evening</th>
<td> </td>
<td> </td>
<td> </td>
<td> </td>
<td> Dinner</td>
<td> </td>
<td></td>
</tr>
</table>

|Social Program=

* Welcome Reception
* Excursion to the BMW factory in Rayong
* Information about funding opportunities in Germany and about studies in Germany for students from Thailand
* Event about intercultural differences together with alumni from Thailand
* Selected talks from participants and alumni.
* Excursion to Samed
* Evaluation of the summer school together with the lecturers and the participants
* Closing banquet

[[Datei:P1037809.JPG|400px|upright|center|alt=Beach.|Beach.]]

|Stay in Rayong=

'''Accomodation'''

All lecturers and participants will be accommodated at the [http://rayong.makmai.com/en Makmai Villa Resort].

[[Datei:Front_Entrance.jpg|600px|upright|center|alt=Beach.|Beach.]]



|Chairs and Organizers=

'''Chair of the Summer School''' Professor [[Steffen Hölldobler]]

'''Organizers of the Summer School''' Dr. Isara Anantavrasilp from KMITL , Professor Dr. rer. nat. habil. Steffen Hölldobler and Emmanuelle Dietz from ICCL

[[Datei:Beach4.JPG|400px|upright|center|alt=Beach.|Beach.]]

}}

2016-04-27T09:21:56Z

Peter Steinke:

{{Vorlesung
|Title=Knowledge Representation and Reasoning Seminar
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler; Peter Steinke;
|Term=SS
|Year=2016
|Module=INF-04-HS,INF-AQUA,INF-BAS2,INF-D-940,MCL-KR,MCL-PI,MCL-PCS,EMCL-A-KR,EMCL-PI,EMCL-PCS
|SWSLecture=0
|SWSExercise=2
|SWSPractical=0
|Exam type=mündliche Prüfung, Referat
|Description===Satisfiability Testing (SAT)==
This years seminar is all about recent research related to SAT solving.

The student has to select a topic from the ones listed below. He has to study the respective literature.
The students are expected to participate in the seminar, write a short report of the assigned topic, and give a presentation in the end of the summer term.
The presentation should have a length of 30 minutes, followed by a 15 minutes discussion.

German students can give the presentation also in German.

For the students who want to participate at the KRR Seminar it is mandatory to attend '''all''' talks during the term.
The report (five pages) and the slides have to be send one week before the presentation to Peter Steinke.

==Topics==

* [http://rd.springer.com/chapter/10.1007/978-3-319-24318-4_3 Speeding up MUS Extraction with Preprocessing and Chunking]
** Authors: Valeriy Balabanov and Alexander Ivrii
* [http://rd.springer.com/chapter/10.1007%2F978-3-319-24318-4_5 Laissez-Faire Caching for Parallel #SAT Solving]
** Authors: Jan Burchard , Tobias Schubert and Bernd Becker
* [http://rd.springer.com/chapter/10.1007%2F978-3-319-24318-4_10 #∃SAT: Projected Model Counting]
** Authors: Rehan Abdul Aziz, Geoffrey Chu, Christian Muise and Peter Stuckey
* [http://www.iiia.csic.es/~levy/papers/SAT15.pdf Using Community Structure to Detect Relevant Learnt Clauses]
** Authors: Carlos Ans ́otegui, Jes ́us Gir ́aldez-Cru, Jordi Levy and Laurent Simon
* [http://arxiv.org/pdf/1505.02405.pdf Exploiting Resolution-based Representations for MaxSAT Solving]
** Authors: Miguel Neves, Ruben Martins, Mikoláš Janota, Inês Lynce and Vasco Manquinho
* [http://rd.springer.com/chapter/10.1007%2F978-3-319-24318-4_23 Between SAT and UNSAT: The Fundamental Difference in CDCL SAT]
** Author: Chanseok Oh
* [http://rd.springer.com/chapter/10.1007%2F978-3-319-24318-4_28 A New Approach to Partial MUS Enumeration]
** Authors: Christian Zielke and Michael Kaufmann
* [http://fmv.jku.at/papers/BiereFroehlich-SAT15.pdf Evaluating CDCL Variable Scoring Schemes]
** Authors: Armin Biere and Andreas Fröhlich

==Schedule==
The seminar meetings take place on Mondays, from 16.40 to 18.10 (DS 6) in room E05.

* 04.04. initial meeting <strike>and the talk by Ebrahim Zidan on the paper "Abduction for Discourse Interpretation: A Probabilistic Framework" </strike> (only the talk is cancelled)
* 11.04. Christoph Wernhard on "Towards Knowledge-Based Assistance for Scholarly Editing" (joint work with Jana Kittelmann)
* 18.04. Emmanuelle Dietz on "Response Patterns and Selection Sequences in the Wason Selection Task" (joint work with Marco Ragni and Ilir Kola)
* 25.04. Ebrahim Zidan on the paper "Abduction for Discourse Interpretation: A Probabilistic Framework"

 
}}

Forschungslinie (SS2016)

2016-04-25T13:17:15Z

Peter Steinke:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Tutors=Peter Steinke;
|Term=SS
|Year=2016
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar.

* [https://ddll.inf.tu-dresden.de/w/images/d/d4/Folien.pdf Einführungsfolien]

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Die Auswertung des Wettbewerbs findet am 4.7. in der 4 DS statt.

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei [https://ddll.inf.tu-dresden.de/web/Peter_Steinke Peter Steinke] registrieren. Eine Vorabversion des Tools muss bis spätestens eine Woche vor dem Wettbewerb eingereicht werden (27.06), damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.

Abgabetermin 
Die finale Version des Werkzeugs muss am Freitag, 30.6., bis 24:00 eingereicht worden sein. Dies erfolgt via Mail an [https://ddll.inf.tu-dresden.de/web/Peter_Steinke Peter Steinke].

Wettbewerbsumgebung 

* [https://ddll.inf.tu-dresden.de/w/images/d/d2/HamiltonianCycleCompetition-Environment-SS2015.tar.gz Wettbewerbes Umgebung]
* [https://ddll.inf.tu-dresden.de/w/images/8/83/Forschungslinie2015-Graphs.tar.gz Graphen des Wettbewerbs 2015]

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (es gibt ein "Checker-Werzeug" in der Umgebung, welches nur dieses Format richtig erkennt, und die Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls auch Graphen aus anderen Quellen zugelassen sind.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut. Bitte bei der Abgabe kurz beschreiben.
</li>
</ul>

}}

2016-04-14T07:00:49Z

Peter Steinke:

{{Vorlesung
|Title=Forschungslinie
|Research group=Wissensverarbeitung
|Lecturers=Steffen Hölldobler;
|Tutors=Peter Steinke;
|Term=SS
|Year=2016
|SWSLecture=0
|SWSExercise=0
|SWSPractical=0
|Exam type=Hausarbeit
|Description=Diese Vorlesung im Rahmen der Forschungslinien-Vorlesung stellt kurz die Forschung um das Erfüllbarkeitsproblem dar.

Wettbewerb 
Es soll ein Löser entwickelt werden, der einen Graphen im DIMACS-Graph-Format einlesen kann, und für diesen Graph einen Hamiltonian-Cycle ausgibt, oder ausgibt, dass es keine Lösung gibt. Im Wettbewerb werden mehrere Graphen gelöst. Der Löser, welcher die meisten Graphen in einem gegebenen Timeout (ca. 10 Minuten) erfolgreich lösen kann, gewinnt. Löser, die eine falsche Lösung ausgeben, werden disqualifiziert. Beispielgraphen gibt es hier: http://mat.gsia.cmu.edu/COLOR/instances.html

Registrierung 
Um an dem Wettbewerb teilnehmen zu können, müssen sich die Team von maximal drei Studenten mit einem Teamnamen, sowie der Namen der Studenten und der Matrikelnummer per Email bis zwei Wochen vor dem Wettbewerb bei [https://ddll.inf.tu-dresden.de/web/Peter_Steinke Peter Steinke] registrieren. Eine Vorabversion des Tools muss bis eine Woche vor dem Wettbewerb eingereicht werden, damit sie auf ihre Lauffähigkeit getestet werden kann (der Wettbewerb wird auf einem Linux System ausgetragen). Der Wettbewerb findet nur statt, wenn sich mindestens drei Teams angemeldet haben.

Abgabetermin 
Die finale Version des Werkzeugs muss am Freitag, 3.7., bis 24:00 eingereicht worden sein. Dies erfolgt via Mail an [https://ddll.inf.tu-dresden.de/web/Peter_Steinke Peter Steinke]

Wettbewerbsumgebung 

* [https://ddll.inf.tu-dresden.de/w/images/d/d2/HamiltonianCycleCompetition-Environment-SS2015.tar.gz Wettbewerbes Umgebung]
* [https://ddll.inf.tu-dresden.de/w/images/8/83/Forschungslinie2015-Graphs.tar.gz Graphen des Wettbewerbs 2015]

Format und andere Details 

<ul>
<li>das Format für die Lösung ist (es gibt ein "Checker-Werzeug" in der Umgebung, welches nur dieses Format richtig erkennt, und die Lösungen entsprechend bewertet):</li>
<ul>
<li>
kein Cycle: 
"s UNSATISFABLE" 
auf stdout, exitcode 20 
</li>
<li>
ein Cycle mit dem Pfad 5->3->4->1->2->5 
"s SATISFIABLE" 
"v 5 3 4 1 2" 
auf stdout, exitcode 10 
</li>
</ul>
<li>
Die Graphen sind eigentlich gerichtet, der Generator liefert für
kleine Graphen meist ungerichtete Graphen, da beide Kanten da sind.
Für größere Graphen ist das nicht garantiert.
</li>
<li>
Der Generator ordnet die Kanten, darauf kann man sich aber nicht
verlassen, falls auch Graphen aus anderen Quellen zugelassen sind.
</li>
<li>
Der SAT Solver darf mehrfach aufgerufen werden. Dann interessiert uns was ihr damit genau tut. Bitte bei der Abgabe kurz beschreiben.
</li>
</ul>
}}