image/svg+xml
PhD Direction
Solving ProblemsbySearching for Truth
From the CSP to SAT via constraint encodings
Setting the scene
SAT solvers
SAT encodings
Machine Learning
2
1--2
1--3
2--3
2--4
2--5
3--5
3--6
4--5
4--7
4--8
5--6
5--8
5--9
6--9
6--10
7--8
8--9
8--11
9--10
9--11
1
3
4
5
6
7
8
9
10
11
12
9--12
11--12
Your challenge:Write the numbers 1 to 12 into the baubles, ensuring that:each number is used exactly once,no two adjacent baubles (nodes) have consecutive numbers, andthe three numbers in any clique add up to no more than 20.
2
1--2
1--3
2--3
2--4
2--5
3--5
3--6
4--5
4--7
4--8
5--6
5--8
5--9
6--9
6--10
7--8
8--9
8--11
9--10
9--11
1
3
4
5
6
7
8
9
10
11
12
9--12
11--12
2
1--2
1--3
2--3
2--4
2--5
3--5
3--6
4--5
4--7
4--8
5--6
5--8
5--9
6--9
6--10
7--8
8--9
8--11
9--10
9--11
1
3
4
5
6
7
8
9
10
11
12
9--12
11--12