Introduction to Artificial Intelligence (ARIN)

Logic Practical


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.

  1. Logic exercises
  2. Graph colouring
  3. Fun with WalkSAT
  4. First-order reasoning by computer

ANSWERS


Logic exercises

They are here.


Graph colouring

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.


Fun with WalkSAT

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.)


First-order reasoning by computer

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.

  1. Grab this file. It is in Prolog ("programming in logic"), a language I assume you have not met before. Have a look at it, but don't worry about understanding it properly. To get at least a rough idea of what is going on note that ":-" should be read as "<-", and that symbols with capital letters are variables and others are constants. The program basically states that the graph is "ok" (i.e. colourable) if there is a colouring which is ok. The key point is that this program will work for any input graph, the representation is not tied to a particular graph.
  2. Type "swipl" into the Linux command line.
  3. Do the following, where stuff after the "?-" is what you type. The first input from you just causes the file to be read in. The other two inputs ask about whether it is possible to colour graphs. The graphs are given in the form vertices followed by edges.
    ?- [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.
    
  4. Do at least two more experiments with the system by varying the number of colours and trying out different graphs.

Last modified: Tue Feb 14 09:58:29 GMT 2012

Valid XHTML 1.1!