OKlibrary  0.2.1.6
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.

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.