OKlibrary  0.2.1.6
OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses > Class Template Reference

Transferring a (boolean) clause-set into a clause-list, and then performing unit-clause propagation. More...

#include <ClsAdaptorUCP.hpp>

List of all members.

Public Types

typedef Lit int_type
typedef std::string string_type
typedef Clauses value_type
typedef std::list< value_typeclause_set_type
typedef
clause_set_type::const_iterator 
const_iterator
typedef clause_set_type::iterator iterator
typedef clause_set_type::size_type size_type
typedef std::vector
< OKlib::Satisfiability::Values::Assignment_status
assignment_type
typedef std::vector< int_typepartial_assignment_type

Public Member Functions

 CLSAdaptorUcp ()
const_iterator begin () const
const_iterator end () const
size_type size () const
const string_typeorig_comment () const
string_type add_comment () const
const assignment_typeucp_total () const
const partial_assignment_typeucp_partial () const
void comment (const string_type &com_)
void n (const int_type n_)
void c (const int_type c_)
void tautological_clause (int_type) const
template<class Range >
void clause (const Range &clause, int_type)
void finish () const
bool empty_clause () const
OKlib::Satisfiability::Values::Sat_status perform_ucp ()

Detailed Description

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
class OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >

Transferring a (boolean) clause-set into a clause-list, and then performing unit-clause propagation.

Specification:

  • Models CLSAdaptor and basic ClauseList.
  • This is the basic linear-time algorithm, using the clause-literal graph and considering only falsified literals during the reduction process.
  • The reduction process is performed when calling perform_ucp() (after having completed the transfer).
  • The clause-list is usable thereafter iff the return-value is "open".
  • Additional comments reflecting the UCP-process are available via add_comment().

Assumptions:

  • Template-parameter Lit needs to be a (signed) integral type.
  • Template-parameter Clauses needs to fulfil concept "Clauses with removal".
Todo:
Complete container-functionality
  • Yet not all required members for a sequence are there.
Todo:
Write unit-tests.
Todo:
Improve implementation
  • Should we store the clause-list via a vector? Likely then data-locality is improved; on the other hand then the final removal of satisfied clauses becomes more complicated.
  • Likely using vectors instead of lists for the occurrence-lists (per literal) is faster: construction is slower, but then usage is faster.
Todo:
Use messages.
Todo:
Separate the transfer from the unit-clause propagation
  • Then for the UCP general (boolean) literals can be used.
Todo:
Harmonise with KLevelForcedAssignments::CLSAdaptorKUcp

Definition at line 98 of file ClsAdaptorUCP.hpp.


Member Typedef Documentation

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef std::vector<OKlib::Satisfiability::Values::Assignment_status> OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::assignment_type

Definition at line 109 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef std::list<value_type> OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::clause_set_type

Definition at line 104 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef clause_set_type::const_iterator OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::const_iterator

Definition at line 105 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef Lit OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::int_type

Definition at line 100 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef clause_set_type::iterator OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::iterator

Definition at line 106 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef std::vector<int_type> OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::partial_assignment_type

Definition at line 110 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef clause_set_type::size_type OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::size_type

Definition at line 107 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef std::string OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::string_type

Definition at line 101 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
typedef Clauses OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::value_type

Definition at line 103 of file ClsAdaptorUCP.hpp.


Constructor & Destructor Documentation

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::CLSAdaptorUcp ( ) [inline]

Definition at line 112 of file ClsAdaptorUCP.hpp.


Member Function Documentation

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
string_type OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::add_comment ( ) const [inline]
template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::c ( const int_type  c_) [inline]

Definition at line 132 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
template<class Range >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::clause ( const Range &  clause,
int_type   
) [inline]
template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::comment ( const string_type com_) [inline]

Definition at line 122 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
bool OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::empty_clause ( ) const [inline]

Definition at line 157 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::finish ( ) const [inline]

Definition at line 156 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::n ( const int_type  n_) [inline]

Definition at line 127 of file ClsAdaptorUCP.hpp.

References OKlib::Satisfiability::Values::unassigned.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
const string_type& OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::orig_comment ( ) const [inline]
template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
size_type OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::size ( ) const [inline]
template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::tautological_clause ( int_type  ) const [inline]

Definition at line 135 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
const partial_assignment_type& OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::ucp_partial ( ) const [inline]

Definition at line 120 of file ClsAdaptorUCP.hpp.

template<typename Lit = OKlib::Literals::Literals_int, class Clauses = OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors<Lit>>
const assignment_type& OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >::ucp_total ( ) const [inline]

Definition at line 119 of file ClsAdaptorUCP.hpp.


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