You are not logged in. Please login at www.codechef.com to post your questions!

×

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

asked 07 May '14, 22:24

danielgarciaos's gravatar image

0★danielgarciaos
1111
accept rate: 0%

edited 07 May '14, 22:26

toggle preview
Preview

Follow this question

By Email:

Once you sign in you will be able to subscribe for any updates here

By RSS:

Answers

Answers and Comments

Markdown Basics

  • *italic* or _italic_
  • **bold** or __bold__
  • link:[text](http://url.com/ "title")
  • image?![alt text](/path/img.jpg "title")
  • numbered list: 1. Foo 2. Bar
  • to add a line break simply add two spaces to where you would like the new line to be.
  • basic HTML tags are also supported
  • mathemetical formulas in Latex between $ symbol

Question tags:

×1,818
×905
×242
×2
×1

question asked: 07 May '14, 22:24

question was seen: 1,715 times

last updated: 07 May '14, 22:26