UnitPropagation Namespace Reference

Functions
template<class Cls >
Auxiliary::Sat_status	unit_propagation_simple (Cls &F)
	Generic function for UCP, applying just iterated linear search for unit-clauses.
template<class Cls >
Auxiliary::Sat_status	unit_propagation_improved (const Cls &F, typename Cls::Pass &phi)
	Generic implementation of the basic linear-time algorithm for UCP.

---

Function Documentation

template<class Cls >

Auxiliary::Sat_status UnitPropagation::unit_propagation_improved	(	const Cls &	F,
		typename Cls::Pass &	phi
	)

Generic implementation of the basic linear-time algorithm for UCP.

Todo:

Make the underlying concepts explicit

• For a literal x, [x.begin,x.end()] is the range of all clauses in which x occurs.

Definition at line 66 of file UnitPropagation.hpp.

References s, Auxiliary::satisfied, Auxiliary::undefined, OKlib::SATCompetition::unknown, and Auxiliary::unsatisfiable.

template<class Cls >

Auxiliary::Sat_status UnitPropagation::unit_propagation_simple

(

Cls &

F

)

Generic function for UCP, applying just iterated linear search for unit-clauses.

Todo:

Make the concept for Cls explicit

• F.unsat() should just check for the empty clause.
• F.sat() should just check for the empty clause-set.
• F.apply(phi) applies the partial assignment in-place.

Definition at line 39 of file UnitPropagation.hpp.

References Auxiliary::satisfiable, satisfiable, Auxiliary::unknown, and Auxiliary::unsatisfiable.