Boolean Satisfiability Problem (SAT)

Modern Boolean Satisfiability Problem (SAT) solvers utilise a ”smart” brute force search. This means that SAT solvers can find ”smart” solutions to Boolean Satisfiability problems. Hence, any problem that can be converted into a SAT problem can be solved in an unexpected manner by a SAT solver. In order to understand the satisfiability problem, we must first define the language in which the problem is phrased. The language is propositional logic. Hence they are sometimes called propositional satisfiability problem solvers. SAT is the first problem that was proven to be NP-complete. Thinking of all the problems in the outside world you could attack with SAT technology like

  1. Model Checking (Formal verification)
  2. Software and hardware verification
  3. Industrial automated planning and scheduling (Industry 4.0) [ https://www.cs.cornell.edu/gomes/pdf/2008_gomes_knowledge_satisfiability.pdf and https://eprints.soton.ac.uk/265340/1/jpms-wodes08.pdf]
  4. Master-key system design[ https://dspace.cvut.cz/bitstream/handle/10467/73952/F3-DP-2018-Horenovsky-Martin-main.pdf ]
  5. Intelligent Energy Optimization in Smart Home Environments[https://www.researchgate.net/publication/230681899_Intelligent_Energy_Optimization_for_User_Intelligible_Goals_in_Smart_Home_Environments]
  6. Combinatorial design like Sudoku and Candy Crush [https://arxiv.org/abs/1403.5830]
  7. Cryptographic problems

The potentials of the technology is obvious. Finding if a problem is solvable is of huge interest in the industry. Especially cryptographic problems can be reduced to their hardness. That is why we used them to tackle improving modern SAT solvers to even better performance.

Join us at FLoC 2018 in Oxford

SAT

Floc2018

Performing hundreds of test runs and a source-code analysis, we empirically identified improved parameter configurations for CryptoMiniSat (CMS) 5 for solving cryptographic CNF instances originating from algebraic known-plaintext attacks on 3 rounds encryption of the Small AES-64 model cipher SR(3, 4, 4, 4). We finally became able to reconstruct 64-bit long keys in under an hour real time which, to our knowledge, has never been achieved so far.

The outcomes are summarized in a paper “CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances” (https://easychair.org/smart-program/FLoC2018/POS-2018-07-07.html#talk:72772) . We are now proud of being invited to present our findings at this year’s “Federated Logic Conference 2018” in Oxford, UK. We that is Anastasia Leventi-Peetz, Oliver Zendel, Werner Lennartz and Kai Weber.

#SAT, #FLoC2018, #Industry4.0, #AI, #Inducto, #Werusys