Master's Thesis: Integration of SAT4J CSP into AGILA/SysMD
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
Bachelor's Thesis: Integration of SAT4J in the AGILA/SysMD Environment
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
Automated Regression Test Generation for Constraint Satisfaction Problems
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