Reducing a problem to 2-SAT

Given a matrix $$A$$ with entries $$a_{ij} \in \{0,1\}$$, the matrix $$B$$ is formed by $$b_{ij}=a_{ij} + a_{i+1,j} + a_{i,j+1} + a_{i+1,j+1}$$. $$B$$ has one row and one column less than $$A$$. The problem is given such a matrix $$B$$ to find one possible matrix $$A$$ that produced $$B$$. This can be done by reducing the problem to 2-SAT, but after many attempts I'm I am not sure how to approach it.

All entries $$b_{ij}\in\{0,1,2,3,4\}$$, but given for example $$a_{ij} + a_{i+1,j} + a_{i,j+1} + a_{i+1,j+1} = 2$$ is there a 2 CNF formula that is equivalent to that (and for the other cases when the entry is $$1$$ or $$3$$)?

• Note that you only need to do the cases $\mathrm{sum}=0$ (trivial), $\mathrm{sum}=1$ and $\mathrm{sum}=2$. For the other cases, you can use the fact that $w+x+y+z=4-(\bar{w}+\bar{x}+\bar{y}+\bar{z})$. – David Richerby Nov 1 '18 at 21:15
• In the case when the sum is $2$, one could just take all combinations: $(w+x) = 1 \land (y+z) =1$, or $(w+y) = 1 \land (x+z) = 1$, and so on. Then put the resulting formula into 2-CNF. (First put it in CNF, and then put it in 2-CNF. Both transformations are standard, see wikipedia.) – Eugen Nov 1 '18 at 21:52
• Sorry, big mistake in the the previous post: putting the resulting formula in 2-CNF is not trivial, and a general translation of boolean formulas into 2-CNF does not exist. – Eugen Nov 1 '18 at 22:04
• @Eugen For the case when the sum is 1 that is like saying "For every pair of variables $x$,$y$ $(\overline{x}|\overline{y})$ is true, but there exists a pair $(x|y)$ that is also true." Now I am not that good with boolean logic, but is it even possible to model "there exists" relation for more than 2 variables in 2 CNF. – Surfrider Nov 1 '18 at 22:31
• (I am predicting Yuval is working on this...) (this comment will be deleted.) – Apass.Jack Nov 1 '18 at 22:35