School of
Electrical Engineering
and Computer Science

DD2442/DD3343 Seminars on Theoretical Computer Science Autumn 2016: Useful Information

On this page you find information about SVN, MiniSat, and the DIMACS format for CNF formulas.

Instructions for SVN

To sign up for an accound at the SVN server, first make sure to be logged in at Then go to and click "log in" to create your account. Note that after this you need to notify the instructors in order to get access to the SVN repository used for storing scribe notes. The instructions below assume that you have done so and that the instructors have confirmed that you have been granted access.

The main instructor mostly uses SVN in Windows with the Tortoise SVN client, which is very intuitive with menu items included in the drop-down menus in the file manager. Probably similar programs exist for Mac and Linux. But it is also perfectly possible to use SVN on the command line in Ubuntu, and below follow some instructions for this.

To check out the repository, do svn checkout (this is case-sensitive). You will need to enter your username and a long and cumbersome password that you should have received separately when signing up at the SVN server, but if you ask your SVN client to store it you will never need to enter it again.

To get updated files from the repository, do svn update. Always update before storing your own changes in the repository.

To specify that a new file should be included in the repository (for instance, a figure for the lecture notes or similar), do svn add <filename> (otherwise the file will just be a local file in your particular directory). The added file will be included in the repository next time you commit changes to the repository (see next paragraph).

To commit your own changes to files in the repository, do svn commit. Chances are that you will get a small window with your favourite editor where you are supposed to add a log comment, but you can also add this comment on the command line by adding the option -m <my message here>. Please do provide log messages, and make sure to make them descriptive. In particular, if you are reviewing someone else's scribed lecture notes, or contributing improvements in general, please make sure to describe your edits.

To remove a file from version control, do svn delete <filename>. The file will be removed from the repository at the next commit.

When scribing, please make sure not to modify any files in the Auxiliary or TemplateFile directories, but only in the directory Lecture<XX> for the lecture you are contributing to.

Doing svn help provides more general info and svn help <command> provides information about <command>.

Please do not hesitate to ask at Piazza if you run into any problems with SVN.

Some Information About MiniSAT

There should be a version of MiniSAT available on all Ubuntu Linux machines at KTH CSC using the command minisat. Please send an e-mail to KTH IT support if this does not work to you (and please do not hesitate to let the instructors know if the IT support is not responding promptly).

If you want to play around with MiniSAT on your own computer, you can download and install the solver from the webpage

The suggested way of running MiniSAT is to do minisat <CNF formula file> <output file>. MiniSAT will then read the CNF formula in DIMACS format from the input file and report the result on the output file. If the solver determines that the formula is unsatisfiable, it writes UNSAT. If it finds the formula to be satisfiable, it writes SAT followed by the signs of the variables (positive=true, negative=false) in a satisfying assignment.

Doing minisat -h will give a list of some MiniSAT options.

Some Information About The DIMACS Format for CNF Formulas

For our purposes, all we need to know about the DIMACS format is the following (simplified) description. The example formula

(xy) ∧ (¬yz)

can be coded in DIMACS format as the following file:

c All of this line is a comment
c This an encoding of the CNF formula mentioned above
p cnf 3 2
1 2 0
-2 3 0
Or in words:
  • The file can start with comments, which are lines beginning with the character c.
  • Then follows a line p cnf <nvars> <nclauses> specifying the exact number of variables and clauses in the formula.
  • After this the clauses follow, one per line, where each line is a list of integers of absolute value at most <nvars> terminated by 0 (zero). The variables are assumed to be indexed from 1 to <nvars> and a minus sign means negation. Zero just means end of clause.

Copyrightʩ Published by: Jakob Nordstr̦m <jakobn~at-sign~kth~dot~se>
Updated 2017-06-01