وقد رأى أي شخص تنفيذ 2-SAT
-
20-09-2019 - |
سؤال
لقد كنت أبحث عن بعض الوقت، لكنني لا أستطيع أن أجد أي تنفيذ خوارزمية 2 السبت.
أنا أعمل في C ++ مع مكتبة دفعة (التي لديها وحدة مكون متصلة بقوة) بحاجة إلى بعض الإرشادات لإنشاء برنامج فعال 2-SAT أو العثور على مكتبة موجودة بالنسبة لي للاستفادة من خلال C ++.
المحلول
أفترض أنك تعرف كيفية طراز مشكلة 2-SAT لحلها مع SCC. الطريقة التي تعامل معها التي تتعامل معها ونفيها ليست أنيقة للغاية، ولكنها تسمح بتنفيذ قصير: إعطاء متغيرات N مرقمة من 0 إلى N-1، في Clauses - يعني نفي المتغير الأول، وفي الرسم البياني I + N يعني نفس الشيء (هل أنا واضح؟)
#include <boost/config.hpp>
#include <iostream>
#include <vector>
#include <boost/graph/strong_components.hpp>
#include <boost/graph/adjacency_list.hpp>
#include <boost/foreach.hpp>
typedef std::pair<int, int> clause;
//Properties of our graph. By default oriented graph
typedef boost::adjacency_list<> Graph;
const int nb_vars = 5;
int var_to_node(int var)
{
if(var < 0)
return (-var + nb_vars);
else
return var;
}
int main(int argc, char ** argv)
{
std::vector<clause> clauses;
clauses.push_back(clause(1,2));
clauses.push_back(clause(2,-4));
clauses.push_back(clause(1,4));
clauses.push_back(clause(1,3));
clauses.push_back(clause(-2,4));
//Creates a graph with twice as many nodes as variables
Graph g(nb_vars * 2);
//Let's add all the edges
BOOST_FOREACH(clause c, clauses)
{
int v1 = c.first;
int v2 = c.second;
boost::add_edge(
var_to_node(-v1),
var_to_node(v2),
g);
boost::add_edge(
var_to_node(-v2),
var_to_node(v1),
g);
}
// Every node will belong to a strongly connected component
std::vector<int> component(num_vertices(g));
std::cout << strong_components(g, &component[0]) << std::endl;
// Let's check if there is variable having it's negation
// in the same SCC
bool satisfied = true;
for(int i=0; i<nb_vars; i++)
{
if(component[i] == component[i+nb_vars])
satisfied = false;
}
if(satisfied)
std::cout << "Satisfied!" << std::endl;
else
std::cout << "Not satisfied!" << std::endl;
}
لا تنتمي إلى StackOverflow