This practical is a mixture of problem-solving and playing with logic-based software. Some of the problems are exercises from AIMA or adaptations thereof.
They are here.
Consider the graph colouring problem with 2 colours on the following graph: A-B-C. It is not difficult for you to see that this is doable. Nonetheless your task here is to encode the problem as a CNF so that the DPLL algorithm could be used to determine that the problem is solvable. Draw out a search tree for DPLL (just do it on paper, you don't need to hand it in.) Which heuristic is particularly helpful for this problem?
Once you have done that consider the problem with the edge A-C added to the graph. Again draw out the DPLL search tree.
I know everything works in Linux so switch if you are not running Linux already.
To check that all is well, grab the example file sample.cnf and do:
/usr/course/arin/bin/ubcsat -alg walksat -i sample.cnf -solve
Here you were asking to use the walksat algorithm on the problem instance sample.cnf; the "-solve" asks that if a model is found it is output.
Have a look at sample.cnf. The lines starting with a "c" are comments. There is then a single line stating how many symbols and how many clauses there are. Each other line is a clause. Each propositional symbol is a number. A negative sign indicates "not", i.e. a negative literal and the 0 at the end is just a delimiter.
Construct (in this format) a CNF for each of the two graph colouring problems above. That's right you have to just type in the clauses using your favourite text editor. Ask WalkSAT to solve them for you.
Grab some graph colouring examples from the SATLIB Benchmark problems page. Experiment with different settings of the 'cutoff' and 'runs' parameters. (Type "ubcsat -hp" for information on parameter settings.)
This is not really an exercise it is meant to introduce you to first-order reasoning by example. I know everything works in Linux so switch if you are not running Linux already.
Recall that graph colouring using propositional logic is cumbersome. To see the advantages of a first-order approach. Do the following.
?- [graphcol]. % graphcol compiled 0.00 sec, 3,240 bytes true. ?- ok([a,b,c],[a-b,b-c]). true ?- ok([a,b,c],[a-b,b-c,a-c]). false.
Last modified: Tue Feb 14 09:58:29 GMT 2012