MiniQBF

 

Florian Lonsing pointed out a bug that occured on several instances.

This was due to a mistake in the parser (please download fixed version below).

 

While this is fixed for QDIMACS instances, I did not yet fix similar issues occuring due to non-standard QDIMACS instances

(e.g., problems containing tautologies).

 

Thanks for the feedback,

Horst

 

 

This is the first version of MiniQBF - a search-based QBF solver based on MiniSAT 2.0 by Niklas Een and Nilkas Soerensson.

 

The current aim of this solver is to provide researchers that are interested in QBF with a light-weight and understandable baseline QBF solver.

I tried to keep the extension and alternations to MiniSAT to a minimum so that it will be quite straight-forward for anyone who knows MiniSAT

to understand how the QBF version works. There are definitively parts of the code and techniques that can be improved (e.g., conflict / solution analysis),

and in terms of updating/changing the code this should indeed be feasible. In total, I hope that this solver will enable people to try out new ideas without

the need of developing a new QBF solver or to put a lot of effort in understanding a solver first.

 

In contrast to MiniSAT this solver is a not a state-of-the-art solver. However, it is quite competitive for a pure search-based solver.

In addition, I also want to point out that I tried to verify the correctness of the solver empirically, but it might be the case that I made a mistake in the code.

Therefore, I also hope that researcher interested in certifying or verifying the result of a QBF solver might find this small QBF solver relatively attractive as well.

 

I would also like to thank the following people for their comments on or contributions to this solver:

 

Said Jabbour

 

The source code can be downloaded here: MiniQBF 1.0 [Fixed a bug in the parser pointed out by Florian Lonsing]. 

 

Please feel free to comment on this or to report bugs, or to improve the solver, etc.
If you prefer, you can also write me an email at: hsamulowitz@googlemail.com

 

Thanks,

Horst