Documentation

Using the Solver

1. Enter your boolean formula in the input field
2. Use the buttons or type operators directly
3. Click "Solve SAT" to get the result
4. View the assignment or error message

Syntax Rules

• Variables: lowercase letters, underscores, and numbers (e.g., a1, var_2)
• Operators: & (AND), | (OR), ~ (NOT), -> (IMPLY), <-> (EQUIV)
• Constants: T (True), F (False)
• Parentheses for grouping expressions

REST API Endpoint

POST /marina
Content-Type: application/json

{
  "prop": "(a & b) -> c"
}

Response:
{
  "assignment": "(a,true) (b,true) (c,true)",
  "error": null
}

Error Responses

• 400: Bad request (missing formula)
• 500: Internal server error
• 200 with error field: Parsing error

IF-expression Normalization

Marina uses the IF-expression normalization technique for SAT solving. This approach:

• Converts boolean formulas to IF-expressions
• Normalizes expressions to reduce complexity
• Performs efficient satisfiability checking
• Returns partial assignments when possible

Performance Characteristics

• Worst-case exponential time complexity (like all SAT solvers)
• Optimized for typical boolean formulas
• Efficient memory usage
• Supports formulas with hundreds of variables

Basic Examples