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?
Asked By : Bordaigorl
Answered By : Kyle Jones
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/30790
0 comments:
Post a Comment
Let us know your responses and feedback