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).

Example

This is an example with 4 variables and 3 clauses:

(x1∨x2∨x3)∧(¬x1∨¬x3∨¬x4)∧(¬x2∨x3∨x4)(x_1 \lor x_2 \lor x_3) \land (\neg x_1 \lor \neg x_3 \lor \neg x_4) \land (\neg x_2 \lor x_3 \lor x_4)

For this particular example, one possible truth assignment that satisfies this formula is:

x1=True,x2=False,x3=True,x4=Falsex_1 = \text{True}, x_2 = \text{False}, x_3 = \text{True}, x_4 = \text{False}

This can be verified by substituting the variables and evaluating that every clause will result in True.

Our Challenge

In TIG, we feature instances of the 3-SAT Challenge. Given a number of variables, the number of clauses is derived from the following formula

num_clauses=⌊num_variables⋅clauses_to_variables_percent100⌋\text{num\_clauses} = \left\lfloor \text{num\_variables} \cdot \frac{\text{clauses\_to\_variables\_percent}}{100} \right\rfloor

in TIG we fix the clauses_to_variables_percent=16%\text{clauses\_to\_variables\_percent} = 16\%.

The size parameter num_variables\text{num\_variables} is chosen by the benchmarkers, it determines the number of variables in a given instance.

When generating an instance:

  • Variable Selection. Each clause picks three variables uniformly at random from 1 to num_variables\text{num\_variables}. Each literal is chosen independently, so a clause can include the same variable multiple times.
  • Negation Decision. Each literal is negated with 50% probability, independently. For example, if variable 3 is selected, it appears as x3x_3 or ¬x3\neg x_3 with equal chance.

A solution is given a binary quality score of 1 (if it is a truth assignment) or 0 (if the assignment is false).

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