OKlibrary  0.2.1.6
OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment > Class Template Reference

Transferring a (boolean) clause-set into a clause-list, and then performing UCP using watched literals. More...

#include <ClsAdaptorUCP.hpp>

Inheritance diagram for OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >:
OKlib::Satisfiability::Reductions::KLevelForcedAssignments::CLSAdaptorKUcp< WatchedClauses, Assignment >

List of all members.

Public Types

typedef Assignment assignment_type
typedef std::string string_type
typedef literal_type int_type

Public Member Functions

 CLSAdaptorUcpW ()
const string_typeorig_comment () const
string_type add_comment () const
const assignment_typeassignment () 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)
 Remarks on the implementation:
void finish ()
bool empty_clause () const
bool contradicting_uclause () const
 returns true if contradicting unit-clauses were found
bool & contradicting_uclause ()
bool push_unit_clause (const literal_type x)
 returns false if assignment not successful due to opposite value already present; has the same effect as if unit-clause {x} would be added
void clear_assignments ()
 needs to take care of contradicting_uclause()
void set_assignments (const assignment_type &fnew)
 needs to take care of contradicting_uclause()
template<class CLSAdaptor >
void output (CLSAdaptor &A)
 output to cls-adaptor (adding a comment in case a contradiction was found)
bool perform_ucp ()
 returns true iff a contradiction was found, and computes the forced assignments

Detailed Description

template<class WatchedClauses, class Assignment>
class OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >

Transferring a (boolean) clause-set into a clause-list, and then performing UCP using watched literals.

Functionality:

  • An object U of type CLSAdaptorUcpW is constructed via the default constructor.
  • U then is to be used as a CLSAdaptor (see specification in OKlib/Satisfiability/Interfaces/InputOutput/ClauseSetAdaptors.hpp), to read in a clause-set.
  • No standardisation on variables is performed, and so it is recommended that this is done before transfer.
  • The original comment is available via U.orig_comment().
  • Then via U.perform_ucp() unit-clause propagation is performed; the return value is true iff a contradiction was found.
  • Via U.add_comment() the additional comment, added after performing UCP, is returned.
  • Via U.output(A) the clause-set can be transferred to another CLS-adaptor A (before and/or after performing UCP).
  • Via U.assignment() a constant reference to the assignment computed is returned.

On the algorithm:

  • Binary clauses are handled on their own (for them we just use clause-literal graphs).
  • The order of the assignments for propagation is given by the Assignment-class.

Requirements:

  • the literal type is a signed integral type
Todo:
Complete specification
Todo:
Complete implementation
Todo:
Write unit-tests
Todo:
Harmonise with UnitClausePropagation::CLSAdaptorUcp
  • See above.

Definition at line 309 of file ClsAdaptorUCP.hpp.


Member Typedef Documentation

template<class WatchedClauses , class Assignment >
typedef Assignment OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::assignment_type

Definition at line 310 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
typedef literal_type OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::int_type

Definition at line 337 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
typedef std::string OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::string_type

Definition at line 311 of file ClsAdaptorUCP.hpp.


Constructor & Destructor Documentation

template<class WatchedClauses , class Assignment >
OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::CLSAdaptorUcpW ( ) [inline]

Definition at line 330 of file ClsAdaptorUCP.hpp.


Member Function Documentation

template<class WatchedClauses , class Assignment >
string_type OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::add_comment ( ) const [inline]

Definition at line 333 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
const assignment_type& OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::assignment ( ) const [inline]

Definition at line 334 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::c ( const int_type  c_) [inline]

Definition at line 349 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
template<class Range >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::clause ( const Range &  clause,
int_type   
) [inline]

Remarks on the implementation:

  • returns immediately when an empty clause was found,
  • unit-clauses are transferred into the assignment f,
  • binary clauses are transferred to F2,
  • all other clauses are transferred to F and watched via FW.

Definition at line 362 of file ClsAdaptorUCP.hpp.

References s.

template<class WatchedClauses , class Assignment >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::clear_assignments ( ) [inline]

needs to take care of contradicting_uclause()

Definition at line 409 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::comment ( const string_type com_) [inline]

Definition at line 338 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
bool OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::contradicting_uclause ( ) const [inline]

returns true if contradicting unit-clauses were found

Definition at line 394 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
bool& OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::contradicting_uclause ( ) [inline]

Definition at line 395 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
bool OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::empty_clause ( ) const [inline]

Definition at line 391 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::finish ( ) [inline]
template<class WatchedClauses , class Assignment >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::n ( const int_type  n_) [inline]

Definition at line 342 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
const string_type& OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::orig_comment ( ) const [inline]

Definition at line 332 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
bool OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::push_unit_clause ( const literal_type  x) [inline]

returns false if assignment not successful due to opposite value already present; has the same effect as if unit-clause {x} would be added

Definition at line 402 of file ClsAdaptorUCP.hpp.

References CgiHandling::success, and OKlib::Literals::var().

template<class WatchedClauses , class Assignment >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::set_assignments ( const assignment_type fnew) [inline]

needs to take care of contradicting_uclause()

Definition at line 411 of file ClsAdaptorUCP.hpp.

template<class WatchedClauses , class Assignment >
void OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >::tautological_clause ( int_type  ) const [inline]

Definition at line 353 of file ClsAdaptorUCP.hpp.


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