I have a Boolean Matrix System (BMS) as described below $$Ax=c$$ where $A$ is a $n\times n$ Boolean matrix (i.e., all entries are either 0 or 1), $c$ and $x$ are two $n$-dimensional Boolean column vector. The product of two Boolean matrices $A_{m\times k}$ and $B_{k\times n}$ is $C_{m\times n}$, defined by $$c_{ij}=\bigvee_{h=1}^{k}(a_{ih}\wedge b_{hj})$$
Assume $A$ and $c$ are given, now how to solve $x$?.
I have do some works. One way to do this is to transform a BMS to CNF, and solve it by SAT Solver. However, the transformation is quite sophisticated, and I have no idea to tackle it. Would you like to give me some advice?
$$ \begin{array}{cl} &~ b=Ax \\ &~ \\ &\Leftrightarrow \left[ \begin{array}{c} b_1 \\ b_2 \\ \vdots \\ b_n \\ \end{array} \right] = \left[ \begin{array}{c} \bigvee^n_{k=1} (a_{1k} \wedge x_k) \\ \bigvee^n_{k=1} (a_{2k} \wedge x_k) \\ \vdots \\ \bigvee^n_{k=1} (a_{nk} \wedge x_k) \\ \end{array} \right] \\ &~ \\ &\Leftrightarrow \left[ \begin{array}{c} \left(\neg b_1 \vee \left( \bigvee^n_{k=1} (a_{1k} \wedge x_k)\right)\right) \wedge \left(b_1 \vee \neg\left( \bigvee^n_{k=1} (a_{1k} \wedge x_k)\right)\right) \\ \left(\neg b_2 \vee \left( \bigvee^n_{k=1} (a_{2k} \wedge x_k)\right)\right) \wedge \left(b_1 \vee \neg\left( \bigvee^n_{k=1} (a_{2k} \wedge x_k)\right)\right) \\ \vdots \\ \left(\neg b_n \vee \left( \bigvee^n_{k=1} (a_{nk} \wedge x_k)\right)\right) \wedge \left(b_n \vee \neg\left( \bigvee^n_{k=1} (a_{nk} \wedge x_k)\right)\right) \\ \end{array} \right] \end{array}$$