Minisat in Visual Studio

[Paul Diac]

Hello,
  Is there a simple way to port Minisat to a specific (if necessary), version of Visual Studio?
  Or are there any other IDEs on windows that can handle Minisat better? (with debug .. )
  Thank you,
 Paul Diac

[Niklas Sörensson]

On Thu, Apr 21, 2011 at 7:50 AM, Paul Diac <paul....@gmail.com> wrote:
>
> Hello,
>   Is there a simple way to port Minisat to a specific (if necessary),
> version of Visual Studio?

It shouldn't be very hard, but I don't run Windows and have little
time to do the porting. That I'm unfamiliar with Visual Studio does
not help either. I'm hoping to do this at some point, but can't make
promises :)

>   Or are there any other IDEs on windows that can handle Minisat better?
> (with debug .. )

I think compiling with cygwin will be easier but still will not work
completely as-is.

Best Regards,

/Niklas

[Michael Tautschnig]

[...]

> >   Or are there any other IDEs on windows that can handle Minisat better?
> > (with debug .. )
>
> I think compiling with cygwin will be easier but still will not work
> completely as-is.
>

I haven't tried the most recent git HEAD, but early 2.2.0 versions do
work fine, both with cygwin and MinGW/MSys, with only minimal patching
(which might even already be included in current git HEAD; if not,
Niklas, feel free to use it) - patch is shown below.

Best regards,
Michael

diff --git a/minisat-2.2.0/core/Main.cc b/minisat-2.2.0/core/Main.cc
index 4388c3e..31b8a30 100644
--- a/minisat-2.2.0/core/Main.cc
+++ b/minisat-2.2.0/core/Main.cc
@@ -96,8 +96,12 @@ int main(int argc, char** argv)
// Use signal handlers that forcibly quit until the solver
will be able to respond to
// interrupts:
signal(SIGINT, SIGINT_exit);
+#ifdef SIGXCPU
signal(SIGXCPU,SIGINT_exit);
+#endif
+

+#if !defined(_MSC_VER) && !defined(__MINGW32__)
// Set limit on CPU-time:
if (cpu_lim != INT32_MAX){
rlimit rl;
@@ -118,6 +122,7 @@ int main(int argc, char** argv)
if (setrlimit(RLIMIT_AS, &rl) == -1)
printf("WARNING! Could not set resource limit:
Virtual memory.\n");
} }
+#endif

