Marina SAT Solver

Solve complex boolean satisfiability problems with our interactive SAT solver.marina being the Malagasy word for True

Fast Solving

Uses IF-expression normalization for efficient SAT solving

Partial Assignments

Returns minimal assignments showing satisfiability

Syntax Validation

Validates formulas with detailed error messages

Web Accessible

Accessible through REST API or web interface

Enter Boolean Formula

SAT
UNSAT

Syntax: & | ~ → ↔ T F ( ) [a-z_][0-9]*

Examples

Click to load examples into the input

Click

Simple AND

Both a and b must be true

a & b
Click

Implication

Complex implication chain

(a & b | ~c) -> d <-> e
Click

Contradiction

Always unsatisfiable

a & ~a
Click

De Morgan

De Morgan&apos;s law example

~(a & b) <-> (~a | ~b)
Click

Zazavavindrano

Malagasy folklore puzzle

zazavavindrano & zazavavindrano -> ((~ swim_warm -> red) & (blue | ~ red))
Click

Complex Logic

Nested operations

~(a -> b|c) <-> ~c&d

Syntax Quick Reference

&AND
|OR
~NOT
->IMPLY
<->EQUIV
TTRUE
FFALSE
a-z_0-9Variables

Active example loaded in input

Formula copied to clipboard

Explore More

SAT Solver

Interactive boolean formula solver with real-time results

Try it now

Examples

Browse through example boolean formulas and puzzles

Browse examples

Syntax Guide

Complete reference for boolean formula syntax and operators

Learn syntax

Quick Syntax Reference

<prop> ::=  T
          | F
          | <atom>
          | ~ <prop>
          | <prop> & <prop>
          | <prop> | <prop>
          | <prop> -> <prop>
          | <prop> <-> <prop>
          | (<prop>)
<atom> ::= ^[a-z_]+[0-9]*$

• Use parentheses for complex expressions: (a & b) -> c

• Variables must match regex: [a-z_][0-9]*

• White spaces are ignored during parsing

• Invalid formulas raise specific exceptions