Computational complexity

Which of these is the definition of the class NP?

Which of these problems are known to be in P? (Select all that apply.)

Karp's reduction from 3-SAT to INDEPENDENT SET is applied to a 3-CNF formula with $7$ clauses on $5$ variables. How many vertices does the graph $G_\varphi$ have?

In the reduction from SAT to 3-SAT, a clause $(\ell_1 \vee \ell_2 \vee \cdots \vee \ell_7)$ with $7$ literals is replaced by a chain of 3-literal clauses using fresh variables $z_1, z_2, \dots$. How many 3-literal clauses does it become?

You want to prove that a new problem $B \in \mathrm{NP}$ is NP-complete. Which is enough?

In the proof of Theorem 5 ($\Leftarrow$ direction) we said: an independent set $S$ of size $m$ in $G_\varphi$ contains exactly one vertex from each clause. Why?

Which of these statements are known theorems (not conjectures)? (Select all that apply.)

The Lean file proves bruteForce_correct : bruteForce φ = true ↔ Satisfiable φ and length_allAssignments : (allAssignments n).length = 2 ^ n. Which conclusion do these two theorems justify?

Implement Karp's reduction. A 3-CNF formula is a list of clauses, each a tuple of three nonzero integers ($v$ for $x_v$, $-v$ for $\neg x_v$). Number the vertices $3i + j$ for the $j$-th literal ($j = 0, 1, 2$) of clause $i$. Write karp_graph(formula) returning the set of edges as pairs (p, q) with p < q: the three edges inside each clause, and an edge between every two vertices whose literals are complementary.