[vyafisct] SAT matrix

express an CNF satisfiability problem as a matrix: rows are clauses, columns are variables.  a matrix entry is +1 if a variable is present positively in the clause, -1 if negated, and zero if not present.

are there interesting SAT problems with pretty matrices?

do matrix operations, e.g., matrix decomposition, yield interesting facts about the satisfiability problem?