Circuit SAT to SAT

Loading...

Do curso por University of California San Diego

Advanced Algorithms and Complexity

220 classificações

University of California San Diego

Advanced Algorithms and Complexity

220 classificações

Curso 5 de 6 em Specialization Data Structures and Algorithms

You've learned the basic algorithms now and are ready to step into the area of more complex problems and algorithms to solve them. Advanced algorithms build upon basic ones and use new ideas. We will start with networks flows which are used in more typical applications such as optimal matchings, finding disjoint paths and flight scheduling as well as more surprising ones like image segmentation in computer vision. We then proceed to linear programming with applications in optimizing budget allocation, portfolio optimization, finding the cheapest diet satisfying all requirements and many others. Next we discuss inherently hard problems for which no exact good solutions are known (and not likely to be found) and how to solve them in practice. We finish with a soft introduction to streaming algorithms that are heavily used in Big Data processing. Such algorithms are usually designed to be able to process huge datasets without being able even to store a dataset.

Na lição

NP-complete Problems

Although many of the algorithms you've learned so far are applied in practice a lot, it turns out that the world is dominated by real-world problems without a known provably efficient algorithm. Many of these problems can be reduced to one of the classical problems called NP-complete problems which either cannot be solved by a polynomial algorithm or solving any one of them would win you a million dollars (see Millenium Prize Problems) and eternal worldwide fame for solving the main problem of computer science called P vs NP. It's good to know this before trying to solve a problem before the tomorrow's deadline :) Although these problems are very unlikely to be solvable efficiently in the nearest future, people always come up with various workarounds. In this module you will study the classical NP-complete problems and the reductions between them. You will also practice solving large instances of some of these problems despite their hardness using very efficient specialized software based on tons of research in the area of NP-complete problems.

Showing NP-completeness6:40

Independent Set to Vertex Cover5:28

3-SAT to Independent Set14:57

SAT to 3-SAT7:04

Circuit SAT to SAT12:01

All of NP to Circuit SAT5:42

Using SAT-solvers14:11

Conheça os instrutores

Alexander S. Kulikov
Visiting Professor
Department of Computer Science and Engineering
Michael Levin
Lecturer
Computer Science
Daniel M Kane
Assistant Professor
Department of Computer Science and Engineering / Department of Mathematics
Neil Rhodes
Adjunct Faculty
Computer Science and Engineering

We now proceed to the most interesting reduction in this model.

Namely we are going to show that every search problem,

every problem from the class NP reduces to SAT.

So for this actually we're going to show, we're going to introduce an intermediate

problem called Circuit SAT which is also an important computational problem.

And we're going to show that any search problem reduces the Circuit SAT and

in turn the Circuit SAT problem reduces through the SAT problem.

So, what is a Boolean circuit?

In some sense it is just a generalization of the Boolean formula.

So, it is a computational model for computing a Boolean function.

An example of a circuit is shown here on the slide.

So it is in effect, a graph, and there with some input notes.

So here we have input nodes marked with variables.

And this input node is marked with a Boolean constant, 1.

And all other nodes are marked by boolean operations, namely with conjunctions.

Here, these junctions here and negations.

So, when x, y and z are assigned boolean values, for example,

0 1, 0, we can compute what is an output of this circuit.

To do this we just apply these Boolean operations to the inputs of each node.

The nodes are called gates.

For example, the value of this gate is equal to 0,

because this is a logical AND of 0 and 1.

The value of this gate Is equal to 1, because this is a logical OR of 1 and 0.

Then, the value of this gate is 1, because this is a negation of 0.

Is the value of this gate, is equal to 1, because this is a logical OR of 1, and 1.

The value of this gate, is also 1 because this is an OR of 1 and 1.

And finally the value of this gate is also equal to 1.

So when x is equal to 0, y is equal to 1 and z is equal to 0,

the output of this circuit is equal to 1, okay.

More formally, a circuit is a directed acyclic graph such that all

of its vertices have in-degree either 0, 1, or 2.

The nodes of in-degree 0 are called inputs.

And they are marked by Boolean variables or by Boolean constants.

Nodes of in-degree 1 are labeled with negations, and nodes of in-degree

2 are labeled with dejunctions or conjunctions or with logical ORs and ANDs.

Also, there is one node which is labelled as an output.

This is a gate of our degree 0.

So a circuit is a computational model.

Such a circuit computes in a natural way a function which

depends on input boolean variables, okay.

So, we can compute this function exactly because

the underlying graph contains no cycles.

We can just topologically sort all the gates and compute the value for

each gate in typological ordering.

I mean, when the input variables are assigned values.

Now, the correspondent search problem is very natural.

We are given a circuit and we would like to check whether it is possible to

assign values to its variables so that the circuit outputs 1.

This is a generalization of the problem

where instead of a circuit, we are given just the formula.

Note, however,

that a CNF formula can also be represented as a circuit in a very natural way.

Just to give an example.

