15.2.2016

Reduction

SAT Problem
Group 1
1

Reduction

2

Reduction

an important concept for understanding the relationship between problems.

3

solving one problem in terms of another 
 Example :

Suppose you have some problem A that you don’t know how to solve. 

If you can find a way to reduce problem A to some problem B that you do know how to solve, then that’s just as good as finding a way to solve A in the first place.

4

SORTING:

Input: A sequence of integers x0, x1, x2, ..., xn−1.

Output: A permutation y0, y1, y2, ..., yn−1 of the sequence such that yi ≤ yj whenever i < j.

PAIRING:

Input: Two sequences of integers X = (x0, x1, ..., xn−1) and Y =
(y0, y1, ..., yn−1).

Output: A pairing of the elements in the two sequences such that the least value in X is paired with the least value in Y, the next least value in X is paired with the next least value in Y, and so on.

5

An illustration of PAIRING. The two lists of numbers are paired up so that the least values from each list make a pair, the next smallest values from each list make a pair, and so on.

6

Solution
PAIRING is to use an existing sorting program to sort each of the two sequences, and then pair off items based on their position in sorted order.

PAIRING is reduced to SORTING, because SORTING is used to solve PAIRING.

7

3-step Process
1. convert an instance of PAIRING into two instances of
SORTING .
2. sort the two arrays .
3. convert the output of SORTING to the output for PAIRING .

8

We can define reduction more formally as a three-step process:
1. Transform an arbitrary of the first problem to an instance of the second problem.There must be a transformation of any instance I of the first problem to an instance I’ of the second problem. 2. Apply an algorithm for the second problem to the instance I’ , yielding a solution SLN’ .
3. Transform SLN’ to the solution of I , known as SLN.

9

10

SAT Problem

11

The Satisfiability Problem
(SAT)
•

A literal is either a boolean variable x or its negation ¬x.

•

A clause is a disjunction of literals.

For example, x1 ∨ x2 ∨ ¬x4 is a clause.

•

A formula in conjunctive normal form (CNF) is propositional formula which is a conjunction of clauses.

(x1 ∨ x2 ∨ ¬x4) ∧ (x2 ∨ ¬x3) ∧ x5 is a CNF formula

12

SAT as a Language/ Problem

•

An instance of SAT is a boolean function.

•

Must be coded in finite alphabet.

•

Use special symbols (,) , + , - as themselves..

13

Example:Encoding for SAT

•

(x+y) (-x + -y) would be encoded by the string
(x1+x10) (-x1 + -x10).

14

Importance of SAT
•

SAT is a basic constraint satisfaction problems.

•

Many different problems can reduced to SAT because of the simple yet powerful expressively of logical constraints.

•

Arise naturally in many applications involving hardware and software verification and correctness.

•

It is a fundamental problem in theory of NP-Completeness.

15

Practical Applications
•

Model Checking

•

Automatic Test Pattern Generation

•

Combinational Equivalence Checking

•

Planning in AI

•

Automated Theorem Proving

•

Software Verification
16

3SAT
In 3SAT every clause must have exactly 3 different literals •

Example: 

(x1∨x2∨¬x4)∧(x2∨¬x3∨x1) is a 3SAT, 
 but (x1∨x2∨¬x4)∧(x2∨¬x3)∧x5 is not.

17

Reduction SAT to 3-SAT

•

φ = (x1 ∧x2)∨ ¬((¬x1 ∨x3)∧x4 ∧ ¬x5)∧ ¬x2.

18

19

20

We now have a bunch of clauses that each have at most 3 literals. We need to convert these clauses into CNF. To do this, for each clause we will write a truth table to see when the clause is true. For instance, if clause C1 = (y1 ⇐ (y2 ∧ ¬x2)), then the truth table for C1 is:

21

With this truth table we will examine each row where the value of
C1 is false, or where ¬C1 is true. In this example we see that

22

We can apply DeMorgan’s laws to this formula to obtain a version of this clause in CNF:

23

To finish this reduction we have to deal with the clauses that have fewer than 3 literals in them.
Suppose for instance that we have some clause (x ∨ y).
This clause is equivalent to (x ∨ y ∨ p) ∧ (x ∨ y ∨ ¬p) because, no matter what value of p we choose, one of x or y must be true for these clauses to be true, which is exactly the condition that satisfies the original clause.
With this reduction we have proven that 3-SAT is at least as hard as SAT. This is useful for showing that other problems are at least as hard as SAT

24

Thank You !

25