sat::Solver Class Reference

Main solver class. More...

#include <Solver.hpp>

Public Member Functions
	Solver (unsigned numVariables)
bool	addClause (Clause clause)
auto	rebase () const -> std::vector< Clause >
TruthValue	val (Variable x) const
bool	satisfied (Literal l) const
bool	falsified (Literal l) const
bool	assign (Literal l)
bool	unitPropagate ()

Detailed Description

Main solver class.

Constructor & Destructor Documentation

Solver()

sat::Solver::Solver ( unsigned  numVariables )

explicit

Ctor. Allocates enough space for the variables.

Parameters

numVariables

Number of variables in the problem

Note

This Ctor needs to exist for the tests. You can add other Ctors if you want

Member Function Documentation

addClause()

bool sat::Solver::addClause

(

Clause

clause

)

Adds a clause to the solver.

Parameters

clause

The clause to add

Returns

bool true if clause was successfully added, false if clause is empty or unit and violates the current model

assign()

bool sat::Solver::assign

(

Literal

l

)

Assigns the given literal

Parameters

l	Literal to assign

Returns

false if literal is already falsified, true otherwise

falsified()

bool sat::Solver::falsified

(

Literal

l

)

const

Checks if a literal does not hold

Parameters

l	literal (needs ti be contained in the solver)

Returns

true if literal the negated literal is satisfied, false otherwise

rebase()

auto sat::Solver::rebase

(

)

const -> std::vector<Clause>

Returns a reduced set of clauses. Excludes satisfied clauses and removes falsified literals from clauses

Returns

equivalent set of clauses

Here you have a possible implementation of the rebase-method. It should work out of the box. To use it, remove the throw-expression and un-comment the code below. The implementation requires that your solver has some sort of container of pointer types to clause called 'clauses' (e.g. std::vector<ClausePointer>). Additionally, your solver needs to have a container of unit literals called 'unitLiterals'.

satisfied()

bool sat::Solver::satisfied

(

Literal

l

)

const

Checks if a literal holds

Parameters

l	literal (needs ti be contained in the solver)

Returns

true if literal holds under current model, false otherwise

unitPropagate()

bool sat::Solver::unitPropagate

(

)

Does the unit propagation.

Returns

true if unit propagation was successful, false otherwise

val()

TruthValue sat::Solver::val

(

Variable

x

)

const

Returns the truth value of the given variable

Parameters

x	a variable (needs to be contained in the solver)

Returns

TruthValue of the given variable

---

The documentation for this class was generated from the following files:

• Solver/Solver.hpp
• Solver/Solver.cpp