SAT solvers are getting more and more efficient in solving large instances and a

Question

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?

Explanation / Answer

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

Related Questions

Navigate

• Browse (All)
• Browse S
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.