If our example considers the following formula in conjunctive normal form.

Here, we have two clauses.

X or y or not z, and y or not x.

We can represent it as a circuit as follows.

So first, we need to compute the value of the first clause.

We do this as follows.

So we compute x or y.

This is computed at this gate.

And then we compute x or y or z.

Okay, so this can respond to the first clause.

Then we need to compute the value of the second clause.

For this we first compute the negation of x.

It is computed at this gate and then we can compute the logical OR

of the mitigation effects and y.

And finally, so this gate computes the value of the second clause.

Finally, we take the logical AND of these two clauses.

So clearly, this circuit computes exactly the same as this

boolean formula in conjunctive normal form.

What we need to do now is to reduce circuit set to its special case.

Namely Circuit-SAT to SAT.

For this we need to do the following.

We need to design a polynomial time algorithm which takes a circuit and

transforms it in a polynomial time into a formula in CNF

which is satisfiable if and only if the initial circuit is satisfiable.

To do this, we are going to do the following.

For each gate of the initial circuit, we introduce a new variable.

So this variable is going to be assigned to this gate.

So, in total, we're going to have variables that correspond to both of these

circuit and also, one Boolean variable for each gate of the initial circuit.

Then, we're going to write down a bunch of clauses.

For each gate of our initial circuit, we're going to write

a few clauses that will somehow en code, the relationship,

because between the input of this gate with the value computed at this gate.

We'll now explain how to write down these clauses.

We start with the case when the current gate g for

which we are going to write down these clauses is labeled with a negation sign.

So consider such a gate, so it is labelled with a negation sign and

the corresponding variable is g.

Assume that its predecessor is marked with label h.

Then, we'll write down the following two clauses of lengths 2.

So what does these two clauses mean?

Well, what is essentially says a full,

if h is = to 1 then g must be equal to 0.

Right, so this is forced by the second clause.

Indeed, if h is equal to 1.

Then in the second clause, this literal is already falsified, which means that

the only way to satisfy the second clause is to set g to be equal to 0, right?

And vice versa.

If h is equal to 0, then g must be equal to 1.

This is forced by the first close.

So if h=0, then in the first clause, the value of h is already falsified.

So the only way to satisfy the first clause is to set g to be equal to 1.

Which means that in any satisfying assignment or for formulas that contains

the following two clauses, h and g always have the opposite values

which in turn means that g always equal to h negated.

And this is exactly what we need to encode in our CNF formula.

Now considering AND gate, assume that g is an AND

gate, and its two direct predecessors are h1 and h2.

We then write down the following three clauses.

Let's again see what do they encode.

The first clause says that if h1=0,

then the only way to satisfy the first clause is to set g to 0.

So if h1=0, then g=0.

This is exactly what we need.

If h1=0 here, then the resulting gate g also computes 0, right?

Because this is a conjunction illogical nth of h1 and h2.

Okay, is the second clause tells us that if h2= 0,

then also g=0, right.

Finally, the last clause says that if h=1 and h2=1,

in this case, these two literals in the last clause are already falsified.

So the only way to satisfy the last clause is to set g=1.

Once again this just means that if we have a formula in which

we have these three clauses, then in many satisfying assignment

to this formula the value of g is equal to the value of h1 and h2.

And this is exactly what we need to encode in our CNF formula.

OR gates are handled similarly, namely if g is an OR

gate, we write down the following three clauses.

The first one says that if h1 = 1,

then this is already falsified, then g must be equal to 1.

If h=1, then g=1.

This corresponds to the second clause.

Finally, if h1=0, and

h2=0, then g=0.

Again in any satisfying, for a formula that contains

the following three clauses, g=h1 or h2.

Finally for an output gate, for the output gate there is a single such gate.

In a circuit we write down a clause containing just one variable or

just one literal corresponding to this gate.

This corresponds to the fact that we would like this gate to be equal to 1.

We would like our circuit to output the value 1.

The reduction is now complete.

We constructed a CNF formula out of a given circuit,

with the following property.

In any satisfying assignment of the result in CNF formula.

The value of the variable g corresponds.

It just equals to the value of the gate g on the corresponding

assignment of the inputs to this circuit.

This in turn means that the resulting formula is satisfiable if and

only if the initial circuit is satisfiable.

In particular given a satisfying an assignment for the CNF formula, just

by reading the values of the inputs of the variables that corresponds to the inputs

of the circuit, we get a satisfying assignment for the initial circuit.

It is also clear that the running time of this reduction is polynomial.

Because we just consider all the gates of the initial circuit.

And for each such gate, we write down at most three clauses.

Explore nosso catálogo

Registre-se gratuitamente e obtenha recomendações, atualizações e ofertas personalizadas.

O Coursera proporciona acesso universal à melhor educação do mundo fazendo parcerias com as melhores universidades e organizações para oferecer cursos on-line.

© 2018 Coursera Inc. Todos os direitos reservados.

Baixar na App Store

Baixar no Google Play