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.
To sign up for an accound at the SVN server,
first make sure to be logged in at
kth.se. Then go to
svn.csc.kth.se
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
https://svn.csc.kth.se/~jakobn/ScribeNotes/DD2442/
(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.
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
www.minisat.se.
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.
For our purposes, all we need to know about the DIMACS format is
the following (simplified) description.
The example formula
(x
∨
y)
∧
(¬y
∨
z)
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.
