Assignment 6: Rosette 123/Homework 1 by Christopher Peterson

Contents

• What I did
  • Question 2
  • Question 5
  • Question 6
  • Question 8
• Conclusion and Future Work

What I did

I had no prior experience with Racket at all going into this assignment. I chose to focus on the homework questions that did not require its use, since I didn't want to spend all of my time learning a new language with no results to show for it. Unfortunately, this meant that I missed out on some of the core Rosette stuff, which part of me was looking forward to experimenting with. I wasn't personally interested in the problems which required proofs (since I was rusty on the material), so I stuck with Questions 2, 5, 6, and 8. I spent a little over an hour on each question, along with some time surveying the entire assignment and looking for problems I was interested in.

Question 2

Question 2 looked fairly daunting, but doable. This took a little over an hour since I wasn't familiar with Tseytin transformation and my prepositional logic was rusty.

The problem asks us to use Tseytin transformation to get an equisatisfiable CNF version of the following:

¬(¬r → ¬(p ∧ q))

I used the following auxilery variables:

• a₁ ⟺ p ∧ q
• a₂ ⟺ ¬r → ¬a₁

Conjuncting all the substitutions:

¬a₂ ∧ (a₂ ⟺ ¬r → ¬a₁) ∧ (a₁ ⟺ p ∧ q)

Replacing the ⟺s:

¬a₂ ∧ (a₂ → (¬r → ¬a₁)) ∧ ((¬r → ¬a₁) → a₂) ∧ (a₁ → (p ∧ q)) ∧ ((p ∧ q) → a₁)

Replacing the →s in the inner part of the expression:

¬a₂ ∧ (a₂ → (r ∨ ¬a₁)) ∧ ((r ∨ ¬a₁) → a₂) ∧ (a₁ → (p ∧ q)) ∧ ((p ∧ q) → a₁)

Replacing the rest of the →s:

¬a₂ ∧ (¬a₂ ∨ r ∨ ¬a₁) ∧ (¬(r ∨ ¬a₁) ∨ a₂) ∧ (¬a₁ ∨ (p ∧ q)) ∧ (¬(p ∧ q) ∨ a₁)

Working on the (¬(r ∨ ¬a₁) ∨ a₂) term, which becomes (¬r ∨ a₂) ∧ (a₁ ∨ a₂) after Demorgan's and distributing:

¬a₂ ∧ (¬a₂ ∨ r ∨ ¬a₁) ∧ ((¬r ∧ a₁) ∨ a₂) ∧ (¬a₁ ∨ (p ∧ q)) ∧ (¬(p ∧ q) ∨ a₁)

¬a₂ ∧ (¬a₂ ∨ r ∨ ¬a₁) ∧ (¬r ∨ a₂) ∧ (a₁ ∨ a₂) ∧ (¬a₁ ∨ (p ∧ q)) ∧ (¬(p ∧ q) ∨ a₁)

Then the (¬a₁ ∨ (p ∧ q)) term, which becomes (¬a₁ ∨ p) ∧ (¬a₁ ∨ q) after distributing:

¬a₂ ∧ (¬a₂ ∨ r ∨ ¬a₁) ∧ (¬r ∨ a₂) ∧ (a₁ ∨ a₂) ∧ (¬a₁ ∨ p) ∧ (¬a₁ ∨ q) ∧ (¬(p ∧ q) ∨ a₁)

Lastly, the (¬(p ∧ q) ∨ a₁), which becomes (¬p ∨ ¬q ∨ a₁) after Demorgan's:

¬a₂ ∧ (¬a₂ ∨ r ∨ ¬a₁) ∧ (¬r ∨ a₂) ∧ (a₁ ∨ a₂) ∧ (¬a₁ ∨ p) ∧ (¬a₁ ∨ q) ∧ (¬p ∨ ¬q ∨ a₁)

