tig-monorepo/docs/challenges/satisfiability.md

Boolean Satisfiability

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: 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:

(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 x_1 = True, x_2 = False, x_3 = True, x_4 = False. This can be verified by substituting the variables and evaluating that every clause will result in True.

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:

• Parameter 1: num\textunderscore{ }variables = The number of variables.
• Parameter 2: clauses\textunderscore{ }to\textunderscore{ }variables\textunderscore{ }percent = The number of variables as a percentage of the number of clauses.

The number of clauses is derived from the above parameters.

num\textunderscore{ }clauses = floor(num\textunderscore{ }variables \cdot \frac{clauses\textunderscore{ }to\textunderscore{ }variables\textunderscore{ }percent}{100})

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

Consider an example instance with num_variables=4 and clauses_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 assignment X1=False, X2=True, X3=True, X4=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.

Figure 1: Chips made possible by electronic circuit design.