Hi all,
I am new in this Forum, but I have used Lazarus for approx 8 years (under linux and windows). I would like to program a simple GUI (something like a time-table) which encodes a problem in CNF, calls another program called
Cryptominisat to solve the problem, and then constructs and shows the time-table.
I've already implemented the program in:
JAVA --> Worked, but I could not integrate Cryptominisat, so I had to work with files to communicate with Cryptominisat. And not all users are allowed to install JAVA on their PCs.
QT --> Worked, but I was not able to cross compile for windows and I was not able to create a single executable in Linux.
What I want:
- integration of Cryptominisat (
https://github.com/msoos/cryptominisat)
- single executable in windows
- single executable in linux
Is this possible and how would I call/convert these lines?
#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
solver.new_vars(3);
//adds "1 0"
clause.push_back(Lit(0, false));
solver.add_clause(clause);
//adds "-2 0"
clause.clear();
clause.push_back(Lit(1, true));
solver.add_clause(clause);
//adds "-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);
assert(solver.get_model()[0] == l_True);
assert(solver.get_model()[1] == l_False);
assert(solver.get_model()[2] == l_True);
std::cout
<< "Solution is: "
<< solver.get_model()[0]
<< ", " << solver.get_model()[1]
<< ", " << solver.get_model()[2]
<< std::endl;
return 0;
}
Thank you for your time