I want to run cryptominisat in c ++, but I can't run it because of undefined reference to

Question

I want to use cryptominisat but I don't know how to do it.

I did Compiling in Linux.

sudo apt-get install build-essential cmake
# not required but very useful
sudo apt-get install zlib1g-dev libboost-programoptions-dev libm4ri-dev libsqlite3-dev help2man
tar xzvf cryptominisat-version.tar.gz
cd cryptominisat-5.8.0
mkdir build && cd build
cmake ..
make
sudo make install
sudo ldconfig

After that, I create sat_test.cpp and wrote the following in sat_test.cpp

#include <cryptominisat5/cryptominisat.h>
#include <assert.h>
#include <vector>
using std::vector;
using namespace CMSat;

int main()
{
SATSolver solver;
vector<Lit> clause;

//Let's use 4 threads
solver.set_num_threads(4);

//We need 3 variables. They will be: 0,1,2
//Variable numbers are always trivially increasing
solver.new_vars(3);

//add "1 0"
clause.push_back(Lit(0, false));
solver.add_clause(clause);

//add "-2 0"
clause.clear();
clause.push_back(Lit(1, true));
solver.add_clause(clause);

//add "-1 2 3 0"
clause.clear();
clause.push_back(Lit(0, true));
clause.push_back(Lit(1, false));
clause.push_back(Lit(2, false));
solver.add_clause(clause);

lbool ret = solver.solve();
assert(ret == l_True);
std::cout
<< "Solution is: "
<< solver.get_model()[0]
<< ", " << solver.get_model()[1]
<< ", " << solver.get_model()[2]
<< std::endl;

//assumes 3 = FALSE, no solutions left
vector<Lit> assumptions;
assumptions.push_back(Lit(2, true));
ret = solver.solve(&assumptions);
assert(ret == l_False);

//without assumptions we still have a solution
ret = solver.solve();
assert(ret == l_True);

//add "-3 0"
//No solutions left, UNSATISFIABLE returned
clause.clear();
clause.push_back(Lit(2, true));
solver.add_clause(clause);
ret = solver.solve();
assert(ret == l_False);

return 0;
}

the way I did the compilation and the result is as follows.
compile

$ g++ sat_test.cpp
    /usr/bin/ld: /tmp/ccZrqNZN.o: in function `main':
    sat_test.cpp:(.text+0x2e): undefined reference to `CMSat::SATSolver::SATSolver(void*,std::atomic<bool>*)'
    /usr/bin/ld: sat_test.cpp:(.text+0x4b): undefined reference to `CMSat::SATSolver::set_num_threads(unsigned int)'
    /usr/bin/ld: sat_test.cpp:(.text+0x5c): undefined reference to `CMSat::SATSolver::new_vars(unsigned long)'
    /usr/bin/ld: sat_test.cpp:(.text+0x98): undefined reference to `CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)'
    /usr/bin/ld: sat_test.cpp:(.text+0xe0): undefined reference to `CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)'
    /usr/bin/ld: sat_test.cpp:(.text+0x17a): undefined reference to `CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)'
    /usr/bin/ld: sat_test.cpp:(.text+0x190): undefined reference to `CMSat::SATSolver::solve(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const*, bool)'
    /usr/bin/ld: sat_test.cpp:(.text+0x1ed): undefined reference to `CMSat::SATSolver::get_model() const'
    /usr/bin/ld: sat_test.cpp:(.text+0x223): undefined reference to `CMSat::SATSolver::get_model() const'
    /usr/bin/ld: sat_test.cpp:(.text+0x259): undefined reference to `CMSat::SATSolver::get_model() const'
    /usr/bin/ld: sat_test.cpp:(.text+0x2d3): undefined reference to `CMSat::SATSolver::solve(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const*, bool)'
    /usr/bin/ld: sat_test.cpp:(.text+0x324): undefined reference to `CMSat::SATSolver::solve(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const*, bool)'
    /usr/bin/ld: sat_test.cpp:(.text+0x3a7): undefined reference to `CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)'
    /usr/bin/ld: sat_test.cpp:(.text+0x3bd): undefined reference to `CMSat::SATSolver::solve(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const*, bool)'
    /usr/bin/ld: sat_test.cpp:(.text+0x421): undefined reference to `CMSat::SATSolver::~SATSolver()'
    /usr/bin/ld: sat_test.cpp:(.text+0x468): undefined reference to `CMSat::SATSolver::~SATSolver()'
    collect2: error: ld returned 1 exit status

I know from the result that undefine is the reason why I can't run it,but I don't know what to do. Please help me.
I was able to use cryptominisat on the command line.

$ cryptominisat5 --verb 0 file.cnf
s SATISFIABLE
v 1 -2 3 0

score 0 · Accepted Answer · answered Aug 19 '21 at 11:53

You forgot to link with cryptominisat5 library, compile like this:

g++ sat_test.cpp -lcryptominisat5

Or even better, use CMake:

cmake_minimum_required(VERSION 3.15)
project(test VERSION 1.0 LANGUAGES CXX)

add_executable(sat_test sat_test.cpp)
target_link_libraries(sat_test PRIVATE cryptominisat5)

I want to run cryptominisat in c ++, but I can't run it because of undefined reference to

1 Answers1