How to install it on VS2019?

[OrchidXu]

I'm new with SAT,the README has only told how to install on VS2015,which parameters needs to modify?

[msoos]

Nothing, it's the same :) Try and let me know how it went!

[josiahblaisdell]

Hi there, I compiled with VS2019, and I have linked/compiled my own program but when I reach this line it crashes: CMSat::SATSolver solver;

The message is: 'sat-fish.exe' (Win32): Loaded 'D:\src\courses\CS517\sat-fish\x64\Debug\sat-fish.exe'. Symbols loaded. 'sat-fish.exe' (Win32): Loaded 'C:\Windows\System32\ntdll.dll'. 'sat-fish.exe' (Win32): Loaded 'C:\Windows\System32\kernel32.dll'. 'sat-fish.exe' (Win32): Loaded 'C:\Windows\System32\KernelBase.dll'. 'sat-fish.exe' (Win32): Loaded 'D:\src\courses\CS517\sat-fish\cryptominisat5.exe'. Symbols loaded. 'sat-fish.exe' (Win32): Loaded 'C:\Windows\System32\msvcp140d.dll'. 'sat-fish.exe' (Win32): Loaded 'C:\Windows\System32\vcruntime140d.dll'. 'sat-fish.exe' (Win32): Loaded 'C:\Windows\System32\vcruntime140_1d.dll'. 'sat-fish.exe' (Win32): Loaded 'C:\Windows\System32\ucrtbased.dll'. The thread 0x20ac has exited with code 0 (0x0). Exception thrown at 0x00000000003E03BC in sat-fish.exe: 0xC0000005: Access violation executing location 0x00000000003E03BC.

In the call stack I see "cryptominisat.exe!_malloc_base(unsigned __int64 size) line 34

More info: I found this post: https://stackoverflow.com/questions/654696/how-to-debug-external-class-library-projects-in-visual-studio

I went ahead and performed the following steps:

• Tools -> Options -> Debugger
• Uncheck "Enable Just my Code"

This now casuses a different crash in "new_scalar.cpp" but I can see where it is crashing.... void* __CRTDECL operator new(size_t const size)

[a1880]

How do you call cryptominisat5.exe? To me, it looks like a parameter problem which leads to memory exhaustion. Can you debug cryptominisat5.exe standalone to find out, what's going on?

[josiahblaisdell]

cryptominisat5.exe seems to work when I run it stand alone. Here is the output: c Outputting solution to console c CryptoMiniSat version 5.7.1 c CMS Copyright Mate Soos (soos.mate@gmail.com) c CMS SHA revision 0544260ae1d4338c260930dce8a6cc0512d3e1fb c CMS is MIT licensed c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14 c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96, c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]' c by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015 c CMS compilation env CMAKE_CXX_COMPILER = C:/Program Files (x86)/Microsoft Visual Studio/2019/Enterprise/VC/Tools/MSVC/14.23.28105/bin/Hostx64/x64/cl.exe | CMAKE_CXX_FLAGS = /DWIN32 /D_WINDOWS /W3 /GR /EHsc | COMPILE_DEFINES = | STATICCOMPILE = ON | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND = | ZLIB_FOUND = | VALGRIND_FOUND = | ENABLE_TESTING = OFF | M4RI_FOUND = FALSE | NOM4RI = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = D:/python38/python.exe | PYTHON_LIBRARY = D:/python38/libs/python38.lib | PYTHON_INCLUDE_DIRS = D:/python38/include | MY_TARGETS = | LARGEMEM = OFF | LIMITMEM = OFF | compilation date time = May 26 2020 14:24:07 c CMS compiled with non-gcc compiler c Executed with command line: D:\src\courses\CS517\sat-fish\cryptominisat5.exe c Reading from standard input... Use '-h' or '--help' for help. c -- clauses added: 0 c INTERRUPTED c -- xor clauses added: 0 c -- vars added 0

c Parsing time: 18.98 s No clauses or variables were put into the solver, exiting without stats

[josiahblaisdell]

I am not sure what you mean by "how do you call cryptominisat.exe?" And I'm wondering if that has something to do with it. I have placed cryptominisat.exe in the build directory. I have also added the cryptominisat libraries to the "Additional Dependencies". Is this what you mean?

In the example code on the git readme it says to just call: CMSat::SATSolver solver;

But you seem to suggest there is some way to call cryptominisat5.exe? I don't want to call the executable, I want to use the cryptominisat library. I am trying to implement this paper: "Satisfiability and Integer Programming As Complementary Tools" (Li et al., 1998)

Hope this helps, thank you for your assistance.

[josiahblaisdell]

Oh my gosh I think I fixed it.... To fix I did the following:

1. recompiled the cryptominisat program using the settings from the cmake config below (and Ninja)
2. Set the solution configuration from Debug to Release
3. Visual Studio -> Project Properties -> C/C++ -> Code Generation -> Set Runtime Library to Multi-threaded (/MT)
4. Visual Studio -> Project Properties -> C/C++ -> Code Generation -> Set "Security Check" to Disable
5. Visual Studio -> Project Properties -> Linker -> Input -> added cryptominisat5win.lib;cryptominisat5_simple.lib; to the additional dependencies

cmake Config is attached. CMakeCache.txt

[a1880]

I was misled by cryptominisat5.exe and cryptominisat.exe being mentioned in your message output. Therefore, I thought that you are calling cryptominisat5.exe as external process rather than as library call. I am glad that it works for you by now.