Using SAT-solvers

Loading...

來自 University of California San Diego 的課程

Advanced Algorithms and Complexity

248 個評分

University of California San Diego

Advanced Algorithms and Complexity

248 個評分

課程 5（共 6 門，Specialization 数据结构与算法）

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.

從本節課中

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

與講師見面

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 conclude with showing how to use SAT-solvers in practice.

Namely we give a toy, example a toy application we're going to use SAT-solvers

to implement a very simple Sudoku solver.

Recall that there is a huge gap between theory and practice of SAT solving.

Namely, currently we did not know how to prove that SAT can be solved in less

than two the n steps.

Namely, we have now example of an algorithm with the running time,

polynomial in the size of the formula times 1.99, for example,

to the n, where n is the number of variables of the input formula.

It is on one hand.

On the other hand we have state of the art SAT-solvers that can

handle instances that arise in practice that contain thousands and

even millions of variables in less than one second.

This suggests the following way of solving hard combinatorial problems in practice.

First you might want to reduce your problem to a satisfiability problem.

The structure of the satisfiability problem allows to do this very naturally

for many problems arising in practice.

We will see this on an example of solving Sudoku puzzle.

Then just use one of the efficient programs,

efficient SAT solvers that are already implemented.

There are many of them, and as I said they are very efficient.

Let me now recall you what a Sudoku puzzle is.

So in this case we are given a 9 x 9 grid which is partially filled by

digits from 1 to 9.

And our goal is to fill all the vacant places with digits so

that each row and each column and each of nine 3 x

3 blocks contain all the digits from 1 to 9.

This is an example of such a puzzle and

this is a solution that we're looking for in this case.

So now that for example in this row we have all digits from 1 to 9 and

also in this column and also in all of these nine 3 x 3 blocks.

So given a Sudoku puzzle we are going to construct

a satisfiable CNF formula such that from its satisfying

assignment we can construct the solution for the initial puzzle.

For this we are going to use the following Boolean variables.

There will be 9 x 9 x 9 of them.

Namely for each possibly values of i, j, and k, where i, j, and

k are at least 1 and at most 9, the variable xijk = 1 or

is equal to true, if the cell [i,j] contains the digit k.

Okay?

So these are Boolean variables.

There are 9 x 9 x 9 of them, which is roughly 700.

In our reduction, we will need a few times the several technical thing.

Assume that we have a few literals and we need to state

a formula which expresses the fact that exactly one of this literals is true.

We show here how to do this for three literals but

it generalizes easily for arbitrary number of literals.

So assume that we have three literals and

we want to express the fact in a CNF formula that exactly one of them is true.

So first we write down a clause that says then at least one of them is true,

this says l1 or l2 or l3.

Then we need to say also the constraints,

the value of these variables to satisfy the following property.

At most one of them is true, namely,

we need to forbid any two of them to have value 1 simultaneously.

We do this by adding a bunch of clauses of length two, namely for

any two different literals from our set,

we add two clause containing negations of these two literals.

For example, this one the first clause says

that it is not possible to assign the value 1 to l1 and l2 simulationously.

The second one says that we should not assign the value 1 to the first and

the third literal.

And, finally, the last one says that we should not assign the value 1 to

the second and the third literal..

So, finally, when we write down such a formula, then in any satisfying

assignment to this formula exactly one of l1, and l2 and l3 is true.

And also, it generalizes easily to any number of literals.

So we first right down the long clause containing all the literals and

then so that will contain k literals.

And then we write down roughly k squared literals

namely k choose 2 clauses that contain all pairs of negated literals.

We now write down the corresponding constraints.

First of all, for every values of i and j from 1 to 9, we state that in the cell [i,

j], there is exactly one digit, so it looks as follows.

So, this is a cell [i, j] in our grid and

we say that exactly one of the variables xij1, xij2 and so

on, xij9 should be assigned the value true.

So, if xij, for example, if xij4 is equal to true,

this means that we are going to put the digit 4 into this cell.

Then we need to state that for each values of k and

i, the row i contains exactly one occurrence of k.

This is done as follows.

We state that for each i and k, exactly one of the following variables is true.

So it is either xi1k or xi2k.

So this corresponds to the fact that either the first column in

the ith row contains k's or the second column or the last column.

Namely, if this is the ith row either this cell contains k or

this cell contains k and so on, the last cell contains k.

Then we do the same for column j and namely for each values of k and

j we state the fact that the column j contains exactly one occurrence of k.

We then need also to state that each of nine 3

x 3 blocks contains one occurrence of the digit k.

Again, we use the corresponding nine variables to say that

exactly one of them is equal to true.

Finally the last type of constraint is that when some cell is already filled.

