Verify Combinatorial CNF SAT Encodings?

I am trying to solve a combinatorial problem by using a SAT Solver.

This involves the following steps:

Encode the problem as set of boolean expressions.
Translate a conjunction of the expressions into CNF/DIMACS
(using home grown tools, bc2cnf, bool2cnf or Limboole)
Solve the CNF
(using SAT Solvers like Cryptominisat, Plingeling, Clasp or Z3)
Translate the solution (assuming a "SAT" result) back into the problem domain

This works in my case for small samples. But for more challenging ones, the SAT solver takes hours or even days without coming to a SAT/UNSAT conclusion. I try to tune my encoding to arrive at a solution. But the more effort I put in my encoding, the less certain I can be that my encoding is actually correct (i.e. "satisfiability equivalent").

The step from boolean expression to CNF is rather convoluted to be efficient in terms of a managable number of clauses and variables. It is painful to wait ages for the SAT solver and not be sure that the time is spent on the right track.

The boolean expression might be wrong. Therefore, I'd like to validate that the CNF actually represents the original problem not just the boolean expression.

My Question:

How could I verify that a given encoding is a valid representation of the original boolean expression?

From the literature, I have known solutions for some problems which I could translate into variable assignments to gain trust in my encoding process. But due to Tseitin encoding, most of the variables in my CNF are auxiliary (switching) variables. Without Tseitin encoding, my CNF would be far too big to be solvable. I therefore cannot simply check if every CNF clause is fulfilled by the known solution.

I have tried to translate the CNF back into boolean expressions using cnf2aig, but the tool is still in its infancy. Without switching variables, it is straightforward to check an assigment against boolean expressions of the primary problem variables.

There are a couple of publications about "CNF to circuit" approaches, but none of them provides a usable tool.

Is there any best practice to accomplish such a check?

So what you are asking is:

Given a boolean expression B and a CNF C, is there a way to tell if they are equisatisfiable?

Or in other words:

Exists a model that satisfies B but not C, or that satisfies C but not B? If no such model exists then both are equisatisfiable.

My solution to that problem would be the following:

I'd use a known-good software (e.g. your unoptimized code or a third party tool) to generate a known-good CNF D from the boolean expression.
Use Tseitin to generate CNF for !B from C and D. I.e. interpret the CNF for C as a product of sums (conjunction of disjunction) and invert the whole expression. Lets call the resulting CNFs C' for the inverse of C and D' for the inverse of D.

So a model that satisfies C would not satisfy C' and vice versa. Similar for D and D'.
Use a SAT solver to find a model that satisfies C and D'. Such a model would satisfy C but not B.
Use a SAT solver to find a model that satisfies C' and D. Such a model would satisfy B but not C.
If steps 3. and 4. both do not yield a model (unsat) then you have proven that B and C are equisatisfiable.

Steps 3. and 4. are easy. Just create one big CNF that contains all clauses from the two CNFs. All variables from B must be encoded with the same literal in both CNFs and the auxilary variables must be allocated from separate pools.

Depending on your problem, the solving steps 3. and 4. might be computationally quite expensive. So this approach might only be feasible if you can split up your problem into smaller chunks that can be verified independent from each other.

I hope that helps. You have said you are trying to make sure your optimizations are correct, so you should have a known-good implementation. Otherwise you could use a library I have written as an external reference:

https://github.com/cliffordwolf/yosys/tree/master/libs/ezsat

The CNF generated by this library is not very efficient! But it is well tested..