This application solves boolean satisfiability (SAT) instances. Each line represents a clause, where clauses are separated by AND. Each number represents a literal, which are separated by OR. Negative numbers represent NOT. By combining these clauses, the solver determines if there is a possible assignment of variables that satisfies all clauses.
|
1 2 3 4 5
-1 -2 -3 -4 -5
1 -2
3 -4 5
5
-1 2
|