Commit c259a333 authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

CaDiCaL bind

parent 371f957a
/*
* Project SUBool
* Petr Kucera, 2022
*/
/**@file cadical_bind.cpp
* Binding class to CaDiCaL solver library. */
#include "cadical_bind.h"
void
SUBool::CadicalBind::SolverInit()
{
mSolver = std::make_unique<CaDiCaL::Solver>();
mResult = PartialValue::UNDEF;
Adapt();
}
bool
SUBool::CadicalBind::Reset(const CNF &cnf)
{
SolverInit();
return AddCnf(cnf);
}
bool
SUBool::CadicalBind::AddCnf(const CNF &cnf)
{
for (const auto &clause : cnf)
{
if (!AddClause(clause))
{
return false;
}
}
return true;
}
bool
SUBool::CadicalBind::AddClause(const Clause &clause)
{
mResult = PartialValue::UNDEF;
for (const auto &lit : clause)
{
mSolver->add(dimacs_literal(lit));
}
mSolver->add(0);
return (mResult != PartialValue::FALSE);
}
void
SUBool::CadicalBind::Interrupt() const
{
mSolver->terminate();
}
bool
SUBool::CadicalBind::Solve(const std::vector<Literal> &assump) const
{
mLitBuffer.clear();
std::for_each(assump.begin(), assump.end(),
[this](const auto &lit) { mLitBuffer.push_back(dimacs_literal(lit)); });
return SolveLitBuffer();
}
bool
SUBool::CadicalBind::Solve() const
{
mLitBuffer.clear();
return SolveLitBuffer();
}
bool
SUBool::CadicalBind::Solve(const PartialAssignment &assump) const
{
mLitBuffer.clear();
for (int i = 1; i <= static_cast<int>(assump.Size()); ++i)
{
if (assump[i] != PartialValue::UNDEF)
{
mLitBuffer.push_back(assump[i] == PartialValue::TRUE ? i : -i);
}
}
return SolveLitBuffer();
}
bool
SUBool::CadicalBind::Solve(const Assignment &assump) const
{
mLitBuffer.clear();
for (int i = 1; i <= static_cast<int>(assump.Size()); ++i)
{
mLitBuffer.push_back(assump[i] ? i : -i);
}
return SolveLitBuffer();
}
bool
SUBool::CadicalBind::SolveLitBuffer() const
{
for (const auto &lit : mLitBuffer)
{
mSolver->assume(lit);
}
auto ret = mSolver->solve();
if (ret == 20)
mResult = PartialValue::FALSE;
else if (ret == 10)
mResult = PartialValue::TRUE;
else
mResult = PartialValue::UNDEF;
IncreaseSolveCount(mResult);
if (mResult == PartialValue::UNDEF)
{
throw SolverTerminatedException(
"CadicalBind::Solve", "Solver finished without result");
}
return bool_of_partial_value(mResult);
}
/*
* Project SUBool
* Petr Kucera, 2017
* Petr Kucera, 2022
*/
/**@file glucose_bind.h
* Binding class to glucose solver library. */
/**@file cadical_bind.h
* Binding class to CaDiCaL solver library. */
#ifndef __CADICAL_BIND_H
#define __CADICAL_BIND_H
......@@ -18,13 +18,26 @@ namespace SUBool
{
class CadicalBind : public SolverInterface
{
private:
bool mCollectLearnts{false};
SolverInterface::ADAPTATION mAdapt{SolverInterface::ADAPTATION::DEFAULT};
std::unique_ptr<CaDiCaL::Solver> mSolver{};
mutable std::vector<int> mLitBuffer{};
mutable PartialValue mResult{PartialValue::UNDEF};
public:
CadicalBind(const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
CadicalBind(
bool collect_learnts, const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT)
: mCollectLearnts(collect_learnts), mAdapt(adapt)
{
SolverInit();
}
CadicalBind(const CNF &cnf, const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT)
: CadicalBind(adapt)
CadicalBind(const CNF &cnf, bool collect_learnts,
const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT)
: CadicalBind(collect_learnts, adapt)
{
AddCnf(cnf);
}
......@@ -52,6 +65,13 @@ namespace SUBool
virtual std::vector<Clause> ExtractLearnts() override;
virtual bool IsIncremental() const override;
virtual void Adapt(const SolverInterface::ADAPTATION adapt);
private:
void Adapt();
void SolverInit();
bool SolveLitBuffer() const;
};
using CadicalWrapper = SolverWrapperTemplate<CadicalBind>;
......
......@@ -141,13 +141,10 @@ template <class Solver>
bool
SUBool::KissatBind<Solver>::AddClause(const Clause &clause)
{
mLitBuffer.clear();
mResult = PartialValue::UNDEF;
for (const auto &lit : clause)
{
kissat_add(
mSolver->solver, lit.Positive() ? lit.Variable() : -lit.Variable());
mLitBuffer.push_back(lit.Positive() ? lit.Variable() : -lit.Variable());
kissat_add(mSolver->solver, dimacs_literal(lit));
}
kissat_add(mSolver->solver, 0);
return (mResult != PartialValue::FALSE);
......@@ -179,7 +176,7 @@ bool
SUBool::KissatBind<Solver>::Solve(const PartialAssignment &assump) const
{
mLitBuffer.clear();
for (unsigned i = 1; i <= assump.Size(); ++i)
for (int i = 1; i <= static_cast<int>(assump.Size()); ++i)
{
if (assump[i] != PartialValue::UNDEF)
{
......@@ -194,7 +191,7 @@ bool
SUBool::KissatBind<Solver>::Solve(const Assignment &assump) const
{
mLitBuffer.clear();
for (unsigned i = 1; i <= assump.Size(); ++i)
for (int i = 1; i <= static_cast<int>(assump.Size()); ++i)
{
mLitBuffer.push_back(assump[i] ? i : -i);
}
......
......@@ -57,7 +57,7 @@ SUBool::TestCadical::TestSimple() const
std::cout << "Testing CaDiCaL binding on a simple CNF" << std::endl;
auto cnf = Dimacs::parse_cnf(dimacs_quinn);
std::cout << "Input: " << cnf << std::endl;
CadicalWrapper wrap;
CadicalWrapper wrap(false);
auto &g = wrap.Solver();
if (!g.AddCnf(cnf))
{
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment