listaArestas = list ( )
listaNodos = list ( )
listaClausulas = list ( )
def reducao( ) :
leitura( )
adicionaNodos( )
criaGadgets( )
def leitura( ) :
stringona = "x,y,!z"
stringona = string .split ( '#' )
for clau in stringona:
clausula = clausula.split ( ',' )
listaClausulas.append ( clausula)
def adicionaNodos( ) :
listaNodos.append ( "T" )
listaNodos.append ( "F" )
listaNodos.append ( "B" )
for clausula in listaClausulas:
for i in range ( 0 , len ( clausula) ) :
variavel = str ( clausula[ i] )
variavel = variavel.replace ( '!' , '' )
print ( variavel)
if variavel not in listaNodos:
listaNodos.append ( variavel)
listaNodos.append ( '!' +variavel)
listaArestas.append ( [ variavel, "!" + variavel] )
listaArestas.append ( [ variavel, "B" ] )
listaArestas.append ( [ "!" + variavel, "B" ] )
def criaGadgets( ) :
k = 0
for clausula in listaClausulas:
listaNodos.append ( "G" +str ( k) )
listaArestas.append ( [ clausula[ 0 ] , "G" +str ( k) ] )
if len ( clausula) > 1 :
listaNodos.append ( "G" +str ( k+1 ) )
listaNodos.append ( "G" +str ( k+2 ) )
listaArestas.append ( [ clausula[ 1 ] , "G" +str ( k+1 ) ] )
listaArestas.append ( [ "G" +str ( k) , "G" +str ( k+1 ) ] )
listaArestas.append ( [ "G" +str ( k) , "G" +str ( k+2 ) ] )
listaArestas.append ( [ "G" +str ( k+1 ) , "G" +str ( k+2 ) ] )
if len ( clausula) > 2 :
listaNodos.append ( "G" +str ( k+3 ) )
listaNodos.append ( "G" +str ( k+4 ) )
listaNodos.append ( "G" +str ( k+5 ) )
listaArestas.append ( [ clausula[ 2 ] , "G" +str ( k+4 ) ] )
listaArestas.append ( [ "G" +str ( k+2 ) , "G" +str ( k+3 ) ] )
listaArestas.append ( [ "G" +str ( k+3 ) , "G" +str ( k+4 ) ] )
listaArestas.append ( [ "G" +str ( k+3 ) , "G" +str ( k+5 ) ] )
listaArestas.append ( [ "G" +str ( k+4 ) , "G" +str ( k+5 ) ] )
listaArestas.append ( [ "G" +str ( k+5 ) , "B" ] )
listaArestas.append ( [ "G" +str ( k+5 ) , "F" ] )
k = k+1
print ( "Lista de Nodos" )
print ( listaNodos)
print ( '\n ' + "Lista de Arestas" )
print ( listaArestas)
reducao( )
bGlzdGFBcmVzdGFzID0gbGlzdCgpCmxpc3RhTm9kb3MgPSBsaXN0KCkKbGlzdGFDbGF1c3VsYXMgPSBsaXN0KCkKCmRlZiByZWR1Y2FvKCk6CiAgICBsZWl0dXJhKCkKICAgIGFkaWNpb25hTm9kb3MoKQogICAgY3JpYUdhZGdldHMoKQoKZGVmIGxlaXR1cmEoKToKCXN0cmluZ29uYSA9ICJ4LHksIXoiCglzdHJpbmdvbmEgPSBzdHJpbmcuc3BsaXQoJyMnKQogICAgZm9yIGNsYXUgaW4gc3RyaW5nb25hOgoJCWNsYXVzdWxhID0gY2xhdXN1bGEuc3BsaXQoJywnKQogICAgICAgIGxpc3RhQ2xhdXN1bGFzLmFwcGVuZChjbGF1c3VsYSkKCmRlZiBhZGljaW9uYU5vZG9zKCk6CiAgICBsaXN0YU5vZG9zLmFwcGVuZCgiVCIpCiAgICBsaXN0YU5vZG9zLmFwcGVuZCgiRiIpCiAgICBsaXN0YU5vZG9zLmFwcGVuZCgiQiIpCgogICAgZm9yIGNsYXVzdWxhIGluIGxpc3RhQ2xhdXN1bGFzOgogICAgICAgIGZvciBpIGluIHJhbmdlKDAsIGxlbihjbGF1c3VsYSkpOgogICAgICAgICAgICB2YXJpYXZlbCA9IHN0cihjbGF1c3VsYVtpXSkKICAgICAgICAgICAgdmFyaWF2ZWwgPSB2YXJpYXZlbC5yZXBsYWNlKCchJywnJykKICAgICAgICAgICAgcHJpbnQodmFyaWF2ZWwpCgogICAgICAgICAgICBpZiB2YXJpYXZlbCBub3QgaW4gbGlzdGFOb2RvczoKICAgICAgICAgICAgICAgIGxpc3RhTm9kb3MuYXBwZW5kKHZhcmlhdmVsKQogICAgICAgICAgICAgICAgbGlzdGFOb2Rvcy5hcHBlbmQoJyEnK3ZhcmlhdmVsKQogICAgICAgICAgICAgICAgbGlzdGFBcmVzdGFzLmFwcGVuZChbdmFyaWF2ZWwsIiEiICsgdmFyaWF2ZWxdKQogICAgICAgICAgICAgICAgbGlzdGFBcmVzdGFzLmFwcGVuZChbdmFyaWF2ZWwsIkIiXSkKICAgICAgICAgICAgICAgIGxpc3RhQXJlc3Rhcy5hcHBlbmQoWyIhIiArIHZhcmlhdmVsLCJCIl0pCgpkZWYgY3JpYUdhZGdldHMoKToKICAgIGsgPSAwCiAgICBmb3IgY2xhdXN1bGEgaW4gbGlzdGFDbGF1c3VsYXM6CiAgICAgICAgbGlzdGFOb2Rvcy5hcHBlbmQoIkciK3N0cihrKSkKICAgICAgICBsaXN0YUFyZXN0YXMuYXBwZW5kKFtjbGF1c3VsYVswXSwiRyIrc3RyKGspXSkKCiAgICAgICAgaWYgbGVuKGNsYXVzdWxhKSA+IDE6CiAgICAgICAgICAgIGxpc3RhTm9kb3MuYXBwZW5kKCJHIitzdHIoaysxKSkKICAgICAgICAgICAgbGlzdGFOb2Rvcy5hcHBlbmQoIkciK3N0cihrKzIpKQogICAgICAgICAgICBsaXN0YUFyZXN0YXMuYXBwZW5kKFtjbGF1c3VsYVsxXSwiRyIrc3RyKGsrMSldKQogICAgICAgICAgICBsaXN0YUFyZXN0YXMuYXBwZW5kKFsiRyIrc3RyKGspLCJHIitzdHIoaysxKV0pCiAgICAgICAgICAgIGxpc3RhQXJlc3Rhcy5hcHBlbmQoWyJHIitzdHIoayksIkciK3N0cihrKzIpXSkKICAgICAgICAgICAgbGlzdGFBcmVzdGFzLmFwcGVuZChbIkciK3N0cihrKzEpLCJHIitzdHIoaysyKV0pCgogICAgICAgIGlmIGxlbihjbGF1c3VsYSkgPiAyOgogICAgICAgICAgICBsaXN0YU5vZG9zLmFwcGVuZCgiRyIrc3RyKGsrMykpCiAgICAgICAgICAgIGxpc3RhTm9kb3MuYXBwZW5kKCJHIitzdHIoays0KSkKICAgICAgICAgICAgbGlzdGFOb2Rvcy5hcHBlbmQoIkciK3N0cihrKzUpKQogICAgICAgICAgICBsaXN0YUFyZXN0YXMuYXBwZW5kKFtjbGF1c3VsYVsyXSwiRyIrc3RyKGsrNCldKQogICAgICAgICAgICBsaXN0YUFyZXN0YXMuYXBwZW5kKFsiRyIrc3RyKGsrMiksIkciK3N0cihrKzMpXSkKICAgICAgICAgICAgbGlzdGFBcmVzdGFzLmFwcGVuZChbIkciK3N0cihrKzMpLCJHIitzdHIoays0KV0pCiAgICAgICAgICAgIGxpc3RhQXJlc3Rhcy5hcHBlbmQoWyJHIitzdHIoayszKSwiRyIrc3RyKGsrNSldKQogICAgICAgICAgICBsaXN0YUFyZXN0YXMuYXBwZW5kKFsiRyIrc3RyKGsrNCksIkciK3N0cihrKzUpXSkKICAgICAgICAgICAgbGlzdGFBcmVzdGFzLmFwcGVuZChbIkciK3N0cihrKzUpLCJCIl0pCiAgICAgICAgICAgIGxpc3RhQXJlc3Rhcy5hcHBlbmQoWyJHIitzdHIoays1KSwiRiJdKQogICAgICAgIGsgPSBrKzEKICAgIHByaW50KCJMaXN0YSBkZSBOb2RvcyIpCiAgICBwcmludChsaXN0YU5vZG9zKQogICAgcHJpbnQoJ1xuJyArICJMaXN0YSBkZSBBcmVzdGFzIikKICAgIHByaW50KGxpc3RhQXJlc3RhcykKCnJlZHVjYW8oKQ==