muhos / ParaFROST

A Parallel SAT Solver with GPU Accelerated Inprocessing
GNU General Public License v3.0
86 stars 6 forks source link

How to get the number of solutions? #6

Closed liyu0x closed 1 year ago

liyu0x commented 1 year ago

Hi, I am using ParaFORST to solve cryptography problems, and how I get the detail of an solution and get the total number of solutions?

Thank you.

liyu0x commented 1 year ago

Hi, I get the variables for an solution, but now I want to get total number of all solutions, what should I do?

muhos commented 1 year ago

Hello, sorry for my late response. I have been away from developping this project for a while. To get the total number of solutions, you have to do model counting. A naive algorithm is to call a SAT solver iteratively considering previous models. More info. can be found here: https://www.cs.cornell.edu/~sabhar/chapters/ModelCounting-SAT-Handbook-prelim.pdf

liyu0x commented 1 year ago

Hello, sorry for my late response. I have been away from developping this project for a while. To get the total number of solutions, you have to do model counting. A naive algorithm is to call a SAT solver iteratively considering previous models. More info. can be found here: https://www.cs.cornell.edu/~sabhar/chapters/ModelCounting-SAT-Handbook-prelim.pdf

Never mind, and thank you for responsing me, I will read it.