solve_sat
Determine if a boolean expression is satisfiable by converting it to CNF and using DPLL to find a satisfying assignment or prove UNSAT.
Instructions
DPLL SAT solver for boolean satisfiability. Converts expression to Conjunctive Normal Form (CNF) and finds satisfying assignments or proves UNSAT.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| expression | Yes | The boolean expression to solve (e.g., "(A || B) && (!A || B) && (!B)") |