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.

  • 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). An example with 4 variables and 3 clauses can be seen below:

(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 = {True}, x_2 = {False}, x_3 = {True}, x4 = {False}

This can be verified by substituting the variables and evaluating that every clause will result in True.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:

Example

The following is an example of the 3-SAT problem with configurable difficulty. Two parameters can be adjusted in order to vary the difficulty of the challenge instance:

  • num_variablesnum\_variables = The number of variables.
  • clauses_to_variables_percentclauses\_to\_variables\_percent = The number of variables as a percentage of the number of clauses.

The number of clauses is derived from the above parameters:

num_clauses=floor(num_variables⋅clauses_to_variables_percent100)num\_clauses = floor(num\_variables \cdot \frac{clauses\_to\_variables\_percent}{100})

Where floorfloor is a function that rounds a floating point number down to the closest integer.

Consider an example Challenge instance with num_variables=4num\_variables = 4 and clauses_to_variables_percent=75clauses\_to\_variables\_percent = 75:

clauses = [
    [1, 2, -3],
    [-1, 3, 4],
    [2, -3, 4]
]

Each clause is an array of three integers. The absolute value of each integer represents a variable, and the sign represents whether the variable is negated in the clause (negative means it’s negated).

The clauses represents the following Boolean formula:

(x1 or x2 or not x3) and (not x1 or x3 or x4) and (x2 or not x3 or x4)

Now consider the following assignment:

assignment = [False, True, True, False]

This assignment corresponds to the variable assiengment:

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

When substituted into the Boolean formula, each clause will evaluate to True, thereby this assignment is a solution as it satisfies all clauses.

Our Challenge

In TIG, the 3-SAT Challenge is based on the example above with configurable difficulty. Please see the challenge code for a precise specification.

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