Author: Chris Murphy
Note: We spent a large portion of time at the beginning of class handling questions about Problem 5 on the written problem set before moving onto new material. The question and notes are replicated to some extent below, but were discussed more in a Q+A format than as a specific set of new information. The problem is replicated for reference at the bottom of the first section.
The Infamous Problem Five
A Review
Recall on a previous exam a question about building a queue from two stacks: smoke and mirrors. The goal was to determine how to enqueue and dequeue items using only stack operations. The type of thinking that went into solving that problem could prove useful to solving problem 5.
Question from Katie Rivard:
That problem was different, in that both the queue's and stacks' functions deal with adding and removing items from a data structure. In this case, we are trying to convert a boolean value (IsSatisfiable) to specific values for each of the variables in our equation.
Answer from Lynn:
You should assume that you can manipulate the formula you are given, and set values for the variables.
Comment from Sarah Zwicker:
The question is not about converting the SAT problem to something else, it's about setting up infrastructure to keep track of what solutions work.
The Actual Problem
Suppose that someone gives you a polynomial-time algorithm to decide formula satisfiability (i.e., given a propositional logic formula, is there some truth assignment that makes it true or does no such truth assignment exist?). Describe how to use this algorithm to find satisyfing assignments -- i.e., to identify one such truth assignment -- in polynomial time.
What you are given is a procedure -- say, IsSatisfiable -- that takes a boolean formula as an argument and returns either yes (if the argument formula is satisfiable) or no (if it is not). IsSatisfiable does not take truth assignments along with its formula or return truth assignments. For example:
IsSatisfiable( p ^ not( p ) )
IsSatisfiable( (p v q) ^ (not(q) v r) ^ (p ^ not(r)) )
would return true, because both the truth assignment {(p, true), (q, false), (r, true)} and the truth assignment {(p, true), (q, false), (r, false)}make (p v q) ^ (not(q) v r) ^ (p ^ not(r)) true. However, IsSatisfiable doesn't produce {(p, true), (q, false), (r, true)} or {(p, true), (q, false), (r, false)}; it just answers yes.
Your task is to come up with a way to find satisfying truth assignments. Like IsSatisfiable, your procedure should take a boolean formula as an argument. Unlike IsSatisfiable, your procedure will return a truth assignment. Because your method needs to run in polynomial time, you will need to make use of the magic IsSatisfiable polynomial-time decision procedure. Your method may call IsSatisfiable on any boolean formula you want. You may call IsSatisfiable more than once. You may, however, only call it a polynomial number of times. (Calling it an exponential number of times would make your procedure exponential even if IsSatisfiable` works its magic in polynomial time.)
Your answer should consist of a pseudocode algorithm (which is allowed to call IsSatisfiable( boolean_formula ) up to a polynomial number of times) as well as an informal English argument that this algorithm runs in polynomial time (assuming that IsSatisfiable does).
K-Cliques
Definition
A K-clique is a completely connected subgraph of a larger graph. For instance, the graph below has a K-clique of size 3 (several, actually), as well as a K-clique of size 4. It does not have a K-clique of size 5 (A 5-Clique). The problem of finding a given sized clique in a graph is NP-Complete.
o-----o |\ /|\ | \ / | \ | X | o | / \ | / |/ \|/ o-----o
3-CNF
If we have a formula in Conjunctive Normal Form (CNF), in triplets (3-CNF). Deciding whether a given formula is satisfiable (known as the 3-SAT problem) is also NP-Complete.
Rhetorical Question: If we are given a magic bullet which can solve the k-clique problem, can we solve 3-SAT as well?
Answer: Of Course!
Assume we have the 3-CNF equation (X v Y v Z) ^ (A v X v X!) ^ (E v Y! v Z) ^ (Z! v Q v X) where X! is 'X-bar'. We begin by laying out the graph as shown below:
Z! Q X X E Y Y! Z Z A X X!
Essentially, you take each triplet in the 3-CNF notation, and start by simply grouping them as sides of a polygon shaped graph. Next, connect everything which is NOT from the same side of the polygon (ie - the same triplet) and which also does NOT directly conflict (for instance, don't connect X to X!). This is a serious amount of lines. I have attempted to draw in all the lines which connect to the top-left X node -- I realize it's sorta cluttered. You would repeat this process for each node in the graph.
Z! Q X / /-----/ /---/ X<---/-----/ -----E \\\----------/ \\\\ Y | \\\-------------Y! | | \ | \ \----\ Z | \ \------Z | \-| A X X!
The Punchline
If a 4-clique exists, we have solved the 3-SAT problem. If we find a 4-clique in our graph, we must have 4 independent clauses that are true (one in each triplet) and which don't contradict.
What We Did This Semester
The work we did this semester can be divided into three topics:
- Complexity, Computability and Automata Theory
- Algorithms and Data Structures
- Programming Languages
Example Topic
The below diagram shows what areas of CS topics associated with SWOOGLE, the Semantic Web Google, would fall into.
Algorithms Automata Programming Languages ------------------------------------------------------------------------------------------- Stacks Trees (and Traversal) Parsing(Grammar) | PROLOG+LISP ------ Hash Table Queue Regular Expressions / Propositional Logic / Arrays Order statistics Graphs / Predicate Calculus / Sorting (n log n) Finite State Machines / Turing Machines / / lambda Calculus Computability ------------------------------------------------------------------------------------------- THETA(1) THETA(log n) THETA(n) Tractable -------> NP - Expensive! Intractable
Note that lambda Calculus is the formalism behind Lisp - we did not talk about it under the name "lambda calculus".
References
Wikipedia was used extensively for supporting documentation - it is linked from the sections where appropriate.