hints for cnf solver

[sbelodon]

Hello,

the situation is following: I've got cnf formula after Tseytin transofrmation. It relies on 32 variables. but Tseytin tranformation introduces much more intermidiate variables(~300 000) (we don't need they values) I want to know your opinion about 2 points: 1.If solver will know that variables 1-32 for example is base(others are intermidiate) and take only it for decisions (except pure literals and other 100% vars) will it speed up solving? 2 will hints from Tseytin transform like variable 3 is conjuction (or other function) of var 1 and 2 speed up solving?

Thanks for answer in advance

[arminbiere]

Splitting on inputs only is an old idea (goes back to the PODEM algorithm in ATPG). But also see the thesis of Matti Järvisalo for reasons, that this is in general not a good idea, at least from a theoretical perspective. Also in practice I have not seen much advantages of doing that. However, there is a 'lglimportant' API function in Lingeling and similarly a 'picosat_set_more_important_lit' API function in PicoSAT (used for instance by Joao Marques-Silva in encoding cardinality constraints in one application). But I am not aware of any 'hints' in a DIMACS file and as I wrote above I do not think that this is a good idea in general.

[arminbiere]

Also let me mention that it is more tricky to have such a function in CaDiCaL or Kissat which have multiple decision queues, one actually being a doubly linked list without a sorting function. For the VMTF doubly linked list one would need two queues (one with higher and one with lower priority). This is awkward (adds lots of code) and probably slow. Then for Tseitin transformation, where the internal variables are functionally dependent on the inputs, you really only need the inputs in the decision queue (since the others are set through propagation). As soon you do for instance Plaisted-Greenbaum or some fancy preprocessing this breaks down though.

[arminbiere]

I will mark this now as a possible enhancement even though it is not trivial to achieve, so unlikely to happen.

[violetcodet]

the same problem it's really hard to model count when the number of variables is large （100 key variables and 300000 ~ intermidiate variables）. Can you give me some hints if you have solved this problem.

[arminbiere]

Not really, but we do have a 'structural' model counter which uses 'dual reasoning' exactly for this reason. It is called 'dualiza' and can be fond here: https://github.com/arminbiere/dualiza