A 2SAT solver, written in Rust. The 2SAT language is the set of 2CNFs
The generalized problem
An input formula is specified using ~
for logical negation, &
for logical AND, and |
for logical OR. Variables may be any alphanumeric string, not starting with a number. Then, the input must be specified as a 2CNF, where clauses (ORs) with 2 variables are enclosed in parentheses, and all clauses are conjoined by &
. &
must not appear within parentheses, only |
can. |
cannot appear outside parentheses. Parentheses may not be nested. Some valid formula strings:
"(a|b)&~c&(~a|~d)&(a|a)&c"
"(x1|x2)&(x3|~x4)"
Some invalid formula strings (they are not 2CNFs):
"a|b"
"(a&b)|(c&d)"
"(a|b|c)"
"a&(b|c)&((c|a)&d|e)"
Note that my parser removes all whitespace, so an input like "hello there & (a | hello there)"
(which is objectively terrible variable naming), is treated as "hellothere&(a|hellothere)"
where the two variables are a
and hellothere
.
Then, if your correctly specified formula is <phi>
, check if it's satisfiable with
$ cargo run <phi>
For example,
$ cargo run "(a|b)&(~a|d)&(b|c)&(~b|d)&(~b|e)&(~d|~c)&(~e|~d)"
Formula is not SAT
$ cargo run "(x1|x2) & (x1|~x3) & (~x1|~x2) & (x1|x4) & (~x1|~x5)"
Formula is SAT with assignment {"x4": true, "x3": false, "x1": false, "x2": true, "x5": false}
If you are curious enough to search through the git history of this repository
you will find that I initially implemented this 2SAT solver using the logical rule of resolution. However, it ran in