Abschlussarbeit / Thesis (EN) AI | Logic: A Novel SAT Solver Architecture
All the current state-of-the-art SAT solvers are based on the architecture of MiniSat. MiniSat is a great and very influential SAT solver, however, it is nearly 20 years old now. It is time to start trying out some alternative approaches. The architecture of MiniSat is very clause (or-clause, i.e., disjunction of literals) centered. The idea is to design a SAT solver where the notion of the clause is generalized, such that a clause can be anything that implements a certain interface. A clause could then be a cardinality constraint, DNF formula or a BDD (Binary Decision Diagram). This way we could integrate available knowledge about various Boolean function representations into SAT solvers. The topic of the thesis is to design and implement a new kind of SAT solver and compare it experimentally with current state-of-the-art SAT solvers.
- Do a literature research on various Boolean function representations (BFRs) such as CNF, DNF, BDD and the architecture of state-of-the-art SAT solvers
- Design a new SAT solver architecture that supports the usage of multiple BFRs instead of just CNF
- Modify a state-of-the-art SAT solver or Implement a new one based on the proposed architecture in C/C++/Java and compare it experimentally to state-of-the-art SAT solvers
- Summarize the results in your thesis and scientific publication(s)
- You can find, read and understand scientific papers relevant for a given topic.
- Creativity in approaching hard problems.
- Can write performant C/C++/Java code (fast running programs).
- Not being scared off by hard (NP-Hard) problems.
- Communicating your ideas clearly and precisely in writing (in English).
Benefits of your thesis at CAS
- An ideal environment for you and your thesis: With us you can spend 100% of your worktime on your thesis where you combine state-of-the-art research with real industry use-cases.
- Professional supervision of your thesis in the CAS Future Labs in Karlsruhe: Every year we accompany many students to their successful graduation - you too can benefit from our experience.
- Get to know the CAS culture (offline and online): by working with business coaches and taking part in many other interactive formats. You will experience our unique WeSpirit and make connections across multiple units.
Referentin People & WeCulture
Please send us the following documents in complete form
- Your motivation: Why this subject? Why with us?
- Time period and type of thesis (master / bachelor)
- Current transcript of grades
- Certificate of enrolment
- Further evidence of your qualifications (e.g. working references)