0votos

Una proposición satisfacible en C#

por josejuan hace 6 años

Puestos a hacer el bruto (este es un problema SAT), es mejor compilar la expresión, así cada test sólo consumirá unos ciclos de procesador.

Determinar la satisfacibilidad de una fórmula lógica.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
var v = t.Where(c => Char.IsLetter(c) && c == Char.ToLower(c)).Distinct().Select(c => c.ToString()); 
var x = string.Format( 
    "using __test; namespace A {{ public static class B {{ public static bool C(Bool {0}) {{ return {1}; }} }} }}", 
    String.Join(", Bool ", v), 
    t.Replace("NOT", "!").Replace("AND", "&&").Replace("OR", "||").Replace("<->", "+").Replace("->", "^")); 
var p = new System.CodeDom.Compiler.CompilerParameters(); 
p.GenerateInMemory = true; 
p.CompilerOptions = "/optimize"; 
p.ReferencedAssemblies.Add(typeof(Bool).Assembly.Location); 
var r = new Microsoft.CSharp.CSharpCodeProvider().CompileAssemblyFromSource(p, x); 
var f = r.CompiledAssembly.GetType("A.B").GetMethod("C"); 
var L = v.Count(); 
var s = Enumerable.Range(0, L).Select(b => 1 << b).ToArray(); 
var S = s.Select(b => new Bool(true)).ToArray(); 
var N = 1 << L; 
int n = -1; 
while( ++n < N ) { 
    for( var i = 0; i < s.Length; i++ ) 
        S [ i ] = ( s [ i ] & n ) != 0; 
    if( (bool) f.Invoke(null, (object []) S) ) { 
        Console.WriteLine("Solución: {0}", String.Join(", ", 
            v.Zip(S, ( c, b ) => string.Format("{0} = {1}", c, b ? 1 : 0)))); 
        break; 
Console.WriteLine("{0} es satisfacible.", n < N ? "Sí" : "No"); 
 
 
 
 
 
 
 
// la clase Bool es necesaria para wrapear los operadores 
public class Bool { 
    private bool x; 
    public Bool( bool y ) { x = y; } 
    public static implicit operator Bool( bool y ) { return new Bool(y); } 
    public static implicit operator bool( Bool x ) { return x.x; } 
    public static Bool operator ^( Bool a, Bool b ) { return !a.x || b.x; } 
    public static Bool operator +( Bool a, Bool b ) { return !( a.x || b.x ); } 
    public override string ToString() { return ( (bool) this ).ToString(); } 
5 comentarios
0votos

Escrito por jneira hace 6 años

ainnns la que hay que montar por no tener macros :-P
0votos

Escrito por josejuan hace 6 años

Tu solución no sólo es fea, previsible y aburrida, sino que no funciona.

Por otro lado, puesto que SAT no tiene solución eficiente, he preferido hacer una que se sale de lo típico (compilar al vuelo) y así tener una solución trivial (como todas las presentadas) pero con la menor constante multiplicativa (hombre, algún speedup adicional se puede hacer, claro).

Ala, ya te he picado, a ver como la mejoras XD XD XD
0votos

Escrito por jneira hace 6 años

jajaja, la tuya mas! la compilacion al vuelo es una forma de hacer metaprogramacion estatica interesante pero rudimentaria comparada con un sistema de macros de verdad (y no lo que tiene c).
No todas las soluciones son triviales, al menos a mi la de joseaalonso no me lo parece...
0votos

Escrito por josejuan hace 6 años

dado el problema planteado, compilar la expresión a código máquina es una opción muchísimo más indicada que las macros.

la solución de josealonso también es la trivial (revisar las 2^n asignaciones de variables posibles) y tiene soluciones mucho más brillantes que esa (que tampoco me gusta).

si tienes una solución ingeniosa que evite codificar la solución (verbosemente) me gustará, la tuya se acerca (lo de fea y aburrida era para picar XD) pero no se ciñe al enunciado (habrá que verla ciñéndose)

ahora si quieres puedes comparar el rendimiento de cada solución
0votos

Escrito por jneira hace 6 años

Mmm con trivial te referias a la parte que trata de identificar los valores de las variables que hacen satisfacible una proposicion concreta y yo hablaba de la parte que consiste en construir un interprete de logica proposicional general a cualquier proposicion. Me habia interesado mas esa parte (el interprete) y no su aplicacion aunque la verdad es que el enunciado trata de lo segundo.

Comenta la solución

Tienes que identificarte para poder publicar tu comentario.