TIG Logo

Challenge

Boolean Satisfiability

Help design more effective microchips by solving Boolean satisfiability problems.

Join the game

Overview

The SAT (or Boolean Satisfiability) problem is a decision problem in computer science.

It's the problem of determining if there exists a truth assignment to a given Boolean formula that makes the formula true (satisfies all clauses). A Boolean formula is built from:

  • Boolean variables: x1,x2,x3,…x_1, x_2, x_3, \ldots
  • Logical connectives: AND (∧\land), OR (∨\lor), NOT (¬\neg)
  • Parentheses for grouping: ( )

3-SAT is a special case of SAT where each clause is limited to exactly three literals (a literal is a variable or its negation).

Applications

SAT has a vast range of applications in science and industry in fields including computational biology, formal verification, and electronic circuit design.

For example: SAT is used in computational biology to solve the "cell formation problem" of organising a plant into cells. SAT is also heavily utilised in electronic circuit design.

Microchips made possible by electronic circuit design

Figure 1: Chips made possible by electronic circuit design