This post is just to explain the CNF DIMACS file format to people new to SAT
Boolean Operators
V – OR
^ – AND
¬ – NOT/Negation
Variable – can assume only values either 1 (true/ON) or 0 (false/OFF) Clause – is the disjunction of a number of variables (negations may also be present)
A CNF expression is made up of conjunction of one or more clauses.
Every Satisfiability problem can be expressed in CNF (conjunctive normal form).
File Format
At the begining of the file there can exist one or more comment line.
comment lines start with a ‘c’
Example:
c This is a comment
c This is another comment
The following lines are information about the expression itself so an example expression is used to help understanding.
(A v ¬B v C) ^ (B v D v E) ^ (D V F)
After comments if any comes the Problem line starts with a ‘p’
p FORMAT VARIABLES CLAUSES
FORMAT is for programs to detect which format is to be expected. Which should always be ‘cnf’
VARIABLES is the count of number of unique variables in the expression
A,B,C,D,E,F
VARIABLES = 6
CLAUSES is the number of clauses in the expression
(A v ¬B v C) ^ (B v D v E) ^ (D V F)
1 1 1 = 3
results to
p cnf 6 3
This line is followed by the information in each clause
unique variables are enumerated from 1 to n
A,B,C,D,E,F
1,2,3,4,5,6
such that
1 represents A
2 represents B
3 represents C
etc…
a negation is represented as ‘-‘
e.g.
-1 represents ¬A
Each variable information is seprated by a blank space
so
(A v ¬B v C) is represented by 1 -2 3
Add a 0 behind to indicate the end of the clause
so
(A v ¬B v C) is represented by 1 -2 3 0
(B v D v E) is represented by 2 4 5 0
(D V F) is represented by 4 6 0
The final File will be
c This is a comment
c This is another comment
p cnf 6 3
1 -2 3 0
2 4 5 0
4 6 0
Some Considerations
If you are building a parser
-the final 0 is sometimes ommited.
If you are building a SAT solver
-CNF is used just to have a common way of expressing the file format your SAT solver could transform the expression in another format for a different strategy.
Further Readings
http://en.wikipedia.org/wiki/Conjunctive_normal_form
http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf
http://classes.soe.ucsc.edu/cmps132/Winter05/hw/hw8sols.pdf
Ever faced the situation where you required to copy text from a Command Prompt and ended up copying the text manually just because you bump at the dialog in Fig:1 when you attempt Alt+enter ?
Here is the solution:
Right Click My computer (Either on the Desktop or in the Windows Menu)
Click Manage as shown in Fig:2
Click Device Manager (which can be found in the Computer Management on the left of the window)
Expand Display Adapters and right click and disable your Display Adapter as shown in Fig:3 and click yes
Open the Command Prompt and press Alt+Enter and it should go full Screen
Known Issues:
Do not run anything in Admin mode or you may not proceed. ( If you happen to do it Alt+F4 till u can use the system again)
Only CMDs opened after Disabling Display Adapter are allowed to go full screen.
A couple of days ago I have posted an explanation of how to send SMS messages over My Go Account using c#. I have decided to do the same but this time using Ruby. I will not go in detail of how to since the explanation can be found here
Requirements:
GO Mobile phone line
My Go account for the phone line (Free for every GO Mobile phone)
As the title says this post describes how to send SMS messages from GO mobile website www.go.com.mt/mygo/ programmatically with C#. This is for educational purposes only and I’m not affiliated in any way to GO. Use the contents of this page at your own risk.
Requirements:
GO Mobile phone line
My Go account for the phone line (Free for every GO Mobile phone)
To send an SMS a user first has to login with his mobile number and password as shown in Fig:1
If the login is successful the user is given access to the form in Fig:2 that takes recipients and a maximum of 420 characters in an SMS. When finished typing the desired SMS click send SMS button.
How to achieve the above programmatically?
To send an SMS there are needed two POSTs, one for Login and the other for the actual SMS to be sent. So a method for sending a POST over HTTPS was created.
Post_data – is the actual data that post will carry
Referrer – is the previous url the post request originated.
cookieC –keeps the cookie the Web Server sends to the browser to maintain the Session state. This is so that to keep the program logged to your My Go account between login and sending a SMS message.
To make sure the Web Server sends the same HTML code that it sends to the Web Browser, the UserAgent is spoofed to the same as the Web Browser used in this case FireFox 5.
Note: the HTML code was cleared from irrelevant tags for clarity. The tags removed include table for formatting and client side validation on the form data.
From the HTML code at https://www.go.com.mt/mygo/ we investigate the login form.
Development becomes easier with the use of Temper Data which empowers the developer to pause and inspect requests and their content. With some manual SMSes testing the query string was figured out.
The code was tested in Visual Studio 2010 in a Console Application the Target Framework was changed to .NET Framework 4 as shown in Fig:3 so as to be able to include the reference to System.Web shown in fig:4.
Make sure the following name spaces are included
using System.Text;
using System.Net;
using System.IO;
Final note
If multiple SMS are to be sent, one could separate login from sending SMS but keep in mind that the session times out after being idle for some time.
What is not included:
Error Handling.
Message Templates.
An explanation of how to send to multiple recipients. This is left for the reader to try out. (probably just separate the numbers with coma)
How to access and retrieve My Go phone book and how to add entries to it programmatically.
Between login and sending an SMS from the website a real web browser sends some GET/POST requests for autocomplete mobile numbers in the phonebook stored in the account. These are skipped entirely.
Does not cater beyond the 8 free daily SMSes that require confirmation from the user to charge the account for the SMS.