Exploring Formula Size vs SAT Difficulty

[R. Kudos]

Are there any parameters that allow generating a smaller SAT encoding at the expense of a (presumably) more difficult problem for the SAT solver?

For example, I think of the log encoding as an example in SAT circles which is generally thought to propagate poorly and thus requires more solve time but has a smaller CNF formula.

I'm hoping to be able to do this without reducing the scope of the errors that are detected by the prover. 

So in other words, is it possible to represent the same problem but by using a more concise CNF encoding at the expense of it probably being a more difficult problem for the SAT solver to solve?

[Martin Nyx Brain]

On Tue, 2020-05-19 at 09:55 -0700, R. Kudos wrote:
> Are there any parameters that allow generating a smaller SAT encoding
> at
> the expense of a (presumably) more difficult problem for the SAT
> solver?

Not really, no. On modern hardware, time tends to be the bottleneck
before memory. In cases where memory is a bottleneck, there tend to be
other things that you can do (i.e. incremental or lazy encoding,
slicing, etc.) that are more effective than making the problem more
time-intensive to solve.

> For example, I think of the log encoding as an example in SAT circles
> which
> is generally thought to propagate poorly and thus requires more solve
> time
> but has a smaller CNF formula.

I am not quite sure what you mean by the log encoding. If you are
referring to the encoding from CSP to SAT where you encode the choice
of one element from a domain of D things by using log_2(D) bits so that
they give a binary number picking the element, then, yes, we already do
that. That's how you can reason about int64_t without running out of
memory.

> I'm hoping to be able to do this without reducing the scope of the
> errors
> that are detected by the prover.

As long as the encoding is logically equivalent or at least
equisatisfiable it should be fine.

> So in other words, is it possible to represent the same problem but
> by
> using a more concise CNF encoding at the expense of it probably being
> a
> more difficult problem for the SAT solver to solve?

I am not aware of any ways of doing this, nor do I think it would be a
particularly useful trade-off. There are ways that the encodings can
be improved (I am working on some) but I don't think "more compact but
harder" is the way to go.

HTH

Cheers,
- Martin

[Hannes Steffenhagen]

I should point out we did actually have some cases recently where memory usage, not performance, was the issue... though I don’t think that was just the size of the resulting formula. At any rate, some cases where solutions could be found within minutes, but memory usage in the dozens of GB (which isn’t extreme of course with modern machines, but more than you’d have on the average workstation).

Diffblue Ltd, a company registered in England and Wales number 09958102. Registered office 10 St Ebbes Street, Oxford, OX1 1PT, UK