PHP re-implementation of https://yurichev.com/news/20200621_regex_SAT/

solver.php

<?php

// simple PHP re-implementation of https://yurichev.com/news/20200621_regex_SAT/
// to take advantage of PCRE jit

ini_set('pcre.backtrack_limit',  (1<<63) - 1);
ini_set('pcre.jit', 1);

function read_text_file($fname) {
  return array_map('trim', explode("\n", file_get_contents($fname)));
}

function read_DIMACS($fname) {
    $content = read_text_file($fname);

    $header = explode(" ", $content[0]);

    assert($header[0] === "p" && $header[1] === "cnf");

    $variables_total = (int)$header[2];
    $clauses_total = (int)$header[3];

    // term can be negative signed integer
    $clauses = array();
    foreach (array_slice($content, 1) as $c) {
        if (strpos($c, "c ") === 0) continue;
        $clause = array();
        foreach (explode(" ", $c) as $var_s) {
            if (strlen($var_s) === 0) continue;
            $v = (int)$var_s;
            if ($v !== 0) $clause[] = $v;
        }
        if (count($clause) > 0)
            $clauses[] = $clause;
    }

    return array($variables_total, $clauses_total, $clauses);
}

list($variables_total, $clauses_total, $clauses) = read_DIMACS($argv[1]);

$s = str_repeat("x", $variables_total) . ";" . str_repeat("x,", $clauses_total);
echo "string=", $s, "\n";
$pat = "^";
for ($i = 0; $i < $variables_total; $i++) {
    $pat .= "(?P<a_" . ($i+1) . ">x?)";
}
$pat .= ".*;";

function term_to_regex($term) {
    if ($term < 0) {
        return "(?P=a_" . abs($term) . ")x";
    } else {
        return "(?P=a_" . $term . ")";
    }
}

foreach ($clauses as $clause) {
    $pat .= "(?:";
    $pat .= implode("|", array_map('term_to_regex', $clause));
    $pat .= '),';
}

echo "pattern=", $pat, "\n";

$res = preg_match("/$pat/", $s, $matches);
if ($res === 0) {
    echo "UNSAT\n";
    exit(0);
} else if ($res === FALSE) {
    echo "ERROR: ", preg_last_error(), "\n";
    exit(1);
}

echo "SAT\n";
$out = "";
for ($i = 0; $i < $variables_total; $i++) {
    $result = $matches[$i+1];
    $out .= ($result === 'x' ? '' : '-') . ($i+1) . " ";
}

echo $out, "\n";

?>