Is possible to know the exact solution value in sharpSAT?

[LifeBach]

Hi! I try to use sharpSAT to solve 2 CNF files and want to know the number of a union of both solution sets, is that possible?
for example:
FileA has 3 variable: a, b, c and have solution set {011,111,110}
FileB has 3 variable: a, b, c and have solution set {101,111,110}
The union of solution set is {011,111,110,101}, so the answer is 4

Is that possible to use sharpSAT to solve this problem? or is possible to know the concrete solution set or even only a single solution in sharpSAT?

[ZaydH]

It has been a few years since I looked at the sharpSAT code in detail. My strong recollection is sharpSAT natively only returns the counts and nothing about the satisfying assignments.

SPUR (which I am the author of) is a SAT sampler built using sharpSAT and definitely contains the information on the satisfying assignments (you will need to make some changes to disable SPUR's second stage). That probably is an easier place to start.

Most SAT formulas of any non-trivial size has lots of satisfying assignments -- so many that enumerating them may take more memory than you have.

[VincentDerk]

If you're only interested in the model count, and you don't necessarily need the most efficient method, you can do 3 calls to sharpSAT: MC(CNF1) + MC(CNF2) - MC(CNF1 ^ CNF2).

MC(CNF1) + MC(CNF2) will double count models present in both CNF1 and CNF2 so you have to substract the conjunction of both. Since it's in a CNF you can easily conjoin both by just appending the clauses.

[haz]

There's also always the option to just encode your way through it, using a package like nnf (disclaimer, I'm one of the maintainers). Essentially, a recipe like...

1. Read both CNF files
2. Define a theory as the Or between them
3. Convert to CNF
4. Write that to file
5. Run sharpSAT or similar

If you want the actual models, your best bet is to use a knowledge compiler (c2d, dsharp, d4, etc)