search

wkschwartz / pigosat

Go (golang) bindings for Picosat, the satisfiability solver
Other
15 stars 4 forks source link

Flatten and simplify the picosat C lib (make go-gettable) #1

Closed justinfx closed 10 years ago

justinfx commented 10 years ago

I started looking at pigosat, and thought the first thing I would do is try to make it go-gettable. This uses the same approach as pygosat, where it only keeps the necessary C source right in the root, and I removed the subdir. cgo will only pick up C/C++ automatically if it is right next to the source. In my other projects that use cgo to do C/C++ bindings, I ended up following Gustavo Niemeyer's approach used in go-qml. But since there are only a few source files, it was easier to just drop them into the root.

wkschwartz commented 10 years ago

Not really sure why I did it the hard way. I just wish the Picosat team would make their code available in a more convenient form than tarball.

Pretty slammed at work right now but I'll test and merge as soon things settle down. However, everything looked fine when I did a quick look through the diff just now.

Thanks for sending a pull request. I hope you can get some use out of this package. I've only scratched the surface of what Picosat can do.

justinfx commented 10 years ago

I meant to ask about the use of the current exposure of the API. I'm just learning about SAT solvers and picosat and I couldn't understand the usage of the bool slice returned by Solve. How would you map that back to the actual variables that were used in the solution? In the case of pycosat I see that it returns the actual solution of variables, but pigosat doesn't expose it. I will probably send some more pull requests shortly to return the solution.

wkschwartz commented 10 years ago

If you send a separate pull request for "solution objects" we can discuss the design more there, but the solution sol []bool I return is basically the same as Picosat's picsoat_defref. With the Go slice, you give it a variable i int and get a boolean sol[i]. With the C function you give it a variable int i and get back an integer picosat_deref(picosat_instance, i) that is positive if true and negative if false. Pycosat's API is just to take that picosat_deref sign and apply it to the variable integer itself. These are all fundamentally interchangeable. The slice of bools felt most Go-y to me. I'm open to other ideas though.

justinfx commented 10 years ago

Sorry, the confusion about the bool slice was based on me not understanding properly that the variables should always be sequential anyways. My initial thought was that I would get back the variable ids to map back into the objects, but I see now that you are implying one would loop over the bools and use the indexes to map back to the included objects.

justinfx commented 10 years ago

Apologies. I overlooked that I did not submit this merge request in a topic branch, and ended up adding in one other commit that is separate, where it improves performance a bit by calling picosat_add_lits once with all literals, in a call to AddClauses. If you want, I can split these into different merge requests. Let me know.

wkschwartz commented 10 years ago

Yes please split. That'll make testing easier when I get to it (whenever my day job lets up...)

Thanks again. On Friday, August 15, 2014, Justin Israel notifications@github.com wrote:

Apologies. I overlooked that I did not submit this merge request in a topic branch, and ended up adding in one other commit that is separate, where it improves performance a bit by calling picosat_add_lits once with all literals, in a call to AddClauses. If you want, I can split these into different merge requests. Let me know.

— Reply to this email directly or view it on GitHub https://github.com/wkschwartz/pigosat/pull/1#issuecomment-52363089.

Billy Schwartz cell: 614-578-8007

justinfx commented 10 years ago

Closed in favor of topic branches #2 and #3