Universe::IUniverseSatSolver class
#include <IUniverseSatSolver.hpp>

Contents

The IUniverseSatSolver interface defines the contract for SAT solvers.

Base classes

class IUniverseSolver virtual

Derived classes

class IUniversePseudoBooleanSolver virtual
class UniverseJavaSatSolver virtual

Constructors, destructors, conversion operators

~IUniverseSatSolver() defaulted override

Public functions

void addClause(const std::vector<int>& literals) pure virtual
void addAllClauses(const std::vector<std::vector<int>>& clauses) virtual
auto solveDimacs(const std::vector<int>& assumptions) -> UniverseSolverResult virtual
auto solveBoolean(const std::vector<Universe::UniverseAssumption<bool>>& assumptions) -> Universe::UniverseSolverResult virtual

Function documentation

Universe::IUniverseSatSolver::~IUniverseSatSolver() override defaulted

Destroys this IUniverseSatSolver.

void Universe::IUniverseSatSolver::addClause(const std::vector<int>& literals) pure virtual

Parameters
literals The literals of the clause to add.
Exceptions
UniverseContradictionException If the clause to add is inconsistent.

Adds to this solver a clause from a set of literals. The literals are represented by non-zero integers such that opposite literals are represented by opposite values (following the classical DIMACS way of representing literals).

void Universe::IUniverseSatSolver::addAllClauses(const std::vector<std::vector<int>>& clauses) virtual

Parameters
clauses A vector of sets of literals in the DIMACS format.
Exceptions
UniverseContradictionException If one of the clauses to add is inconsistent.

Adds to this solver several clauses from a set of sets of literals. This is convenient to create in a single call all the clauses.

UniverseSolverResult Universe::IUniverseSatSolver::solveDimacs(const std::vector<int>& assumptions) virtual

Parameters
assumptions The assumptions to consider when solving (as a set of literals).
Returns The outcome of the search conducted by the solver.

Solves the problem associated to this solver.

Universe::UniverseSolverResult Universe::IUniverseSatSolver::solveBoolean(const std::vector<Universe::UniverseAssumption<bool>>& assumptions) virtual

Parameters
assumptions The assumptions to consider when solving.
Returns The outcome of the search conducted by the solver.

Solves the problem associated to this solver.