If we have an instance where the cell [i,

j] already contains the digit k, we then we need just one clause

stating that the corresponding variable must be equal to true.

We know that it is already true, so we just add a single unit clause.

So the resulting formula contains about 2 to the 700 variables, so

the search space of all

possible candidate solutions in this case contains roughly ten to the two hundred.

So this is a huge search space.

It is certainly not possible for modern computers

to go through all possible candidates for a solution in this case.

At the same time, modern SAT-solvers solve the results in formula in blink of an eye.

We will see now.

We are going to use a mini SAT-solver for solving our Sudoku puzzle.

Before writing down the reduction let me show you the input format for

this SAT-solver.

So the formula is given in the following symbol format.

The first line here shows that our formula has 2 variables and 3 clauses.

Then each of the following three lines define a clause.

The first clause contains two variables, x1 and x2.

The second clause contains the variable x1 and the negation of the variable x2, so

minus x2 means the negation of the second variable.

Finally as the last clause contains two variables,

the negation of x1 and the negation of x2 okay?

So now let's call minisat on this formula, so

it reports immediately that it is satisfiable.

Now let's make it unsatisfiable, so for this we add the false clause.

-1, 2, 0, okay.

Let's call minisat again.

Yeah, in this case, the formula is unsatisfiable of course.

Now finally let me show you the code of an actual reduction that produces the CNF

formulas and then calls in minisat solver and then reads the solution for

a given Sudoku puzzle from a satisfying assignment to these formula.

So this is a simple code in Python, this gives the initial

Sudoku puzzle and then we create a list of clauses.

Then we just use variable digits which contains all the digits from 1 to 9.

The following method just returns a unique integer number for every variable.

We need this in order to give a formula to a minisat solver.

Then we have a method which, given a list of literals writes down clauses

that express the fact that exactly one of these literals is equal to true.

Namely, we first add a clause that contains all the literals

in the list literals, then for all pairs of literals

we add a clause containing two negated literals from this list.

As we've discussed already this expresses the fact that exactly one of them

is equal to true.

We then start writing down clauses expressing that each cell contains

exactly one digit.

Namely, for all pairs of digits we write down a clause stating that at least,

for all pairs of i and j, we write down the clause saying

that the cell [i, j] contains exactly one digit.

So the corresponding variable xijk is equal to 1 for exactly one value of k.

Then we say that k appears exactly once in row i.

For this we consider all possible values of i and

k and state that exactly one of the variables i,

j, k is equal to true for all possible values of j.

Then we say the same for columns, and then we say the same for blocks.

Namely, we can see that all possible starting position of blocks 1, 4, and 7.

And then for each such block and for each k we state

that each such block contains exactly one occurrence of k.

Then we read the input puzzle.

Namely, we read all the cells and if the corresponding cell is

specified, then we just add a unit clause containing exactly

one corresponding variable.

Finally, we write down all the clauses.

Namely, we open a file, tmp.cnf,

in the first line we write, p cnf, followed by the number of variables.

In our case it is roughly 1,000 and then the number of clauses.

Then for each clause which is currently in our list of clauses we first append 0 to

satisfy the format which is accepted by the mini-SAT,

and then we just write down this clause.

Then we call the MiniSAT SAT-solver,

give it the formula tmp.cnf and also indicate the file tmp.sat,

where it will write down the satisfying assignment, okay?

Then we open the satisfying assignment file and read the first line.

If it is UNSAT, we just report that the formula is unsatisfiable.

If the first line is SAT, we know that the formula is satisfiable and

we know that then the second line will be followed by a satisfying assignment.

At this line we read the corresponding satisfying assignment and

then we parse it.

We just see that if

the corresponding variable in this assignment we print it, okay?

So and this is basically all, this completes all reduction.

So let's see what happens.

If we call this Python script

it will immediately find an answer.

So this is an answer for our initial puzzle.

Let me also make a small sanity check.

Let me tweak a little bit this puzzle.

Let me put 5 here.

Then the corresponding puzzle will be for

sure unsatisfiable just because now the first line contains

two occurrences of 5 so it is not possible to complete this puzzle.

Okay, now let me call it once again so in this case, the corresponding

formula is unsatisfiable and our scripts reports that there is no solution.

As you can see, it works in just the blink of an eye.

And you can feed your favorite Sudoku puzzle into this script to see how

fastly the mini SAT-solver will solve this puzzle.

探索我們的目錄

免費加入並獲得個性化推薦、更新和優惠。

Coursera 致力於普及全世界最好的教育，它與全球一流大學和機構合作提供在線課程。

© 2019 Coursera Inc. 保留所有權利。

通過 App Store 下載

通過 Google Play 獲取