Two Sat Problem

Two Sat

In this problem we must solve the satisfiability of logical formulas which consist of two propositions, without denying or denied joined by OR. There are also several of these formulas, consider the following example:

p1∨p3

p2∨¬p1

p2∨¬p3

¬p1∨¬p2

Note that if p1 is false, and p2, p3 are true, you can meet all the above. I mean, what you should do is to find a truth value for all propositions such that all formulas appraise real. It is not always possible to find a truth value to propositions that achieves satisfying all formulas, consider the following example:

p1∨¬p2

p1∨p2

¬p1∨¬p2

¬p1∨p2

Any possible combination of truth values ​​for the above propositions can not meet all the rules. The goal here is to make a program that given a set of propositions and rules to determine whether or not it is possible to meet all the rules, and if possible, to say truth values ​​satisfy all the rules.

Input:
The input consists of several test cases. The first line of each test case contains two integers N and M represent the number of rules and propositions respectively. Then follow N lines with two integers representing a rule, if the integer is positive represetenta the id of the proposition and if negative represents the negated proposition. In the example shown as the first two test cases the examples described above.

1 ≤ N ≤ 10000
1 ≤ M ≤ 5000

output:
For each test case print “Yes” or “No” without quotes. If the answer is “Yes” next to this should put an integer indicating the number of true propositions V, and on the next line V integer indicating the number of the true proposition.

example:

Input:
4 3

+1 +3

+2 -1

+2 -3

-1 -2

4 2

+1 -2

+1 +2

-1 -2

-1 +2

1 3

+1 -3

Output:

Yes 2

2 3

No

Yes 3

1 2 3

This is the code I made in C++ but I need a new logical solution… Thanks for your help.

``````#include<iostream>                   // Entradas y salidas cout y cin
#include<vector>                     //  representacion  nodos y el vector  listas  adyacencia
#include<list>                       //  insertar y borrar elementos en un punto especifico  la lista
#include<algorithm>                  // Implementa Sort,  no tener  implementar nuestro propio sort

using namespace std;                 //  utilizar todo lo  esta dentro del estandar  C++ y no tener  usar std::, aparte  saber diferenciar y saber a  me estoy refiriendo

struct Nodo{                         // Reordena los nodos por el tiempo  finalizacion y me muestra cual es el nodo  originalmente estaba en la posicion
int id;
int d;                           // Tiempo  Inicializacion
int f;                           // Tiempo  finalizacion
char color;                      // Color
Nodo *pi;                        // Pi(papa)
};

Void printNodo() {             //  precisar  entrega bien la respuesta
Cout<<"id"<<id<<endl;
Cout<<"tiempo_ini: "<<d<<endl;
Cout<<"tiempo_fin: "<<f<<endl;

class Grafo{                         // Clase  grafo
public:                              // Metodo publico
vector<Nodo>v;                   // Vector  nodos
vector<list<int>> al;            // Vector  lista  adyacencia (Vector donde  cada nodo se tiene una lista)
};

Grafo(){}                            // Constructor
/*
int getIndice(int id){
for(int=0;i<v.size();i++){
if(v[i].id==id)return i;
}
return -1;
}
*/
Grafo(int n){                         // Constructor
for(int i=0; i<n; i++){
Nodo n;
n.id=i;
v.push_back(n);
al.push_back(list<int n>());
}
}

void addArista(int u,int v){         // Adiciona una arista a la lista  adyacencia

}

Void printAl() {                     //  poder verificar  el grafo quedo bien construido
For (int i=0; i<v.size();i++){
Cout <<"nodo"<<v[i].id<< ":";
For (int j : al[i]){
Cout <<j<<" ";
}
Cout<<endl;
}
}

Void dfvisit(int u) {                 // El usuario me da un orden  recorrer los nodos y se recorren en ese orden
Time++;
U.d=time;
U.color= 'g';
For(int vi : al[u]) {
If (v[vi].color== 'w') {
V[vi].Pi=&v[u];
Dfsvisit(vi);
}
}
V[u].color ='b'
Time++;
V[u].f=time;
V[u].sccid=sccid;
}

Void dfs() {                         // El usuario no tiene un orden en particular y se da un orden por defecto
For (nodo &u : v) {
U.color= 'w';
U.pi=nullptr;
}
Time=0;
Sccid=0;
For (nodo &u : v) {
If(u.color == 'w')
Dfsvisit(u.id);
}
}
Grafo transpuesta() {               // Crea la transpuesta  un grafo
Grafo g(v.size());
For (int origen=0; origen<v.size(); origen++){
For (int destino :al[origen]){
G.addArista(destino,origen);
}
}
Retun g;
}
};

Void testAl(grafo &g){             // Prueba  funcione bien la lista  adyacencia
Cout <<"grafo original: "<< endl;
G.printAl();
Grafo t=g.transpuesta();
Cout<<"\ngrafo transpuesto: \n";
T.printAl();
}

Void testDFS(grafo &g){           // Prueba  funcione bien el dfs
G.dfs();
Cout <<endl;
For (nodo &u : g.v) {
U.printNodo();
Cout <<endl;
}
}

Bool compareNodo(const Nodo &a,const Nodo &b){ //  implementacion, compara nodo con el sort del lenguaje siguiendo el criterio  ordenamiento dado
Return a.f >b.f;
}

Void scc(grafo &g) {                // Me dice  componente es fuertemente conectado
Grafo gt = g.transpuesta();
Gt.dfs();
Vector<Nodo>nodos=g.v;
Sort(nodos.begin(),nodos

Int main() {
Int n,e,u,v;
Clin >> n >> e;
Grafo g(n);
For (int i=0; i<e; i++) {
Clin >>u>>v;
G.addArista(u,v);
}
G.printAl``````