超大文件排序

16:00
我报的错是 /tmp/sortA3aLjF: No space left on device。直接用HPC无法解决gigabyte级别的排序问题了，估计得用外排序做。晚点po结果
19:30
其实bash里面的sort是可以做到的。因为这个sort本来就是n路merge外排序。默认临时文件存在/tmp目录下。因为我的/tmp目录下空间不足，所以会报错。使用-T换至自定义的路径即可

http://vkundeti.blogspot.com/2008/03/tech-algorithmic-details-of-unix-sort.html
http://www.linuxquestions.org/questions/linux-newbie-8/sort-big-files-tmp-sorta3aljf-no-space-left-on-device-823971/

Fast-forward to other forks

For convenience to develop and not to mix with my original project (Moonlyt/Moonlyt) in the team, I forked the project to my own repository (Wenling/Moonlyt) and do local development. But actually I have no idea how to keep my repo up-to-date with the original one, and this brought me a lot of trouble like I have to clone one to my local path then delete the old one of mine...

It's quite easy to reserve my own branch.

Reference:
http://git-scm.com/book/en/Git-Branching-Basic-Branching-and-Merging

# switch to a new branch
git checkout -b upstream/master
# bind the branch to the remote original one 
git remote add upstream git://github.com/moonlyt/moonlyt.git
# usually fetch is better as it don't automatically implement the merge command for 
# you. Pull request for update from original (upstream) to my repo (master)
git pull upstream master
# switch to my master branch
git checkout master
# merge upstream and my master branch
git merge upstream/master
# push 
git push origin master




ctrl-z和ctrl-c都是中断命令,但是他们的作用却不一样.
ctrl-c是强制中断程序的执行,
ctrl-z是将任务中断,但是此任务并没有结束,他仍然在进程中他只是维持挂起的状态,用户可以使用fg/bg操作继续前台或后台的任务,fg命令重新启动前台被中断的任务,bg命令把被中断的任务放在后台执行.
恢复挂起的程序命令：
1、用jobs 查看被挂起程序的序号x
2、用fg %x 恢复被挂起程序（如果只有一个被挂起程序，那直接fg就可以恢复了）

DPLL implemented with c++

First C++ code written... I think it's quite efficient with all the test set included in path data.

The simplest data set looks like:
-1 -3 0 -1 -5 0 -3 -5 0 -2 -4 0 -2 -6 0 -4 -6 0 1 2 0 3 4 0 5 6 0

used vector saving clauses and map saving assignments.
the main recursive function looks like following:
/*
1. If the set of clauses is empty, it returns true
2. Otherwise, if the set of clauses contains an empty clause, it returns false
3. Otherwise, if there is a unit clause, it applies unit propagation and then calls itself recursively
4. Otherwise, if there is a pure literal, it applies the pure literal rule and then calls itself recursively
5. Otherwise, it applies either the resolution rule or the splitting rule and calls itself recursively
*/

Git Repo: git@github.com:Wenling/DPLL-Algorithm.git
Google Drive: https://docs.google.com/file/d/0B0mZhauSOmW4dFZESVRtMGRpWms

DPLL Algorithm with ML

Git Repo: git@github.com:Wenling/DPLL-Algorithm.git
There are three satisfiability-preserving transformations in DP.
• The 1-literal rule
• The affirmative-negative rule
• The rule for eliminating atomic formulas
The first two steps reduce the total number of literals in the formula.
The last step reduces the number of variables in the formula.
By repeatedly applying these rules, eventually we obtain a formula containing an
empty clause, indicating unsatisfiability, or a formula with no clauses, indicating
satisfiability.


The DPLL algorithm replaces resolution with a splitting rule.
• Choose a propositional symbol p occuring in the formula.
• Let delta be the current set of clauses.
• Test the satisfiability of delta and {p}.
• If satisfiable, return true.
• Otherwise, return the result of testing delta and {¬p} for satisfiability.

Brute Force SAT Solver with Scheme

Produced some code solving the SAT problem with scheme, a functional language. It's not perfect and might caused the application to crash when the number of literals of an assignment is more than 25.. One problem is the allassign function: it will save much more space with tail recursion.. But I was too lazy to change my code.

#lang racket

