I have a logic to feed to SAT solver
(a1&&b1)||(a2&&b2)||(a3&&b3)||(a4&&b4)||(a5&&b5)
to feed to SAT solver which accepts CNF
I tried wolfram alpha to convert it into CNF but it's way too complicated to understand than the DNF. the original semantic is that, A and B intersects on one of the columns. which is why I think DNF is more readable
is there any way to incorporate some additional boolean variables to simplify it and convert it to CNF ?
the ultimate target is to maintain a relatively readable CNF
======ammend the whole context is that I am trying to express Einstein's puzzle using CNF, I find some of the clauses are difficult to express using CNF.
Okay so what you actually want is to convert the given clause to an equi-satisfiable CNF, not to solve it nor to simply convert it to CNF.
Just create new boolean variables $p_{1..5}$.
Note that $a_k \land b_k \to p_k \equiv \neg a_k \lor \neg b_k \lor p_k$ and $p_k \to a_k \land b_k \equiv ( \neg p_k \lor a_k ) \land ( \neg p_k \lor b_k )$.
Thus by appending these two CNFs for each $k$ you get $p_k \equiv a_k \land b_k$ in any satisfying assignment.
After that the original clause can be replaced by $p_1 \lor \cdots \lor p_5$.