16
$\begingroup$

SAT solvers are getting more and more efficient in solving large instances and are being used as back-ends in various contexts. Every time one wants to use them to solve a problem in a specific domain, he/she has to come up with an ad-hoc encoding that not only has the right set of solutions but also puts the constraints (even redundant) in a form that helps the heuristics of solvers in finding a solution faster.

Many such encodings seem to me would be very common, for example: asserting that a finite set of nodes is linked as a tree, or as a DAG, or a list is sorted...

Is there a repository/recipe book of common encodings for common problems with optimised solutions?

$\endgroup$
  • $\begingroup$ 1. This question looks very useful, but also potentially overbroad. I think it might be a better question if you focus it on a single domain (yes, this might involve multiple questions, one per domain -- but make sure to do some research before asking and show us what you've done). $\endgroup$ – D.W. Oct 9 '14 at 18:47
  • $\begingroup$ 2. Also, what research have you done? Have you looked at SAT front-ends, such as STP, Alloy, and Minion? Have you looked at cs.stackexchange.com/q/12087/755, cs.stackexchange.com/q/13188/755, cs.stackexchange.com/a/6522/755, cs.stackexchange.com/a/12153/755? at the questions tagged sat-solvers or satisfiability? $\endgroup$ – D.W. Oct 9 '14 at 18:51
  • $\begingroup$ Yes, the question may be a bit broad. @D.W. thanks for the links some of them are directly relevant. I should have mentioned I am not interested in solving a particular problem, nor in general methods for more efficient encodings; the expression "best-practices" I used is probably misleading, I'll edit. I am interested in a recipe book =) $\endgroup$ – Bordaigorl Oct 9 '14 at 19:15
  • $\begingroup$ Regarding the domain I would say (hyper)graph theory but this is probably still very broad... $\endgroup$ – Bordaigorl Oct 9 '14 at 19:19
  • $\begingroup$ See also related question cs.stackexchange.com/q/12087 $\endgroup$ – András Salamon May 20 '17 at 8:11
9
$\begingroup$

I read a survey paper a few years ago that seems relevant, "Successful SAT Encoding Techniques" by Magnus Björk.

Abstract:

This article identifies good practices for SAT encodings by analysing interviews with a number of well known SAT experts. The purpose is both to determine the confidence in different encoding strategies by analysing whether there is consensus among the experts or not, as well as bringing out hidden knowledge to SAT users.

There is consensus that encoding techniques usually have a dramatic impact on the efficiency of the SAT solver, that it often takes much work to find a good encoding, and that the size of an enconding is only very loosely related to the hardness of finding a solution. Topics where the interviewees disagree include the feasibility of including arithmetics in SAT problems and whether to formulate problems as clauses or circuits.

The article describes a number of strategies that are good in different situations, such as different ways to represent numbers and how to use incrementality.

$\endgroup$
4
$\begingroup$

It is always a good idea to first check out the Handbook of Satisfiability [1] (I guess it's not freely available, sorry). Here, Chapter 2 is titled "CNF Encodings". At the very least, the book provides literature references on the state of the art on the time of the writing, and you can expand your search through them.

In addition, here and here are two recent slides on SAT preprocessing. The slides give a concise overview of preprocessing techniques, and also further references. The idea is that instead of trying to "manually" model the problem in an efficient way, you just model it in the easiest way, press go, and a software gives you an efficient encoding.


[1] Biere, Armin, Marijn Heule, and Hans van Maaren, eds. Handbook of satisfiability. Vol. 185. IOS Press, 2009.

$\endgroup$
3
$\begingroup$

not exactly a direct answer but another increasingly closely related angle: some of this is covered by a relatively new area of research known as SMT, Satisfiability Modulo Theories. the basic idea is to combine problem encodings (eg say integer arithmetic, graphs, etc) into the SAT solver but also use/ leverage the extra knowledge that comes from this coupling to build more advanced solution algorithms. heres a survey. as pointed out they can be much more efficient than combining an ad-hoc encoding mechanism with standard SAT solvers.

  • Satisfiability Modulo Theories: An Appetizer / Leonardo de Moura and Nikolaj Bjørner

    Satisfiability Modulo Theories (SMT) is about checking the satisfiability of logical formulas over one or more theories. The problem draws on a combination of some of the most fundamental areas in computer science. It combines the problem of Boolean satisfiability with domains, such as, those studied in convex optimization and term manipulating symbolic systems. It also draws on the most prolific problems in the past century of symbolic logic: the decision problem, completeness and incompleteness of logical theories, and finally complexity theory. The problem of modularly combining special purpose algorithms for each domain is as deep and intriguing as finding new algorithms that work particularly well in the context of a combination. SMT also enjoys a very useful role in software engineering. Modern software, hardware analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using symbolic logic for describing states and transformations between them. A well tuned SMT solver that takes into account the state-of-the-art breakthroughs usually scales orders of magnitude beyond custom ad-hoc solvers.

$\endgroup$
  • $\begingroup$ This is a very good point. But even when you use a SMT solver, there is a purely SAT based portion of the search that can benefit from successful "recipes"... $\endgroup$ – Bordaigorl Oct 10 '14 at 17:18
  • $\begingroup$ it is not entirely accurate to say theres a "purely SAT based portion of the search," because (as stated/ my understanding) it uses the special known/ constructed structure of the generated instances in its heuristics which a "vanilla" solver would not "recognize". in other words it (ie the combination) is not "reducible/ separable" to constituent parts (ie encoder plus solver) or merely another standardized encoding system. $\endgroup$ – vzn Oct 10 '14 at 17:20
  • $\begingroup$ I see. I'll read more about it thanks! $\endgroup$ – Bordaigorl Oct 10 '14 at 17:27
  • $\begingroup$ sure. also note answer set programming is somewhat similar. $\endgroup$ – vzn Oct 10 '14 at 17:33

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.