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

Started implementing CaDiCaL support

parent 26ff4b50
......@@ -88,6 +88,38 @@ function(su_add_kissat_lib libs)
endfunction(su_add_kissat_lib)
# END of KISSAT related part
# CaDiCaL related part
option(USE_CADICAL "If the project should compile with CaDiCaL support" ON)
if(USE_CADICAL)
if(DEFINED ENV{CADICAL_HOME})
set (CADICAL_HOME $ENV{CADICAL_HOME})
message(STATUS "Using CADICAL_HOME=${CADICAL_HOME}")
else()
set (CADICAL_HOME ${SUBool_SOURCE_DIR}/solvers/cadical)
message(STATUS "CADICAL_HOME not defined, using default CADICAL_HOME=${CADICAL_HOME}")
endif()
find_library(CADICAL_LIB cadical ${CADICAL_HOME}/build)
if(CADICAL_LIB)
message(STATUS "Using CADICAL_LIB: ${CADICAL_LIB}")
include_directories(SYSTEM "${CADICAL_HOME}/src")
add_compile_definitions(CADICAL_H="cadical.hpp")
add_compile_definitions(HAS_CADICAL=1)
else()
message(WARNING "CaDiCaL lib not found, CaDiCaL support is switched off")
set(CADICAL_LIB "")
set(USE_CADICAL OFF)
endif()
else()
message(STATUS "CaDiCaL support will not be available")
endif()
function(su_add_cadical_lib libs)
if(USE_CADICAL)
set(${libs} ${${libs}} ${CADICAL_LIB} PARENT_SCOPE)
endif()
endfunction(su_add_cadical_lib)
# END of CADICAL related part
include_directories (BEFORE SYSTEM ${Boost_INCLUDE_DIRS})
include_directories (${SUBool_SOURCE_DIR}/lib)
include_directories (SYSTEM ${GLUCOSE_HOME})
......
USE_KISSAT=ON
USE_CADICAL=ON
all:
cd build && make
......
/*
* Project SUBool
* Petr Kucera, 2017
*/
/**@file glucose_bind.h
* Binding class to glucose solver library. */
#ifndef __CADICAL_BIND_H
#define __CADICAL_BIND_H
#if HAS_CADICAL
#include CADICAL_H
#include "random_utils.h"
#include "solver_bind.h"
namespace SUBool
{
class CadicalBind : public SolverInterface
{
public:
CadicalBind(const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT);
CadicalBind(const CNF &cnf, const SolverInterface::ADAPTATION adapt =
SolverInterface::ADAPTATION::DEFAULT)
: CadicalBind(adapt)
{
AddCnf(cnf);
}
virtual bool Reset(const CNF &cnf) override;
virtual bool AddCnf(const CNF &cnf) override;
virtual bool AddClause(const Clause &clause) override;
virtual void Interrupt() const override;
virtual bool Solve(const std::vector<Literal> &assump) const override;
virtual bool Solve() const override;
virtual bool Solve(const PartialAssignment &assump) const override;
virtual bool Solve(const Assignment &assump) const override;
/* Throws NoModelException if no model is currently
* available. */
virtual PartialValue ValueOfVariable(unsigned var) const override;
virtual PartialValue ValueOfLiteral(const Literal &lit) const override;
virtual PartialAssignment Model() const override;
virtual Clause ConflictClause() const override;
virtual size_t LearntsSize() const override;
virtual std::vector<Clause> Learnts() const override;
virtual std::vector<Clause> ExtractLearnts() override;
virtual bool IsIncremental() const override;
};
using CadicalWrapper = SolverWrapperTemplate<CadicalBind>;
} // namespace SUBool
#endif // HAS_CADICAL
#endif // __CADICAL_BIND_H
......@@ -197,7 +197,7 @@ SUBool::solve_with_learning(const CNF &prime, const CNF &cnf,
auto r = g.Solve(assump);
if (learned)
{
learned->Append(g.Learnts());
learned->Append(g.ExtractLearnts());
}
if (!r)
{
......
......@@ -284,7 +284,7 @@ SUBool::CompHypothesis::NextLearnedClause()
void
SUBool::CompHypothesis::ExtractLearnts()
{
auto learnts = mSolver.Solver().Learnts();
auto learnts = mSolver.Solver().ExtractLearnts();
logs.TLog(3) << "Extracted " << learnts.size() << " learnts from the solver"
<< std::endl;
size_t cnt = 0;
......
......@@ -139,6 +139,7 @@ namespace SUBool
virtual size_t LearntsSize() const override;
virtual std::vector<Clause> Learnts() const override;
virtual std::vector<Clause> ExtractLearnts() override;
virtual bool IsIncremental() const override;
};
......@@ -220,9 +221,8 @@ bool
SUBool::GlucoseBind<Solver>::Solve(const std::vector<Literal> &assump) const
{
mLitBuffer.clear();
std::for_each(assump.begin(), assump.end(), [this](const auto &lit) {
mLitBuffer.push(glucose_lit(lit));
});
std::for_each(assump.begin(), assump.end(),
[this](const auto &lit) { mLitBuffer.push(glucose_lit(lit)); });
return SolveLitBuffer();
}
......@@ -263,8 +263,8 @@ SUBool::GlucoseBind<Solver>::SolveLitBuffer() const
IncreaseSolveCount(mResult);
if (mResult == PartialValue::UNDEF)
{
throw SolverTerminatedException("GlucoseBind::Solve",
"Solver finished without result");
throw SolverTerminatedException(
"GlucoseBind::Solve", "Solver finished without result");
}
return bool_of_partial_value(mResult);
}
......@@ -282,8 +282,8 @@ SUBool::GlucoseBind<Solver>::ValueOfVariable(unsigned var) const
{
if (!bool_of_partial_value(mResult, false))
{
throw NoModelException("GlucoseBind::ValueOfVariable",
"No model available");
throw NoModelException(
"GlucoseBind::ValueOfVariable", "No model available");
}
return of_glucose_value(mSolver->modelValue(var - 1));
}
......@@ -294,8 +294,8 @@ SUBool::GlucoseBind<Solver>::ValueOfLiteral(const Literal &lit) const
{
if (!bool_of_partial_value(mResult, false))
{
throw NoModelException("GlucoseBind::ValueOfLiteral",
"No model available");
throw NoModelException(
"GlucoseBind::ValueOfLiteral", "No model available");
}
return of_glucose_value(mSolver->modelValue(glucose_lit(lit)));
}
......@@ -344,6 +344,13 @@ SUBool::GlucoseBind<Solver>::Learnts() const
return learnts;
}
template <class Solver>
std::vector<SUBool::Clause>
SUBool::GlucoseBind<Solver>::ExtractLearnts()
{
return Learnts();
}
template <class Solver>
size_t
SUBool::GlucoseBind<Solver>::LearntsSize() const
......
......@@ -24,20 +24,18 @@ SUBool::ImplicateChecker::IsImplicate(const CNF &cnf, const Clause &clause)
SimpSolverWrapper wrap(cnf);
auto &g = wrap.Solver();
auto r = is_implicate(g, clause);
AddToLearnts(g.Learnts());
AddToLearnts(g.ExtractLearnts());
return r;
}
std::optional<SUBool::Clause>
SUBool::ImplicateChecker::PrimeSubimplicate(const CNF &cnf,
const Clause &clause,
unsigned ignore_var,
bool promised_sat)
const Clause &clause, unsigned ignore_var, bool promised_sat)
{
IncSolverWrapper wrap(cnf);
auto &g = wrap.Solver();
auto prime = prime_subimplicate(cnf, clause, ignore_var, promised_sat);
AddToLearnts(g.Learnts());
AddToLearnts(g.ExtractLearnts());
return prime;
}
......@@ -66,12 +64,12 @@ SUBool::ImplicateChecker::LearnedSize() const
}
bool
SUBool::ImplicateChecker::Solve(const CNF &cnf,
const std::vector<Literal> &assump)
SUBool::ImplicateChecker::Solve(
const CNF &cnf, const std::vector<Literal> &assump)
{
SimpSolverWrapper wrap(cnf);
auto &g = wrap.Solver();
auto result = g.Solve(assump);
AddToLearnts(g.Learnts());
AddToLearnts(g.ExtractLearnts());
return result;
}
......@@ -94,6 +94,7 @@ namespace SUBool
virtual size_t LearntsSize() const override;
virtual std::vector<Clause> Learnts() const override; // TODO:
virtual std::vector<Clause> ExtractLearnts() override;
virtual bool IsIncremental() const override;
};
......@@ -144,8 +145,8 @@ SUBool::KissatBind<Solver>::AddClause(const Clause &clause)
mResult = PartialValue::UNDEF;
for (const auto &lit : clause)
{
kissat_add(mSolver->solver,
lit.Positive() ? lit.Variable() : -lit.Variable());
kissat_add(
mSolver->solver, lit.Positive() ? lit.Variable() : -lit.Variable());
mLitBuffer.push_back(lit.Positive() ? lit.Variable() : -lit.Variable());
}
kissat_add(mSolver->solver, 0);
......@@ -165,9 +166,11 @@ bool
SUBool::KissatBind<Solver>::Solve(const std::vector<Literal> &assump) const
{
mLitBuffer.clear();
std::for_each(assump.begin(), assump.end(), [this](const auto &lit) {
mLitBuffer.push_back(lit.mPositive ? lit.Variable() : -lit.Variable());
});
std::for_each(assump.begin(), assump.end(),
[this](const auto &lit) {
mLitBuffer.push_back(
lit.mPositive ? lit.Variable() : -lit.Variable());
});
return SolveLitBuffer();
}
......@@ -217,8 +220,8 @@ SUBool::KissatBind<Solver>::SolveLitBuffer() const
IncreaseSolveCount(mResult);
if (mResult == PartialValue::UNDEF)
{
throw SolverTerminatedException("KissatBind::Solve",
"Solver finished without result");
throw SolverTerminatedException(
"KissatBind::Solve", "Solver finished without result");
}
return bool_of_partial_value(mResult);
}
......@@ -236,8 +239,8 @@ SUBool::KissatBind<Solver>::ValueOfVariable(unsigned var) const
{
if (!bool_of_partial_value(mResult, false))
{
throw NoModelException("KissatBind::ValueOfVariable",
"No model available");
throw NoModelException(
"KissatBind::ValueOfVariable", "No model available");
}
return of_kissat_value(kissat_value(mSolver->solver, var));
}
......@@ -248,8 +251,8 @@ SUBool::KissatBind<Solver>::ValueOfLiteral(const Literal &lit) const
{
if (!bool_of_partial_value(mResult, false))
{
throw NoModelException("KissatBind::ValueOfLiteral",
"No model available");
throw NoModelException(
"KissatBind::ValueOfLiteral", "No model available");
}
return of_kissat_value(kissat_value(
mSolver->solver, lit.mPositive ? lit.Variable() : -lit.Variable()));
......@@ -275,8 +278,8 @@ template <class Solver>
SUBool::Clause
SUBool::KissatBind<Solver>::ConflictClause() const
{
throw NotImplementedException("KissatBind::ConflictClause",
"Not implemented");
throw NotImplementedException(
"KissatBind::ConflictClause", "Not implemented");
/* // TODO: not working
std::vector<Literal> conflict_literals;
if (mSolver->solver->conflict.used)
......@@ -301,6 +304,16 @@ SUBool::KissatBind<Solver>::Learnts() const // TODO:
// return learnts;
}
template <class Solver>
std::vector<SUBool::Clause>
SUBool::KissatBind<Solver>::ExtractLearnts() // TODO:
{
throw NotImplementedException(
"KissatBind::ExtractLearnts", "Not implemented");
// std::vector<SUBool::Clause> learnts;
// return learnts;
}
template <class Solver>
size_t
SUBool::KissatBind<Solver>::LearntsSize() const
......
......@@ -72,6 +72,7 @@ namespace SUBool
constexpr unsigned positive_literal_index(unsigned var) noexcept;
constexpr unsigned negative_literal_index(unsigned var) noexcept;
constexpr int dimacs_literal(const Literal &lit) noexcept;
std::vector<Literal> literals_of_assignment(const Assignment &alpha);
std::vector<Literal> literals_of_assignment(const PartialAssignment &alpha);
......@@ -151,6 +152,13 @@ SUBool::negative_literal_index(unsigned var) noexcept
return 2 * var - 1;
}
constexpr int
SUBool::dimacs_literal(const Literal &lit) noexcept
{
return (lit.Positive() ? static_cast<int>(lit.Variable())
: -static_cast<int>(lit.Variable()));
}
constexpr unsigned
SUBool::Literal::Index() const noexcept
{
......
......@@ -99,6 +99,8 @@ namespace SUBool
virtual size_t LearntsSize() const = 0;
virtual std::vector<Clause> Learnts() const = 0;
// Clears internal learnts cache if there is any
virtual std::vector<Clause> ExtractLearnts() = 0;
virtual bool IsIncremental() const = 0;
};
......
cmake_minimum_required (VERSION 3.0.2)
function(su_add_test_exec name use_glucose use_kissat)
function(su_add_test_exec name use_inc_solver use_kissat)
set(ATE_LIBS test_${name} subool)
set(ATE_SRC test_${name}.cpp)
if (${use_glucose})
if (${use_inc_solver})
su_add_glucose_lib(ATE_LIBS)
su_add_cadical_lib(ATE_LIBS)
endif()
if (${use_kissat})
su_add_kissat_lib(ATE_LIBS)
......@@ -26,6 +27,7 @@ if(USE_KISSAT)
su_add_test_exec(kissat true true)
endif()
su_add_test_exec(glucose true true)
su_add_test_exec(cadical true true)
su_add_test_exec(cnfcompress false false)
su_add_test_exec(cnfutil true true)
su_add_test_exec(canon true true)
......
/*
* Project SUBool
* Petr Kucera, 2022
*/
/**@file test_cadical.cpp
* Test connection to cadical library.
*/
#include <chrono>
#include <sstream>
#include "cadical_bind.h"
#include "cnfutil.h"
#include "dimacs.h"
#include "random_utils.h"
#include "test_cadical.h"
#include "util.h"
const char *dimacs = "p cnf 8 8\n"
"1 2 5 0\n"
"-5 3 4 0\n"
"1 2 6 0\n"
"-6 -3 4 0\n"
"1 2 7 0\n"
"-7 3 -4 0\n"
"1 2 8 0\n"
"-8 -3 -4 0\n";
const char *dimacs_1 = "c 1 clause\n"
"p cnf 3 1\n"
"-1 2 -3 0";
const char *dimacs_quinn = "c quinn.cnf\n"
"c\n"
"p cnf 16 18\n"
" 1 2 0\n"
" -2 -4 0\n"
" 3 4 0\n"
" -4 -5 0\n"
" 5 -6 0\n"
" 6 -7 0\n"
" 6 7 0\n"
" 7 -16 0\n"
" 8 -9 0\n"
" -8 -14 0\n"
" 9 10 0\n"
" 9 -10 0\n"
"-10 -11 0\n"
" 10 12 0\n"
" 11 12 0\n"
" 13 14 0\n"
" 14 -15 0\n"
" 15 16 0";
bool
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;
auto &g = wrap.Solver();
if (!g.AddCnf(cnf))
{
std::cout << "CaDiCaL returned false when adding CNF [FAILED]"
<< std::endl;
return false;
}
bool result = g.Solve();
std::cout << "CaDiCaL solve result: " << result
<< (result ? " [PASSED]" : " [FAILED]") << std::endl;
PartialAssignment alpha = g.Model();
std::cout << "Model: " << alpha << std::endl;
auto val = cnf.Value(alpha);
std::cout << "Value on model: " << val << std::endl;
return (val == PartialValue::TRUE);
}
#if 0
bool
SUBool::TestGlucose::TestLearntsRandom(const unsigned nrounds,
const unsigned nclauses, const unsigned clause_size,
const unsigned nvars) const
{
std::cout << "Testing glucose learnts" << std::endl;
for (unsigned round = 0; round < nrounds; ++round)
{
CNF cnf = random_k_cnf(nclauses, clause_size, nvars);
std::cout << "Round " << round + 1 << std::endl;
//<<", cnf:"<<std::endl; std::cout<<cnf;
SimpSolverWrapper wrap;
auto &g = wrap.Solver();
if (!g.AddCnf(cnf))
{
std::cout << "Glucose returned false when adding CNF [FAILED]"
<< std::endl;
return false;
}
std::vector<Literal> assump(5);
std::cout << "Using assumptions:";
for (unsigned i = 0; i < assump.size(); ++i)
{
assump[i] = Literal(i + 1, (sub_rand() % 2) == 0);
std::cout << " " << assump[i];
}
std::cout << std::endl;
bool result = g.Solve(assump);
std::cout << "Glucose solve result: " << (result ? "SAT" : "UNSAT")
<< std::endl;
auto learnts = g.Learnts();
std::cout << "...nLearnts=" << learnts.size() << std::endl;
bool all_implicates = true;
for (const auto &clause : learnts)
{
std::cout << clause;
if (!is_implicate(cnf, clause))
{
std::cout << " !not implicate!";
all_implicates = false;
}
std::cout << std::endl;
}
if (all_implicates)
{
std::cout << "All learnts are implicates [PASSED]" << std::endl;
}
else
{
std::cout << "Not all learnts are implicates [FAILED]" << std::endl;
return false;
}
}
return true;
}
bool
SUBool::TestGlucose::TestConflict(
const CNF &cnf, const std::vector<Literal> &assumptions) const
{
std::cout << "Testing glucose conflict clause with assumptions: ";
for (unsigned i = 0; i < assumptions.size(); ++i)
{
std::cout << " " << assumptions[i];
}
std::cout << std::endl;
SimpSolverWrapper wrap;
auto &g = wrap.Solver();
g.AddCnf(cnf);
if (g.Solve(assumptions))
{
std::cout << "no conflict [OK]" << std::endl;
return true;
}
auto c = g.ConflictClause();
std::cout << "... conflict clause: " << c << std::endl;
if (!is_implicate(cnf, c))
{
return false;
}
std::unordered_set<Literal> assump_set(
assumptions.begin(), assumptions.end());
for (const auto &lit : c)
{
if (assump_set.find(lit.Negation()) == assump_set.end())
{
return false;
}
}
return true;
}
bool
SUBool::TestGlucose::TestConflicts(const unsigned nrounds,
const unsigned nconflicts_per_round, const unsigned nvars,
const unsigned nclauses) const
{
std::cout << "Testing glucose conflict clause" << std::endl;
for (unsigned round = 0; round < nrounds; ++round)
{
auto sat_cnf = random_sat_cnf(nclauses, nvars);
for (unsigned confl_round = 0; confl_round < nconflicts_per_round;
++confl_round)
{
if (!TestConflict(sat_cnf.first,
random_literal_vector_with_size(nvars / 3, nvars)))
{
std::cout << "[FAILED]" << std::endl;
return false;
}
}
}
std::cout << "[OK]" << std::endl;
return true;
}
bool
SUBool::TestGlucose::TestIncrementalSimple() const
{
std::cout << "Testing glucose incremental capabilities on a simple CNF"
<< std::endl;
IncSolverWrapper wrap;
auto &g = wrap.Solver();
auto cnf = Dimacs::parse_cnf(dimacs);
std::cout << cnf << std::endl;
g.AddCnf(cnf);
PartialAssignment gamma(8);
gamma[2] = PartialValue::FALSE;
auto b = g.Solve(gamma);
std::cout << "Solving " << gamma << " with result " << (b ? "SAT" : "UNSAT")
<< std::endl;
gamma[1] = PartialValue::FALSE;
b = g.Solve(gamma);
std::cout << "Solving " << gamma << " with result " << (b ? "SAT" : "UNSAT")
<< std::endl;
std::cout << "[OK]" << std::endl;
return true;
}
bool
SUBool::TestGlucose::TestIncremental(const unsigned n_rounds,
const unsigned n_clauses, const unsigned n_vars,
const unsigned assump_length) const
{
std::cout << "Testing glucose incremental capabilities" << std::endl;
IncSolverWrapper wrap;
auto &g = wrap.Solver();
auto sat_cnf = random_sat_cnf(n_clauses, n_vars);
g.AddCnf(sat_cnf.first);
if (!g.Solve())
{
std::cout << "The CNF is declared UNSATISFIABLE [FAILED]" << std::endl;
}
for (unsigned round = 0; round < n_rounds; ++round)
{
auto assump = random_literal_vector_with_size(assump_length, n_vars);
std::cout << "Trying assumptions: " << VectorPrinter(assump) << std::endl;
auto b = g.Solve(assump);
std::cout << "Result: " << (b ? "SAT" : "UNSAT") << std::endl;
SimpSolverWrapper wrap2;
auto &g2 = wrap2.Solver();
g2.AddCnf(sat_cnf.first);
auto b2 = g2.Solve(assump);
std::cout << "Result 2: " << (b2 ? "SAT" : "UNSAT") << std::endl;
if (b != b2)
{
std::cout << "[FAILED] mismatch" << std::endl;
}
std::cout << g.LearntsSize() << std::endl;
}