sat-solver/verify_solution.cpp

105 lines
1.9 KiB
C++

#include <assert.h>
#include <print.hpp>
#include "verify_solution.hpp"
static bool evaluate(
int* input,
const struct problem* p)
{
for (const auto clause: p->clauses)
{
for (const auto bundle: clause->bundles)
{
if (input[bundle.variable - 1] == bundle.value)
{
goto next_clause;
}
}
return false;
next_clause: ;
}
return true;
}
static void brute_force(
int* solution,
unsigned i, unsigned n,
const struct problem* p,
bool expecting)
{
if (i == n)
{
if (evaluate(solution, p) != expecting)
{
puts("verification failed! :(");
abort();
}
}
else for (int val = 0; val < 2; val++)
{
solution[i] = val;
brute_force(solution, i + 1, n, p, expecting);
}
}
void verify_solution(
refcounted<problem> problem,
refcounted<solution> solution)
{
switch (solution->kind)
{
case solution::all:
{
unsigned n = problem->number_of_variables;
int* solution = new int[n]();
brute_force(solution, 0, n, problem.get(), true);
delete[] solution;
break;
}
case solution::none:
{
unsigned n = problem->number_of_variables;
int* solution = new int[n]();
brute_force(solution, 0, n, problem.get(), false);
delete[] solution;
break;
}
case solution::specific:
{
if (!evaluate(solution->input, problem.get()))
{
puts("verification failed! :(");
abort();
}
break;
}
}
puts("verified.");
}