the input form of minisat+？

[先建 王]

first,I use logic synthesus software(such as SIS) to convert the
circuit into NOR netlist and generate a BLIF file;
then,I propose a satisfiability-based(SAT) approach for solving the
circuit cell assignment problem,I would like to use minisat+(pseudo-
boolean solver) to solve this problem.
But what is the input form of minisat+?.opb or .lin or others,I am
confused that it.
how do I convert the BLIF file to a file that minisat+ can read?
Help me. Please!

[Hadi Katebi]

The input to Minisat is CNF in DIMACS format. Check it on the web, you'll find a bunch of resources.

I don't know if there is any tool that converts BLIF to DIMACS, but a tool called ABC form Berkeley (which is mainly a verification and synthesis tool) integrates minisat in some of its routins (for example, CEC = Combinational Equivalence Checking). The most common format to ABC is BLIF. Here is the link to ABC: http://www.eecs.berkeley.edu/~alanmi/abc/

Hadi

[王先建]

Thank you for your reply.After I installed the minisat+,I found that there is "Example" folder ,and in this folder,the input forum of minisat+ was .opb,but it was not CNF.then I tested an example,but I found that it could generate a CNF file.

minisat+ is pseudo-boolean solver which is not same to minisat.

Here is the link to minisat+ and minisat:http://minisat.se/

I don't kown whether my understanding is  right or not.

2011/3/22 Hadi Katebi <hadi....@gmail.com>

[Niklas Sörensson]

Hello,

Yes, the input-format of MiniSat+ is OPB, but unfortunately the
OPB-format has changed a bit since MiniSat+ was developed and there
are some minor differences. You can read about the OPB format here:

http://www.cril.univ-artois.fr/PB11/format.pdf

Note that OPB is a flat format for linear constraints and if you need
to convert a circuit (for instance from BLIF) you need to use
something like the Tseitin transformation. There are tools that would
help you with that transformation if the target format is DIMACS, but
I'm not aware of any tools that directly translates to OPB and allows
to provide an optimisation function.

Maybe you can use standard tools (ABC perhaps?) to translate first to
DIMACS and the translate the result to OPB + an optimisation function,
but I suspect it might be problematic to keep track of the variables
in order to add the optimisation function.

/Niklas