;counts the the number of clauses
(define (countclauses data)
  (cond
    ((null? data) 0)
    ((= (car data) 0) (+ 1 (countclauses (cdr data))))
    (#t (countclauses (cdr data)))))

;determines the maximum variable number
(define (maxvar data)
  (cond
    ((null? data) 0)
    (#t (let* ((max (maxvar (cdr data)))
               (c (car data))
               (a (if (< c 0) (- c) c)))
          (if (> a max) a max)))))

;takes a single argument, a list of integers representing a SAT problem in DIMACS format,
;and returns a list of lists, where each list represents a clause.
(define (getClauses lis)
  (saveClause lis '()))

(define (saveClause lis temp)
  (cond 
    ((null? lis) '())
    ((zero? (car lis)) (append (list temp) (saveClause (cdr lis) '())))
    (else (saveClause (cdr lis) (cons (car lis) temp)))))

;takes a positive integer n and generates all possible assignments of length n.
(define (allassign num)
  (allassign2 num '(())))

(define (allassign2 num temp)
  (cond
    ((zero? num) temp)
    (else (append (allassign2 (- num 1) (list (cons #t (car temp)))) (allassign2 (- num 1) (list (cons #f (car temp))))))))

;takes a variable and a list representing an assignment
;returns the value of that variable under that assignment
(define (eval-var var lis)
  (cond 
    ((eq? var 1) (car lis))
    (else (eval-var (- var 1) (cdr lis)))))

;similar function to evaluate a literal
(define (eval-lit var lis assgn)
  (cond
    ((eq? var 1) (if (< (car lis) 0) (not (eval-var (opposite (car lis)) assgn)) (eval-var (car lis) assgn)))
    (else (eval-lit (- var 1) (cdr lis) assgn))))

(define (opposite var)
  (if (< var 0) (- 0 var) var))

;evaluate a clause
(define (eval-clause var lis assgn)
  (cond
    ((eq? var 1) (eval-clause2 (car lis) assgn))
    (else (eval-clause (- var 1) (cdr lis) assgn))))

(define (eval-clause2 lis assgn)
  (cond
    ((null? lis) #f)
    ((eq? #t (eval-lit 1 lis assgn)) #t)
    (else (eval-clause2 (cdr lis) assgn))))

;evaluate a CNF
(define (eval-form lis assgn)
  (cond
    ((null? lis) #t)
    ((eq? #f (eval-clause 1 lis assgn)) #f)
    (else (eval-form (cdr lis) assgn))))

;main function, determines whether a list of integers is satisfiable
(define (sat lis)
  (SATsolver2 (getClauses lis) (allassign (maxvar lis))))

(define (SATsolver2 lis assgn)
  (cond
   ((null? assgn) #f)
   ((eq? #t (eval-form lis (car assgn))) #t)
   (else (SATsolver2 lis (cdr assgn)))))

SAT Solver

In computer science, satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE.

SAT was the first known example of an NP-complete problem. That briefly means that there is no known algorithm that efficiently solves all instances of SAT, and it is generally believed (but not proven, see P versus NP problem) that no such algorithm can exist.

3-satisfiability is a special case of k-satisfiability (k-SAT) or simply satisfiability (SAT), when each clause contains exactly k = 3 literals.

3-SAT is NP-complete and it is used as a starting point for proving that other problems are also NP-hard. This is done by polynomial-time reduction from 3-SAT to the other problem.

EG. Subset sum problem
Assume that we are given some integers, such as {-7, -3, -2, 5, 8}, and we wish to know whether some of the integers can add up to zero. As the number of integers that we feed into the algorithm becomes larger, the number of subsets grows exponentially, and in fact the subset sum problem is NP-complete. An algorithm that verifies whether a given subset has sum zero is called verifier. A problem is said to be in NP if and only if there exists a verifier for the problem that executes in polynomial time.

Assessment with Epic

It took me 3.5h today to finish the test, from 11:00am to 2:30pm. There are three parts of the test: Math, Understanding a new language, and coding. Epic gives 5h maximum but time you use is also an evaluation.

1. Math problem. 14 of them I think. Easier than GRE quantity but has some weird questions. Mainly because I cannot understand what it is asking..
Eg. A goat jumps 3ft height per minute, and slide back 2ft per minute. If it wants to jump out of a cliff, which is 50.5ft, from the bottom. How many minutes does it take?

2. Given a new language, understand it and answer questions.
A new language is given and there are 20 questions. Not that hard at all.
Eg. the language has two forms of variables: string and integer, expressions are strictly operated left to right, boolean expressions. Variables are not declared type explicitly.
Functions like SET, READ, KILL.

3. Programming skills.
1) Long Subtraction -- Given two arrays A, B, each contains elements of digits, return an array of A - B. Your machine can only do calculation of less than 20.
eg. A = [1,2,5,7,5];
B = [3,4,8,9];
A - B = [9,0,8,6];

2) I forgot

3) Given a keyboard with every letter maps a digit from 0 to 9, return all possible permutation of given a n digit number.

eg. 0 <- z,a,q,x,s,w
1 <- c,d,e
2 <- v,f,r
3 <- b,g,t
...
Then permutation of num 1230 will be:
cvbz
cvba
cvbq
...

4) There is one kind of numbers call Fibonacci number (forgot the specific name), which satisfy the following situation:
A. can be spilt into several numbers;
B. The first two number are the same, the next number is equal to the sum of previous two
eg. 112 (2 = 1 + 1), 12,122,436(12 + 12 = 24, 12 + 24 = 36)
If you are given a range by the user, print all numbers that are Fibonacci number in the range.

I finished the first and second part with less than 1h, while Epic gives more than 2h to do. But I cannot finish question 4 on time, even though I was given more than 110 min...