Skip to content

Instantly share code, notes, and snippets.

@allanlw
Last active June 23, 2020 02:38
Show Gist options
  • Save allanlw/69df509519335b88db886d48503a0f15 to your computer and use it in GitHub Desktop.
Save allanlw/69df509519335b88db886d48503a0f15 to your computer and use it in GitHub Desktop.
<?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";
?>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment