3
$\begingroup$

What is known about the following optimization problem for formulas in propositional logic:

  • input: formula $F$
  • output: formula $G$ in CNF with $\mathrm{Var}(G) \supseteq \mathrm{Var}(F)$ such that for all assignments $m$, $m$ is a model of $F$ exactly if $m$ is the restriction (to $\mathrm{Var}(F)$) of some model of $G$
  • measure: size of $G$

The Tseitin transformation realizes the input/output specification in polynomial time but it does not care for size. One would say "why bother" because for Tseitin, the size of $G$ is linear in the size of $F$, and what more could you hope for?

My motivation is to improve bit blasting encodings of (finite domain) SMT problems, and there, even small improvements may be useful.

E.g., $F$ could be the formula that describes multiplication of 8-bit numbers: it has $3\times8$ variables, encoding numbers $a,b,c$; and it is true iff $ab = c$. One can take any of the multiplication circuits, and Tseitin-transform them, but this may not be the best approach.

I know that reducing CNF size does not always reduce SAT solver runtime, so there could be other interesting criteria (for "propagatability"), but I'd like to start with some obvious measure.

$\endgroup$
  • $\begingroup$ Your description of the relationship between $F$ and $G$ does not quite match what Tseitin does: If $m$ is a model of $G$, then its restriction is a model of $F$, but in the other direction we have only that for each model $m'$ of $F$, there is one model of $G$ among the assignments which restrict to $m'$. $\endgroup$ – Klaus Draeger Apr 23 '15 at 13:15
  • $\begingroup$ @KlausDraeger right, of course. $\endgroup$ – d8d0d65b3f7cf42 Apr 23 '15 at 16:16
  • $\begingroup$ sounds like basically a compression or encoding question/ algorithm. it would help if you defined "bit blasting encodings". and why do this? as you allude the SAT solver is likely to run about as fast on the equivalent compressed problem. have you worked with SAT or SMT solvers? maybe something to discuss here in Computer Science Chat $\endgroup$ – vzn Apr 23 '15 at 17:55
  • $\begingroup$ "run about as fast" .. far from it. Every single variable or clause may count. Yes, I have experience with this. $\endgroup$ – d8d0d65b3f7cf42 Apr 23 '15 at 18:10
  • $\begingroup$ There's lots of research on optimizing bit-blasting and optimizing Tseitin transforms. Have you read the paper introducing STP, for instance? (From memory, I think the authors were Vijay Ganesh and David Dill) $\endgroup$ – D.W. Apr 23 '15 at 22:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.