Context: I have a huge circuit with lots of input bits (around 300). Among these, only about 40 are free, the others are fixed by the current state. I have to find all satisfying assignments knowing there are no more than 10.
This is Circuit-SAT which is NP-complete. Currently I solve a Tseitin-transformed version, but it takes hours to find even a single solution. Brute-force is not an option (even if it's only 40 bits), tried it and takes even more time somehow.
My idea was to try to convert the original circuit (not the CNF) to disjunctive normal form (DNF). It would incorporate all solutions in the final form. I know that there exists a polynomial-time conversion algorithm, but with the risk of exponential blowup with regards to space. But I was thinking about it and since there are surely no more than 10 solutions, I wonder if it would be possible without the exponential blowup considering the complexity of the circuit and that solutions for sub-parts of it might very well blow up exponentially (would they?).
My question: Is it reasonable to think that if there are only a few solutions, it won't blow up exponentially?
It is the point of Tseitin encoding to prevent the exponential growth when converting your circuit to CNF. The direct translation of a circuit to DNF would require - as you noticed - the complete search for all SAT solutions. Every minterm in the DNF is one input variable assignment which satisfies your circuit.
My suggestion is to use a tool like bc2cnf to convert your circuit to CNF. bc2cnf simplifies your circuit by exploiting constant values for inputs. Due to the modest size of 40 non-fixed input variables, you can hope that the result is a rather small CNF which can then be solved by modern SAT solvers like cryptominisat or Z3.