What is Boolean satisfiability problem?

The Boolean satisfiability problem is often abbreviated to SAT. In the field of computer science the Boolean satisfiability problem is concerned with the determination of whether or not an interpretation exists, satisfying some given Boolean formula. The other way round, we can say that it is established when in a given Boolean formula; the variables can be assigned in such a way that upon evaluation, the value of the formula is TRUE. If any such assignment is not found, the function that the formula expresses is FALSE for all the ways in which the variables can be assigned. In this case, the problem is said to be unsatisfiable and satisfiable in the former case. Consider the following examples for a better understanding:
- X AND NOT y: This problem is satisfiable since we can find many values for which x is true and y is false.
- X AND NOT x: This problem is unsatisfiable since ’a’ cannot have two values at the same time.

This Boolean unsatisifiability problem actually falls under the category of the NP – complete problems. Till date we don’t have any algorithm that can effectively solve all types of such problems and it is also believed that there is no such algorithm. However there exists a number of problems involving decision and optimization that can be transformed into the SAT instances. The algorithms that have been used to solve a large subset of these problems have been grouped in a class called the SAT solvers. The application of the SAT instances is in the following fields:
- Circuit design
- Automatic theorem proving

Extensive research has been going on for extending the capabilities of the algorithms for solving SAT. but, presently we don’t have any such method that can deal with all the instances of the SAT. A Boolean expression also called as the propositional logic formula is composed of the operators: AND, OR, NOT, () etc. and variables. A formula can be called satisfiable only if it evaluates to be TRUE through assigning the variables appropriate logical values i.e., whether TRUE or FALSE. This formula is used for checking the satisfiability of a SAT instance. Another type of problems falling under this category is decision problem. This type of problems plays a major role in the following fields:
- Theoretical computer science
- Complexity theory
- Artificial intelligence and
- Algorithmics

We have many cases of the SAT problems where we need to have formulas with a certain structure. A variable or a literal is of two types namely the positive literal and the negative literal (negative of a variable). Then we have a clause two which is nothing but a single literal or a disjunction of the literals. If a clause consists of 0 or 1 positive literal, it is said to be a horn clause. If a formula is a conjunction of the clauses, it is a CNF (conjunctive normal form) formula.
It has been observed that defining the notion of generalized CNF formula is useful for solving some instances of the SAT problems. Different problem versions occur due to the different sets of the allowed operators. The Boolean algebra laws can be used for transforming every propositional logic formula in to its CNF equivalent form which might be longer than the one in its original form. SAT problems were the first problems discovered under the field of the NP- complete problems. Before 1971, this concept didn’t even exist. If the formulas can only be used in the disjunctive normal form, SAT is said to be trivial. These formulas are satisfiable iff only one of their conjunctions can be satisfied.

Control Structure Testing - Condition Testing, Data Flow Testing, Loop Testing

Control structure testing is a group of white-box testing methods.
CONDITION TESTING
- It is a test case design method.
- It works on logical conditions in program module.
- It involves testing of both relational expressions and arithmetic expressions.
- If a condition is incorrect, then at least one component of the condition is incorrect.
- Types of errors in condition testing are boolean operator errors, boolean variable errors, boolean parenthesis errors, relational operator errors, and arithmetic expression errors.
- Simple condition: Boolean variable or relational expression, possibly proceeded by a NOT operator.
- Compound condition: It is composed of two or more simple conditions, Boolean operators and parentheses.
- Boolean expression: It is a condition without Relational expressions.

DATA FLOW TESTING
- Data flow testing method is effective for error protection because it is based on the relationship between statements in the program according to the definition and uses of variables.
- Test paths are selected according to the location of definitions and uses of variables in the program.
- It is unrealistic to assume that data flow testing will be used extensively when testing a large system, However, it can be used in a targeted fashion for areas of software that are suspect.

LOOP TESTING
- Loop testing method concentrates on validity of the loop structures.
- Loops are fundamental to many algorithms and need thorough testing.
- Loops can be defined as simple, concatenated, nested, and unstructured.
- In simple loops, test cases that can be applied are skip loop entirely, only one or two passes through loop, m passes through loop where m is than n, (n-1), n, and (n+1) passes through the loop where n is the maximum number of allowed passes.
- In nested loops, start with inner loop, set all other loops to minimum values, conduct simple loop testing on inner loop, work outwards and continue until all loops tested.
- In concatenated loops, if loops are independent, use simple loop testing. If dependent, treat as nested loops.
- In unstructured loops, redesign the class of loops.

Control Structure Testing : Condition testing

Condition testing is a test case design approach that exercises the logical conditions contained in a program module. Errors in conditions can be due to:
* Boolean operator error
* Boolean variable error
* Boolean parenthesis error
* Relational operator error
* Arithmetic expression error
The condition testing method concentrates on testing each condition in a program. The purpose of condition testing is to determine not only errors in the conditions of a program but also other errors in the program. A number of condition testing approaches have been identified.
Domain testing needs three and four tests to be produced for a relational expression. For a relational expression of the form
E1 < relational-operator > E2
Three tests are required the make the value of E1 greater than, equal to and less than E2,respectively.