# How to reduce MAX-2SAT problem to finding a cut in a graph

I'm trying to reduce the MAX-2SAT problem to finding a cut in a graph, with no luck so far.
Let me first show a description of the problem:
2SAT: Given a boolean formula $\varphi$ in a CNF form, where every clause has 2 literals (a variable or its negation), one should decide whether there is an assignment that will satisfy $\varphi$.
The 2SAT problem is in $P$.

MAX-2SAT: Given a boolean formula $\varphi$ in a CNF form, where every clause has 2 literals, and $k\in \mathbb{N}$, one should decide if there is an assignment that will satisfy at least $k$ clauses in $\varphi$.
This is an $NPC$ problem, and I'm trying to reduce it to finding the maximum cut in a graph:
MAX-CUT: Given $(G=(V,E), w, k)$, where $G$ is an undirected graph, $w$ is a weight function; $w: E\rightarrow \mathbb{N}$ and $k\in\mathbb{N}$, one should decide whether there exist a cut $(V_1,V_2)$, s.t its weight is at least $k$, meaning $k\leq \sum _{u\in V_1, v\in V_2}w(u,v)$.

I tried some obvious constructions that didn't work, like setting:
$G=(V,E)$
$V=\left \{ v_x|x\text{ is a literal in } \varphi \right \}$
$E=\left \{(v_x,u_z)|\text{ There exist a clause } x\vee z \text{ in } \varphi\right \}$
and finally setting $w(e)=1$ $\forall e\in E$

This obviously didn't work, since having $k$ satisfied clauses in $\varphi$ does not imply a $k$-weighted cut in $G$.
(If the above can be improved to achieve the desired reduction, I would love to get some guidance)
I looked around online, and found that it is possible to construct an "implication graph" from $\varphi$, where every clause $(x\vee z)$ in $\varphi$ is translated to the equivalent logical expressions: $\bar{x}\Rightarrow z$ and $\bar{z}\Rightarrow x$, and these, in turn, are translated to vertices $\bar{x}, z, \bar{z}, x$, and directed edges $\bar{x}\rightarrow z$ and $\bar{z}\rightarrow x$, but I just can't see how that helps, since, again, $k$ satisfied clauses in $\varphi$ does not imply $k$-weighted cut in $G$.
Any help would be greatly appreciated.

Idea: Have two vertices $x,\bar{x}$ for each variable, and connect them with an edge with some large weight which will force any maximal cut to put them in different parts of the cut. The idea is that for any two variables $x,y$, $x$ and $y$ get the same truth value iff the vertices $x,y$ are in the same part of the cut. This way you encode a truth assignment.
For each clause $x \lor y$, we would like to do something of the following sort: add a vertex $\varphi_{x \lor y}$ and connect it to both $x$ and $y$. In order to guarantee that $\varphi_{x \lor y}$ is in some specific part of the cut, add a new vertex and connect it to all "clause" vertices with an edge having some large weight. This idea doesn't quite work since the value of the cut depends on how many literals satisfy the clause. Find a way to fix it.
Clause $x_i \vee x_j$ is equivalent to $x_i+x_j-x_ix_j$; clause $\bar x_i\vee x_j$ is equivalent to $1-x_i+x_ix_j$; clause $x_i\vee \bar x_j$ is equivalent to $1-x_j+x_ix_j$, and clause $\bar x_i\vee \bar x_j$ is equivalent to $1-x_ix_j$. Therefore, we could recast the MAX 2-SAT objective of maximizing the number of satisfied clauses as the QUBO objective of maximizing a quadratic function of binary variables.
All that remains is to cast the QUBO problem as a MAX-CUT problem. There is a well-known reduction from QUBO to MAX-CUT due to Hammer (1965). Consider QUBO instance $\max \sum_{i\neq j} q_{ij}x_ix_j + \sum_i c_ix_i$. Construct a graph with one node $y_i$ for every variable $x_i$ in the QUBO instance in addition to super-node $S$. Define the weights of each edge between $y_i$ and $y_j$ to be $w_{ij} = -q_{ij}$ and define the weight between each $y_i$ and $S$ to be $w_{iS} = c_i + \sum_j q_{ij}$. A bit of algebra shows that you can construct the optimal QUBO solution $x^*$ from the optimal MAX-CUT solution $y^*$ by setting $x_i^*=1$ if $y_i^*$ lies across the cut from $S$ and $x_i^*=0$ if $y_i^*$ lies in the same set as $S$.