COMPUTER SCIENCE TRIPOS Part IB – 2021 – Paper 6
Artificial Intelligence (sbh11)
A Boolean satisfiability problem has four variables, x1, x2, x3 and x4. A literal l
can be a variable or its negation, denoted l. The formula of interest, in conjunctive
normal form (CNF), is
f = (x2 ∨ x3) ∧ (x2 ∨ x3) ∧ (x1 ∨ x2 ∨ x4). (1)
The aim is to find assignments to the variables such that f is true under the usual rules
for Boolean operations. This question addresses the use of more general constraint
satisfaction to solve this problem.
(a) Give a general description of a constraint satisfaction problem (CSP).
[3 marks]
(b) Explain how a Boolean satisfiability problem in CNF form and with n variables
can be converted to a CSP, also having n variables and having a suitable
constraint for each clause. Illustrate your answer using the 4-variable formula f
in (1). [3 marks]
(c) Explain, again using a constraint corresponding to a clause from (1), how general
constraints can be converted to binary constraints. Provide a graph illustrating
the problem from (1) after it has been converted to a CSP with only binary
constraints. [4 marks]
(d) Explain, how forward checking works in the context of a general CSP. How does
this benefit a CSP solver? [3 marks]
(e) Using the CSP equivalent you developed for (1), with only binary constraints,
demonstrate how forward checking works using the sequence of assignments
x1 = F, x2 = F, x4 = T. [5 marks]
(f ) How would you expect the solution obtained when applying forward checking to
be affected if constraints were allowed to propagate more widely? [2 marks]