Integration of SAT4J CSP in the AGILA/SysMD Environment

Problem Description: Modern SAT Solvers are capable of solving much more than mere SAT-instances. A growing number of those solvers are used to model and solve Constraint Satisfaction Problems. Thus, it is only logical to compare the capabilities of such a specialized solver for given Constraint Satisfaction Problems.

Task of the thesis: The goal of the thesis is to integrate the Java-based SAT-Solver SAT4J CSP into the AGILA/SysMD environment and to define a translation interface between the used languages.

(Possible) Organization:

Phase 0 (1 Month):
Get familiar with Constraint Satisfaction Problems, SAT and the used framework

Phase 1 (1 Week):
Translation between solver languages (SysMD -> XML)

Phase 2 (1 Month):

Integration of Java-based Sat4J CSP in Kotlin-based AGILA tool

Phase 3 (1 Month):

Testing and Experiments: Compare your integration with the built-in tooling of AGILA

Phase 4 (2,5 Month):

Thesis writing

Betreuer: Axel Ratzke

Integration of SAT4J in the AGILA/SysMD Environment

Problem Description: Boolean (and selected discrete) Constraint Satisfaction Problems can be mapped almost one to one onto a SAT instance. Thus, it is only logical to compare the capabilities of such a specialized solver for given Constraint Satisfaction Problems.

Task of the thesis: The goal of the thesis is to integrate the Java-based SAT-Solver SAT4J into the AGILA/SysMD environment and to define a translation interface between the used languages.

(Possible) Organization:

Phase 0 (1 Month):
Get familiar with Constraint Satisfaction Problems, SAT and the used framework

Phase 1 (1 Week):
Translation between solver languages (SysMD -> Dimacs CNF/AIG and vice versa)

Phase 2 (1 Month):

Integration of Java-based Sat4J in Kotlin-based AGILA tool

Phase 3 (1 Month):

Testing and Experiments: Compare your integration with the built-in tooling of AGILA

Phase 4 (2,5 Month):

Thesis writing

Betreuer: Axel Ratzke

Problem Description: To test and/or demonstrate the capabilities of a Solver for a Constraint Satisfaction Problem, test cases are needed which are not easily solvable by the human eye.

To construct such a test in the appropriate scope by hand is difficult, time consuming and error prone. To counter this problem, already existing test cases could be appropriately scaled up to the task.

Task of the thesis: The goal of the thesis is to develop a generator, that takes a minimal test as well as some control parameters and generates an upscaled variation of the test.

(Possible) Organization:

Phase 0 (1 Month):
Get familiar with Constraint Satisfaction Problems and the used framework

Phase 1 (1 Week):
Variation generation: Generate variations (within predefined bounds) of input model

Phase 2 (1 Month):

Problem generation: Based on a constraint and a solution generate a matching problem and populate it with variations and further solutions

Phase 3 (1 Month):

Accumulation of multiple problems: Generate a test case comprised of multiple (possibly) unrelated constraint systems

Phase 4 (2,5 Month):

Thesis writing

Betreuer: Axel Ratzke