Solving Exact Cover via SAT

A place to discuss the science of computers and programs, from algorithms to computability.

Formal proofs preferred.

Moderators: phlip, Moderators General, Prelates

Aldarion
Posts: 133
Joined: Thu Jul 19, 2007 7:00 pm UTC

Solving Exact Cover via SAT

Postby Aldarion » Thu Jan 16, 2014 6:49 am UTC

I've got an Exact Cover problem i've been trying to beat for a long time, using Algorithm X.
Now, I've managed to find some solutions, but what interests me much more is counting all of them.
The problem is that Algorithm X is really slow, finding a couple of solutions (out of potentially millions) per hour. I could use another implememtation of the Algorithm, but even if it's ten times as fast it would be still too slow. I need a better algorithm, but X is, as far as I know, the best available algorithm for Exact Cover.
Yesterday I had an idea, though: if I were to convert my problem into a SAT problem, I could use a modern SAT solver - and they are said to be quite efficient.
Does my plan make sense, or will the conversion likely result in such a hard instance of SAT that even the modern algorithms will be just as slow?
I'm not good, I'm not nice, I'm just right.

korona
Posts: 495
Joined: Sun Jul 04, 2010 8:40 pm UTC

Re: Solving Exact Cover via SAT

Postby korona » Thu Jan 16, 2014 9:49 am UTC

You cannot be sure until you try. I've worked with SAT for several years. Modern CDCL-SAT solvers perform very well on many instances obtained from such applications. SAT solvers often perform better than specialized solvers for NP-complete problems. However it is hard to tell how the solver will perform without knowing the encoding you want to use.

Translating the problem to SAT should not be that hard so you could just try it and see how solvers like lingeling or glucose (or other solvers from the application track and hard combinatorial tracks of the SAT competition) perform.

If you want to count the solution I suggest you use a incremental solver (I've worked with PicoSAT in the past but there are other solvers that also have incremental interfaces) and after you found a solution you add a clause that bans this solution from the solution space and run the incremental solver again. Incremental solvers are able to keep learned clauses between runs which greatly reduces solve time for consecutive runs.

Aldarion
Posts: 133
Joined: Thu Jul 19, 2007 7:00 pm UTC

Re: Solving Exact Cover via SAT

Postby Aldarion » Thu Jan 16, 2014 9:09 pm UTC

Thank you!
Could you recommend a good SAT solver for Windows? I'm not good at compiling sources, and I don't have a Linux machine anyway.
I'm not good, I'm not nice, I'm just right.

korona
Posts: 495
Joined: Sun Jul 04, 2010 8:40 pm UTC

Re: Solving Exact Cover via SAT

Postby korona » Sat Jan 18, 2014 1:30 pm UTC

Unfortunately I develop on Linux so I don't know which SAT solver run on windows. But they should be trivial to port as they don't use many system calls.

You could simply install a virtual machine to test them out. If you have a AMD or Intel CPU with hardware virtualization you'll get native performance for CPU bound tasks like SAT solving.

Aldarion
Posts: 133
Joined: Thu Jul 19, 2007 7:00 pm UTC

Re: Solving Exact Cover via SAT

Postby Aldarion » Sat Jan 18, 2014 5:24 pm UTC

I did some more research and found out that I wasn't actually looking for a SAT solver! :)
After all, getting a solution (or several solutions) isn't what I need.
So the problem I want to solve is #SAT. For this I found https://sites.google.com/site/marcthurley/sharpsat, and even managed to compile it.
It's been running for a couple of hours now, showing no signs of halting. Oh well. With a problem file weighing 573 MB, it's a wonder it didn't outright crash.
I'm not good, I'm not nice, I'm just right.

korona
Posts: 495
Joined: Sun Jul 04, 2010 8:40 pm UTC

Re: Solving Exact Cover via SAT

Postby korona » Sun Jan 19, 2014 11:14 am UTC

#SAT can be solved by a SAT solver and some iterative procedure. I never heard of sharpsat, and it never won a SAT competition so chances are that it cannot compete with other solvers. I suggest you try to use a state-of-the-art SAT solver like lingeling or glucose and see if it can find a single solution. Solvers are often able to find solutions even if the problem size is multiple GBs. If it can find a single one fast then counting them might be viable.

You could also explain how your encoding works and we could try to reduce the size of your encoding.

Aldarion
Posts: 133
Joined: Thu Jul 19, 2007 7:00 pm UTC

Re: Solving Exact Cover via SAT

Postby Aldarion » Sun Jan 19, 2014 7:17 pm UTC

The "iterative procedure" part bothers me a bit; did you mean what you said earlier?

korona wrote: after you found a solution you add a clause that bans this solution from the solution space and run the incremental solver again. Incremental solvers are able to keep learned clauses between runs which greatly reduces solve time for consecutive runs.


If I'm right about this, the problem has something like 100! solutions. Adding them up one at a time wouldn't be very practical...

korona wrote:I suggest you try to use a state-of-the-art SAT solver like lingeling or glucose and see if it can find a single solution.

Trying right now with lingeling. No solution yet, but it's been only an hour.

korona wrote:You could also explain how your encoding works and we could try to reduce the size of your encoding.


I took the Exact Cover matrix and encoded it as shown here. At the end, the problem has 52000 variables and 35,271,818 clauses.
I'm not good, I'm not nice, I'm just right.

korona
Posts: 495
Joined: Sun Jul 04, 2010 8:40 pm UTC

Re: Solving Exact Cover via SAT

Postby korona » Mon Jan 20, 2014 4:08 pm UTC

Counting 100! solutions is infeasible, even running a loop from 1 to 100! that does nothing would take ages (i.e. longer than the existence of the universe). How big is your input problem? I guess there are 52000 points? How many sets are there?

Aldarion
Posts: 133
Joined: Thu Jul 19, 2007 7:00 pm UTC

Re: Solving Exact Cover via SAT

Postby Aldarion » Mon Jan 20, 2014 4:58 pm UTC

Well, SharpSAT doesn't seem to be counting the solutions.
There's an example .cnf file (taken from another program, unaffiliated with SharpSAT's author) which it processes in about a second, finding 206829646435704880299088281600 solutions.
The ExactCover problem has 2304 points and 52000 subsets. Each of the subsets becomes a variable in the reduction to SAT.
I'm not good, I'm not nice, I'm just right.

Aldarion
Posts: 133
Joined: Thu Jul 19, 2007 7:00 pm UTC

Re: Solving Exact Cover via SAT

Postby Aldarion » Thu Jan 23, 2014 8:56 pm UTC

If it helps, here is the original problem: Solving the Octopuszle
I'm not good, I'm not nice, I'm just right.


Return to “Computer Science”

Who is online

Users browsing this forum: No registered users and 4 guests