/usr/include/opengm/inference/sat.hxx is in libopengm-dev 2.3.6+20160905-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 | #pragma once
#ifndef OPENGM_INFERENCE_SAT_HXX
#define OPENGM_INFERENCE_SAT_HXX
#include <iostream>
#include <vector>
#include <boost/config.hpp>
#include <boost/graph/strong_components.hpp>
#include <boost/graph/adjacency_list.hpp>
#include <boost/foreach.hpp>
#include "opengm/inference/inference.hxx"
#include "opengm/operations/and.hxx"
#include "opengm/operations/or.hxx"
#include "opengm/inference/visitors/visitors.hxx"
namespace opengm {
/// 2-SAT solver
///
/// \ingroup inference
template<class GM>
class SAT : Inference<GM, opengm::Or> {
public:
typedef opengm::Or AccumulationType;
typedef GM GraphicalModelType;
OPENGM_GM_TYPE_TYPEDEFS;
template<class _GM>
struct RebindGm{
typedef SAT<_GM> type;
};
template<class _GM,class _ACC>
struct RebindGmAndAcc{
typedef SAT<_GM> type;
};
struct Parameter{
Parameter ( ) {};
template<class P>
Parameter (const P & p) {};
};
SAT(const GraphicalModelType&, const Parameter& = Parameter());
std::string name() const;
const GraphicalModelType& graphicalModel() const;
InferenceTermination infer();
template<class VISITOR>
InferenceTermination infer(VISITOR &);
virtual void reset();
ValueType value() const;
typedef visitors::VerboseVisitor<SAT<GM> > VerboseVisitorType;
typedef visitors::TimingVisitor<SAT<GM> > TimingVisitorType;
typedef visitors::EmptyVisitor<SAT<GM> > EmptyVisitorType;
private:
const GraphicalModelType& gm_;
std::vector<int> component_;
};
template<class GM>
inline SAT<GM>::SAT
(
const GraphicalModelType& gm,
const Parameter& para
)
: gm_(gm)
{
if(!NO_DEBUG) {
OPENGM_ASSERT(gm_.factorOrder() <= 2);
OPENGM_ASSERT(typeid(OperatorType) == typeid(opengm::And));
for(size_t i=0; i<gm_.numberOfVariables();++i) {
OPENGM_ASSERT(gm_.numberOfLabels(i) == 2);
}
}
}
template<class GM>
void
inline SAT<GM>::reset()
{
}
template<class GM>
inline std::string
SAT<GM>::name() const
{
return "2Sat";
}
template<class GM>
inline const GM&
SAT<GM>::graphicalModel() const
{
return gm_;
}
template<class GM>
InferenceTermination
SAT<GM>::infer() {
EmptyVisitorType v;
return infer(v);
}
template<class GM>
template<class VISITOR>
InferenceTermination
SAT<GM>::infer
(
VISITOR & visitor
) {
visitor.begin(*this);
typedef std::pair<int, int> clause;
typedef boost::adjacency_list<> Graph; // properties of our graph. by default: oriented graph
// build graph
Graph g(gm_.numberOfVariables() * 2);
for(size_t f=0; f<gm_.numberOfFactors(); ++f) {
if(gm_[f].numberOfVariables() != 2) {
throw RuntimeError("This implementation of the 2-SAT solver supports only factors of order 2.");
}
std::vector<size_t> vec(2);
for(vec[0]=0; vec[0]<2; ++vec[0]) {
for(vec[1]=0; vec[1]<2; ++vec[1]) {
if(!gm_[f](vec.begin())) {
const int v1=gm_[f].variableIndex(0)+(1-vec[0])*gm_.numberOfVariables();
const int nv1=gm_[f].variableIndex(0)+(0+vec[0])*gm_.numberOfVariables();
const int v2=gm_[f].variableIndex(1)+(1-vec[1])*gm_.numberOfVariables();
const int nv2=gm_[f].variableIndex(1)+(0+vec[1])*gm_.numberOfVariables();
boost::add_edge(nv1,v2,g);
boost::add_edge(nv2,v1,g);
}
}
}
}
component_.resize(num_vertices(g));
strong_components(g, make_iterator_property_map(component_.begin(), get(boost::vertex_index, g)));
visitor.end(*this);
return NORMAL;
}
template<class GM>
inline typename GM::ValueType
SAT<GM>::value() const
{
bool satisfied = true;
for(IndexType i=0; i<gm_.numberOfVariables(); i++) {
if(component_[i] == component_[i+gm_.numberOfVariables()]) {
satisfied = false;
}
}
return satisfied;
}
} // namespace opengm
#endif // #ifndef OPENGM_INFERENCE_SAT_HXX
|