if (argc == 1)
printf("Reading from standard input... Use '--help' for
help.\n");
@@ -146,7 +151,9 @@ int main(int argc, char** argv)
// Change to signal-handlers that will only notify the solver
and allow it to terminate
// voluntarily:
signal(SIGINT, SIGINT_interrupt);
+#ifdef SIGXCPU
signal(SIGXCPU,SIGINT_interrupt);
+#endif

if (!S.simplify()){
if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
diff --git a/minisat-2.2.0/simp/Main.cc b/minisat-2.2.0/simp/Main.cc
index e59d73b..af7da39 100644
--- a/minisat-2.2.0/simp/Main.cc
+++ b/minisat-2.2.0/simp/Main.cc
@@ -22,7 +22,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
OTHER DEALINGS IN THE SOFTWA

#include <signal.h>
#include <zlib.h>
+#if !defined(_MSC_VER) && !defined(__MINGW32__)
#include <sys/resource.h>
+#endif

#include "utils/System.h"
#include "utils/ParseUtils.h"
@@ -100,8 +102,11 @@ int main(int argc, char** argv)
// Use signal handlers that forcibly quit until the solver
will be able to respond to
// interrupts:
signal(SIGINT, SIGINT_exit);
+#ifdef SIGXCPU
signal(SIGXCPU,SIGINT_exit);
+#endif

+#if !defined(_MSC_VER) && !defined(__MINGW32__)
// Set limit on CPU-time:
if (cpu_lim != INT32_MAX){
rlimit rl;
@@ -122,6 +127,7 @@ int main(int argc, char** argv)
if (setrlimit(RLIMIT_AS, &rl) == -1)
printf("WARNING! Could not set resource limit:
Virtual memory.\n");
} }
+#endif

if (argc == 1)
printf("Reading from standard input... Use '--help' for
help.\n");
@@ -149,7 +155,9 @@ int main(int argc, char** argv)
// Change to signal-handlers that will only notify the solver
and allow it to terminate
// voluntarily:
signal(SIGINT, SIGINT_interrupt);
+#ifdef SIGXCPU
signal(SIGXCPU,SIGINT_interrupt);
+#endif

S.eliminate(true);
double simplified_time = cpuTime();

[Niklas Sörensson]

Hello Michael,

On Wed, Apr 27, 2011 at 2:14 PM, Michael Tautschnig
<michael.t...@googlemail.com> wrote:
> [...]
>> >   Or are there any other IDEs on windows that can handle Minisat better?
>> > (with debug .. )
>>
>> I think compiling with cygwin will be easier but still will not work
>> completely as-is.
>>
>
> I haven't tried the most recent git HEAD, but early 2.2.0 versions do
> work fine, both with cygwin and MinGW/MSys, with only minimal patching
> (which might even already be included in current git HEAD; if not,
> Niklas, feel free to use it) - patch is shown below.

I've tried to match this in current HEAD but have not yet had chance
to try it on any Windows-type build.

Thanks,

/Niklas

[svadimr]

I successfully built minisat on windows in visual studio without
cygwin or others. There are several small steps that should be done,
if you can wait till next Wednesday I can make a guide.

Vadim

On Apr 28, 7:56 pm, Niklas Sörensson <nikla...@gmail.com> wrote:
> Hello Michael,
>
> On Wed, Apr 27, 2011 at 2:14 PM, Michael Tautschnig
>

[Shayak Lahiri]

Hi Vadim,

Waiting for your guide. Many thanks in advance.
It would be a great help.

Shayak

[svadimr]

I just wrote this step by step, sorry for the disorder but it's really
late at night now:

download minisat2.2 from the website
extract the files
open visual studio (I'm working with 2010, butI did it for 2008 as
well)
File -> New -> Project
Win32 Console Application
Location -> the location of the project I'll use "Location" (we will
need later)
Name -> I will use "Minisat"
Ok -> Next
Choose "Empty Project"
Finish
Copy mtl, core, simp, utils directories to Location/Minisat/Minisat/

From now we will work with visual studio:
Add all header and cc files to the project
Pay attention to add only one main.cc file (usually the one under simp
directory in order to use preprocessing)

Create another directory "win" under Location/Minisat/Minisat (under
project directory)
Put there:
zconf.h
zdll.exp
zdll.lib
zlib.def
zlib.h

Add .h and .lib to the project

Put:
zlib1.dll under Location/Minisat/Minisat

Open project properties -> C/C++ -> General
Additional Include Directories: $(SolutionDir)\$(ProjectName)\;

Replace staff in files:

IntTypes.h
replace:
#else

# include <stdint.h>
# include <inttypes.h>

#endif

with:

#elif _MSC_VER

# include <stdint.h>

#else

# include <stdint.h>
# include <inttypes.h>

#endif

Main.cc
replace:
# include <zlib.h>
# include <sys/resource.h>

with:
#ifdef _MSC_VER
# include <win/zlib.h>
#else
# include <zlib.h>
# include <sys/resource.h>
#endif

replace:
void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", solver.starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n",
solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random)
(%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 /
(float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n",
solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)
\n", solver.tot_literals, (solver.max_literals -
solver.tot_literals)*100 / (double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n",
mem_used);
printf("CPU time : %g s\n", cpu_time);
}

With:
void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %-12lld\n", solver.starts);
printf("conflicts : %-12lld (%.0f /sec)\n",
solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12lld (%4.2f %% random) (%.0f /
sec)\n", solver.decisions, (float)solver.rnd_decisions*100 /
(float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12lld (%.0f /sec)\n",
solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12lld (%4.2f %% deleted)\n",
solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 /
(double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n",
mem_used);
printf("CPU time : %g s\n", cpu_time);
}

After:
signal(SIGINT, SIGINT_exit);
add:
#ifndef _MSC_VER

Before:

if (argc == 1)
printf("Reading from standard input... Use '--help' for
help.\n");

add:
#endif

replace:
signal(SIGXCPU,SIGINT_interrupt);
with:
#ifndef _MSC_VER
signal(SIGXCPU,SIGINT_interrupt);
#endif

ParseUtils.h
replace:
# include <zlib.h>

with:
#ifdef _MSC_VER
# include <win/zlib.h>
#else
# include <zlib.h>
#endif

System.cc
add before #endif in the last line:
double Minisat::memUsedPeak() {
return 0; }

[vikrant 75]

hello svadimr

can you tell how to input .cnf file in Visual Studio. I made the modifications u said, now when i run this program the exe stops working

here's what i do:-

I input  XYZ.cnf file in properties->debugging->command line argument

And then i run the program.

the screen shows: "problem statistics" and then MAIN.exe stop working

thanks 

[henry@Tianjin University]

Hello, svadimr. After reading your guide , I did it step by step, but I have a question . Which version of zlib should I download ? I download zlib 1.2.8, I can't find zdll.lib and zdll.exp. By the way, I want to run minisat in eclipse under ubuntu 13.04, do you know how to run it ? Thanks!

在 2011年6月16日星期四UTC+8上午11时31分40秒，svadimr写道：

[svadimr]

Sorry for late response only now noticed it. Be sure to place zlib.lib in the correct place it is ususally the problem.

[svadimr]

I attached the files to make your life easier for windows. To run minisat in eclipse under ubuntu, you don't really need to do anything but configure eclipse to run the correct makefile. Nothing else is required.

Good luck,

Vadim.