I am implementing a MAX-3SAT solver in C. Obviously, there is a lot of literature regarding boolean formulae in conjunctive normal form. I was planning to store them in the format:
int **formulae;
Which is an array of arrays of variable IDs, where the variable is negative to indicate negation (just as in the standard DIMACS CNF format).
Here is my question: are there any "clever" data structures for 3SAT I should know about? Perhaps structures that enhance the performance of solving algorithms?