ipasir_val return 0 when not important

[cormackikkert]

Hi Armin,

Would it be possible for ipasir_val to return 0 when a literal is not important for satisfiability? Currently, not important literals can be assigned true or false, it would be nice if they were always 0.

In the meantime is there a hack to see if a literal is important? The best I can think of is run the SAT solver again with the literal negated as a unit assumption, but this could be slow if if I want to check lots of literals.

Thanks,

Cormac

[arminbiere]

I would rather prefer to have then an additional API function which allows to check that. Actually what you are really asking for I think is to have CaDiCaL trim the produced model to become a prime implicant. There are algorithms for doing this:

David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure:
Computing prime implicants. FMCAD 2013: 46-52

I have two submitted papers on similar problems. I will keep this issue open and comment on this later then again.