How to install minisat2 on Mac OS X 10.6.8?

[dani nantes]

Hi, I am trying to install Minisat on my Mac OS X 10.6.8, when I try to follow the directions in README I get the following problem:

$ cd Documents/minisat/
$ export MROOT
$ cd core
$ make rs
Makefile:4: /mtl/template.mk: No such file or directory
make: *** No rule to make target `/mtl/template.mk'. Stop.

Does anybody know what to do? What should I do to install minisat on mac?

Kind regards,

[Michael Tautschnig]

Hi,

[...]

It seems you missed an essential part in the README file. It says:

export MROOT=<minisat-dir>

but all you did was "export MROOT", without the minisat directory. You will want
to use

cd Documents/minisat/
export MROOT=$PWD
cd core
make rs

Best,
Michael

[Bruno Cauet]

This is not minisat-related. You're not setting MROOT's value. replacing the line with something like
$ export MROOT=`pwd`
Should fix your problem.

Good look and enjoy minisat,
Bruno

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Daniele Nantes]

Hey!

thanks for your help! As you can see, I am starting with the thing. :)

I did what you have suggested, and now I have this:

Documents daninantes$ cd minisat/

minisat daninantes$ export MROOT=$PWD

minisat daninantes$ cd core

core daninantes$ make rs

Making dependencies

Compiling: core/Main.or

Compiling: core/Solver.or

Compiling: utils/Options.or

Compiling: utils/System.or

Linking: minisat_static ( core/Main.or core/Solver.or utils/Options.or utils/System.or )

ld: library not found for -lcrt0.o

collect2: ld returned 1 exit status

make: *** [minisat_static] Error 1

Do you know what is the problem?

Best,

--
Daniele Nantes
PhD Student

Departamento de Matemática

Universidade de Brasília
Department of Informatics
King's College London

www.mat.unb.br/~dnantes

[Niklas Sörensson]

Hi Daniele,

Static linking does not work on Mac OS X for some reason. Try "make r" for a dynamic build.

Regards,
Niklas

[Daniele Nantes]

Hi,

thanks for your advise. Now I have a minisat (exec). But when I do 

$minisat

I get

Reading from standard input... Use '--help' for help. 

and it runs forever.

Now I have this:

MacBook-Pro-de-Daniele-Nantes-Sobrinho:core daninantes$ make

Compiling: core/Main.o

Compiling: core/Solver.o

Compiling: utils/Options.o

Compiling: utils/System.o

Linking: minisat ( core/Main.o core/Solver.o utils/Options.o utils/System.o )

MacBook-Pro-de-Daniele-Nantes-Sobrinho:core daninantes$ minisat

Reading from standard input... Use '--help' for help.

^C

*** INTERRUPTED ***

restarts              : 0

conflicts             : 0              (0 /sec)

decisions             : 0              ( nan % random) (0 /sec)

propagations          : 0              (0 /sec)

conflict literals     : 0              ( nan % deleted)

Memory used           : 4.33 MB

CPU time              : 0.000348 s

*** INTERRUPTED ***

[Mate Soos]

Hi Daniele,

On 04/09/2013 03:54 PM, Daniele Nantes wrote:
> thanks for your advise. Now I have a minisat (exec). But when I do
>
> $minisat
>
> I get
>
> Reading from standard input... Use '--help' for help.

It's waiting for input, just type:

0 + Enter
Ctrl+D

and it should exit with UNSAT. If you want to use it in a more proper way:

$ minisat myfile.cnf

or

$ cat myfile | minisat

Mate

[dani nantes]

Thanks a lot for your help!

It is working now.. I am starting with minisat, and I didn't find any tutorial or short manual for beginners. It does not make it easy.

 Thank you again for the attention.

Kind regards,

[khushi chndrakar]

i m running .opb file through minisat+ getting optimal solution but  how could i know that how much memory (memory usage ) that file has taken .any command which  i can give in command line?

--

[Armin Biere]

http://www.cril.univ-artois.fr/~roussel/runsolver/
http://fmv.jku.at/runlim/

(I use the latter of course).

Armin