sat-solver/find_solutions.cpp
2025-03-07 09:45:39 -06:00

106 lines
2.2 KiB
C++

#include <assert.h>
#include <stdio.h>
#include <automata.hpp>
#include "find_solutions.hpp"
static bool is_empty_solution_space(
unsigned number_of_variables,
const struct automata* start)
{
const struct automata* moving = start;
while (moving && number_of_variables--)
{
moving = moving->on[0] ?: moving->on[1];
}
return !moving || !moving->is_accepting;
}
void find_solutions(
unsigned number_of_variables,
const struct automata* start)
{
bool found_solution = false;
// there are three cases:
// 1. solutions for no inputs
// 2. solutions for all inputs
// 3. solutions for some inputs
// consider case 1: (solutions for no inputs)
if (!found_solution)
{
if (is_empty_solution_space(number_of_variables, start))
{
puts("no solutions.");
found_solution = true;
}
}
// consider case 2: (solutions for all inputs)
if (!found_solution)
{
// to do this, we'll dis-prove the opposite: that the complement of the
// solution space is empty.
struct automata* complement = automata::complement(start);
if (is_empty_solution_space(number_of_variables, complement))
{
puts("all solutions.");
found_solution = true;
}
automata::free(complement);
}
// consider case 3: (solutions for some inputs)
if (!found_solution)
{
int solution[number_of_variables];
const struct automata* moving = start;
for (unsigned i = 0; i < number_of_variables; i++)
{
if (moving->on[0])
{
solution[i] = 0, moving = moving->on[0];
}
else
{
solution[i] = 1, moving = moving->on[1];
}
}
assert(moving && moving->is_accepting);
for (unsigned i = 0; i < number_of_variables; i++)
{
printf("variable %u = %i\n", i + 1, solution[i]);
}
found_solution = true;
}
}