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