#!/bin/bash
# Pasa fórmulas 3-SAT al azar por minisat, con cerca de 4,26 cláusulas por variable. Se corre con `make solver`,
# dentro del entorno del curso. Los tiempos son los que reporta minisat, y dependen de la máquina.
set -u
mkdir -p build/solver
printf '%10s %10s %8s %16s %12s\n' variables cláusulas semilla resultado segundos
for n in 100 150 200 250 300; do
    m=$((n * 426 / 100))
    for seed in 1 2 3; do
        cnf=build/solver/f.cnf
        build/random_3sat "$n" "$m" "$seed" > "$cnf"
        log=$(timeout 30 minisat "$cnf" build/solver/f.out 2>&1)
        code=$?
        case "$code" in
            10) result=satisfacible ;;
            20) result=insatisfacible ;;
            124) result="más de 30 s" ;;
            *) result="código $code" ;;
        esac
        cpu=$(printf '%s\n' "$log" | grep 'CPU time' | sed 's/.*: *//; s/ s$//')
        printf '%10s %10s %8s %16s %12s\n' "$n" "$m" "$seed" "$result" "${cpu:--}"
    done
done

echo
echo "El principio del palomar: una paloma más que huecos."
printf '%10s %10s %10s %16s %12s\n' huecos variables cláusulas resultado segundos
for holes in 7 8 9 10; do
    cnf=build/solver/p.cnf
    build/pigeonhole "$holes" > "$cnf"
    header=$(head -n 1 "$cnf")
    log=$(timeout 30 minisat "$cnf" build/solver/p.out 2>&1)
    code=$?
    case "$code" in
        10) result=satisfacible ;;
        20) result=insatisfacible ;;
        124) result="más de 30 s" ;;
        *) result="código $code" ;;
    esac
    cpu=$(printf '%s\n' "$log" | grep 'CPU time' | sed 's/.*: *//; s/ s$//')
    printf '%10s %10s %10s %16s %12s\n' "$holes" "$(echo "$header" | cut -d' ' -f3)" "$(echo "$header" | cut -d' ' -f4)" "$result" "${cpu:--}"
done