Show all tags

Nice find, detective! ;)

Latest Posts


Playing Hard Mastermind Games with a SAT-based AI

Back in the day, Mastermind was a popular two player code-breaking game, and many variations thereof still exist as both standalone games and puzzles within other games. Although it is difficult for a human player to make optimal guesses of the secret code, or at least guesses that do not conflict with the provided clues, the setting is usually simple enough for an AI to find such candidates via explicit exploration of the game tree.

However, such approaches becomes unfeasible when the number of possibilities for secret codes grows into the millions. This post illustrates the problem with standard approaches, and how finding consistent candidates can be approached with SAT solving – yielding an AI that can handle orders-of-magnitude harder Mastermind instances.

» Read more

Solving a Logic Synthesis Puzzle via SAT/SMT

A few weeks ago, I was asked the following riddle: Design a logic circuit with three inputs and three outputs, such that the outputs are the inverted inputs. You may use arbitrary many AND and OR gates, but at most two NOT gates. Although the characterisation of this problem as an SMT instance is straightforward, I found it necessary to reduce it to SAT and incorporate further assumptions to achieve reasonable performance.

This post illustrates said process, ranging from the original idea to a standard formulation of SAT-based logic synthesis to a problem-specific and more constrained instance.

» Read more

SMT-based Reasoning About the Fast Inverse Square Root

While there is a mathematical explanation for the choice of 0x5F3759DF in the famous bit-level hack for approximating the multiplicative inverse of the square root of a 32-bit floating-point number, it is not immediately clear to what extent the reasoning is really applicable in the context of machine data types and their peculiarities. This post illustrates how this, and related aspects, can be investigated with SMT-based reasoning about the actual implementation.

» Read more