I don't have a simple and fast way of verifying this solution, but I'm reasonably confident in the process that I took to reach it. It's definitely in CNF and I don't think I made any major logical missteps when simplifying it (although it's possible my best-guess Tseytin transformation was done incorrectly). I thought this was a fun problem to work through and I learned quite a bit (as well as refreshed my boolean logic).

Question 5

Question 5 looked doable. It took me around 10 minutes to set up CaDiCaL and produce cadical_output.txt using Cygwin. It took me around another hour to learn about CDCL, understand & parse the log file, and produce this writeup. For the sake of time, I'm going to describe the algorithm's process informally instead of the explicit writeup and implication graph mentioned in the homework.

The log file starts off with:

c LOG 0 checking that all clauses contain a negative literal
c LOG 0 found purely positively irredundant size 2 clause[3] 1 3
c LOG 0 checking that all clauses contain a positive literal
c LOG 0 found purely negatively irredundant size 2 clause[5] -4 -2

This step wasn't mentioned on any CDCL explanation I saw, and I'm honestly not sure what it's checking for and/or doing.

The log file then goes into the first guess, that x₁ = True. I don't understand what the watch/unwatch statements are doing, so I'll ignore those:

c LOG 0 checking increasing variable index true assignment
c LOG 1 search decide 1
c LOG 1 search assign 1 @ 1 decision
c LOG 1 propagating 1
c LOG 1 unwatch -1 in irredundant size 3 clause[1] -1 2 4
c LOG 1 watch 4 blit -1 in irredundant size 3 clause[1] 2 4 -1
c LOG 1 unwatch -1 in irredundant size 3 clause[7] -4 -1 2
c LOG 1 watch 2 blit -1 in irredundant size 3 clause[7] -4 2 -1
c LOG 1 search assign 3 @ 1 irredundant size 2 clause[9] 3 -1
c LOG 1 propagating 3
c LOG 1 unwatch -3 in irredundant size 3 clause[11] -3 -2 4
c LOG 1 watch 4 blit -3 in irredundant size 3 clause[11] -2 4 -3
c LOG 2 search decide 2
c LOG 2 search assign 2 @ 2 decision
c LOG 2 propagating 2
c LOG 2 search assign -4 @ 2 irredundant size 2 clause[5] -4 -2
c LOG 2 ignoring lucky conflict irredundant size 3 clause[11] -2 4 -3
c LOG 2 backtracking to decision level 0 with decision 0 and trail 0
c LOG 2 unassign 1 @ 1
c LOG 2 unassign 3 @ 1
c LOG 2 unassign 2 @ 2
c LOG 2 unassign -4 @ 2
c LOG 2 unassigned 4 literals 100%
c LOG 2 reassigned 0 literals 0%

It's clear that x₃ = True due to the (x₃ ∨ ¬x₁) clause. This would add (x₁ = 1) → (x₃ = 1) to the implication graph.

The solver then guessed that x₂ = True. This meant that x₄ = False due to the (¬x₄ ∨ ¬x₂) clause. This would add (x₂ = 1) → (x₄ = 0) to the implication graph.

These assignments led to a contradition, as the (¬x₃ ∨ ¬x₂ ∨ x₄) clause is no longer satisfiable. This causes the solver to backtrack all the way to the start.

The solver then tries x₁ = False:

c LOG 0 checking increasing variable index false assignment
c LOG 1 search decide -1
c LOG 1 search assign -1 @ 1 decision
c LOG 1 propagating -1
c LOG 1 search assign 3 @ 1 irredundant size 2 clause[3] 1 3
c LOG 1 search assign 4 @ 1 irredundant size 2 clause[13] 1 4
c LOG 1 search assign -2 @ 1 irredundant size 2 clause[15] -2 1
c LOG 1 propagating 3
c LOG 1 propagating 4
c LOG 1 propagating -2

The solver finds that x₃ = True due to the (x₁ ∨ x₃) clause. This would add (x₁ = 0) → (x₃ = 1) to the implication graph.

The solver then finds that x₄ = True due to the (x₁ ∨ x₄) clause. This would add (x₁ = 0) → (x₄ = 1) to the implication graph.

Lastly, the solver finds that x₂ = False due to the (¬x₂ ∨ x₁) clause. This would add (x₁ = 0) → (x₂ = 0) to the implication graph.

These assignments do not produce a contradiction and are taken as the proof that the problem is satisfiable. Overall, I enjoyed walking through this process and learning the mechanics behind boolean satisfiability solvers. I think it's interesting that the solvers operate on a (vastly optimized) guess-and-check framework.

Question 6

The rest of the problems seemed to rely on Question 6. This problem took me around an hour to figure out, with the time evenly spent across the problems.

Github's markdown isn't the best, but I'll be using the variable p_v^c to represent color(v) = c.

1. A single vertex being colored could be represented as an OR of it being each of k colors: (p₁¹ ∨ p₁² ∨ ... ∨ p₁^k). These can be AND'd together n times to make sure each vertex has at least one color.
2. Two vertexes being different colors could be represented by (¬p_u^a ∨ ¬p_u^b), AND'd together for every vertex u in V and every pair of colors a, b (where a and b aren't the same) in C.
3. Both vertexes being the different colors would be represented by (¬p_w^c ∨ ¬p_v^c), AND'd together for every edge (v, w) pair in E and every color c in C.
4. From a purely satisfiability perspective, I think the limit on colors per vertex is unnecessary. Multi-coloring a vertex purely makes the problem harder (could just single color it any of the chosen colors instead). Therefore, we do not need to enforce it using constraints, as an optimal solution will just avoid the optional multi-coloring when it is necessary to do so, not changing the satisfiability at all.
5. My constraints are already in CNF. The first one uses |V|k variables and |V| clauses. The third one uses 2|E|k variables and |E|k clauses. Together, they use |V|k + 2|E|k variables and |V| + |E|k clauses.

I'm not sure these are all correct (particularily part #5), but I think I have the general idea correct. This was a fun problem to think about, especially part #4.

Question 8

I spent around another hour thinking about Question 8, as it was the next logical step up from Question 6. I couldn't come up with an answer, but I had some interesting ideas which may have materialized into an answer with more time or more knowledge about the k-coloring problem.

I mostly thought about the second part of this problem: reducing the edge variables and clauses to |E|log(k). This felt somewhat possible, where the base of the logarithm might be related to the average connectivity of the graph, and the relationship would more directly model the fact that all connections from a vertex v must have a different color than v. I considered something along the lines of:

p_v^c → ¬(p₁^c ∨ p₂^c ∨ ... ∨ p_w^c)

Which basically says that if a node is a certain color, all of its neighboring nodes must be different colors. While this is a bit smarter, it doesn't avoid the fundamental issue of having to check the condition for every single color in the graph.

Ultimately, I suspect that the answer lies with more pre-determined color choices. I think that instead of giving every vertex an abitrary color (0, 1, 2, ..., k), you could give a vertex the lowest number possible. This would reduce the number of times colors must be checked and potentially hit the log(k) goal.

Overall, this problem was very interesting to think about and try ideas for, even if I didn't get too far. I'd be interested to see the solution.

Conclusion and Future Work

I'm happy with my solutions, and felt as though I learned a decent amount. With more time, I think I would have been able to complete most of these problems, particularily the ones requiring Racket and the deeper dive into k-coloring, which were both too time prohibitive for me to really get into in 4 hours.