Simple SAT Solver
Introduciton
This is simple SAT solver for tiny problems, up to 10-15 variables.
I tried to make this solver AST-agnostic, so input for solver is a program containing AND, OR and NOT instructions. Please refer to test/test.cpp and test/demo.cpp how to prepare data.
Sample session with test/demo:
# expression are given in prefix notation $ ./demo "and A not A" raw expression: and A not A parsed: (A) and (not (A)) result: unsatisfiable $ ./demo "or A not A" raw expression: or A not A parsed: (A) or (not (A)) result: tautology $ ./demo "and or A B A" raw expression: and or A B A parsed: ((A) or (B)) and (A) result: satisfiable $ ./demo "and and or A B A not B" raw expression: and and or A B A not B parsed: (((A) or (B)) and (A)) and (not (B)) result: satisfiable
License
Public domain