Non-Deterministic Satisfiability Problem

What is Non-Deterministic Satisfiability Problem?

The non-deterministic satisfiability problem is a decision problem that is studied in theoretical computer science and logic. The problem is frequently abbreviated as NSAT. It is closely related to the well-known Boolean satisfiability problem (SAT), which asks whether a given Boolean formula can be satisfied by assigning truth values to its variables. This problem has been around for a long time and has a lot of history behind it.

We are given a Boolean formula in conjunctive normal form (CNF) with n variables and m clauses, and the goal of the NSAT is to determine whether or not there is a non-deterministic assignment of truth values to the variables that satisfy the formula. In other words, we want to find out if the formula can be satisfied by a set of truth values that are not predetermined. A set of all of the possible truth value assignments that can be made to variables is an example of a non-deterministic assignment.

The issue is regarded as one of the most challenging issues in the field of computer science, and experts have determined that it is an NP-complete problem. This indicates that it is thought to be computationally intractable, which means that there is no known algorithm that is capable of solving it efficiently for all instances and that it is just as difficult as any other problem that falls under the umbrella of NP.

The NSAT has many important applications in computer science and other related fields, including automated reasoning, formal verification, and cryptography, to name just a few. Backtracking, branch-and-bound, and local search algorithms are some examples of the many approaches and heuristics that can be used to tackle NSAT instances. Despite the difficulty of the problem, there are many different approaches and heuristics that can be used.

Truth Table

• Boolean expressions are the expressions which produce boolean value when evaluated i.e. 0 or 1, True or False etc.
• AND ( [katex] \land [/katex] ), OR ( \[ \lor \] ) and NOT (‘) are the most commonly used Boolean operators. Given two boolean variables a and b, the truth table for these boolean operators is shown below:

a	B	a \[ \land \] b	a \[ \lor \] b	a’
0	0	0	0	1
0	1	0	1	1
1	0	0	1	0
1	1	1	1	0

• The satisfiability problem is to check the correctness of the assignment. Let x₁, x₂, …, x_n are Boolean variables having values either true or false.
• The satisfiability problem is to find the true value of the Boolean expression consisting of AND/OR Boolean operations.
• Boolean expressions are formed using boolean operators and boolean variables.

                       Example: y   =   ( a \[ \land \] b ) \[ \lor \] ( a’ \[ \lor \] b \[ \land \] c)

• Let expression E(x₁, x₂, …, x_n) represents the Boolean expression of n Boolean variables. In the guessing stage, the nondeterministic algorithm assigns the true or false value of each of x_i non-deterministically.
•  In the verification stage, the truth value of the assignment for expression is checked.

Algorithm

The nondeterministic algorithm for the satisfiability problem is described below :

Algorithm NON_DET_SAT_PROBLEM(E)
// Description : Solve satisfiability problem using non-deterministic algorithm
// Input : Boolean expression E of n variables
// Output : Success / Failure

// Guessing stage
for i ← 1 to n do
    x[i] ← select (true, false)
end

// Verification stage: Check truth of expression
if E(x1, x2, …, xn) is true then
    success( )
else
    failure( )
end

• Guessing stage runs in O(n) time. Evaluation of expression E of n variable can be done in O(f(n)) time. Thus running time of the algorithm would be O(n) + O(f(n)). 

---

YouTube Channel: CodeCrucks