Syntax Guide

Comprehensive reference for Marina SAT Solver boolean formula syntax

BNF Grammar

Formal definition of valid formulas

<prop> ::=  T                     (true)
          | F                     (false)
          | <atom>               (variable)
          | ~ <prop>             (negation)
          | <prop> & <prop>      (conjunction)
          | <prop> | <prop>      (disjunction)
          | <prop> -> <prop>     (implication)
          | <prop> <-> <prop>    (equivalence)
          | ( <prop> )           (parentheses)

<atom> ::= [a-z][a-z0-9_]*       (lowercase letters, numbers, underscore)

Operator Precedence

1. Parentheses
Highest precedence - ( )
2. Negation
~ (NOT)
3. Conjunction
& (AND)
4. Disjunction
| (OR)
5. Implication
->
6. Equivalence
<->

Variable Rules

Valid Variables
ab1var_namex_123
Invalid Variables
Avar-name1var_var

Operators Reference

&
AND
Operator

Logical conjunction - both operands must be true

Example:a & b
Result:

true only if both a AND b are true

|
OR
Operator

Logical disjunction - at least one operand must be true

Example:a | b
Result:

true if a OR b (or both) are true

~
NOT
Operator

Logical negation - inverts the truth value

Example:~a
Result:

true if a is false, false if a is true

->
IMPLY
Operator

Material implication - if a then b

Example:a -> b
Result:

false only if a is true and b is false

<->
EQUIV
Operator

Logical equivalence - a if and only if b

Example:a <-> b
Result:

true if a and b have the same truth value

Common Examples

Simple Expression

a & (b | c)

a must be true AND (b OR c must be true)

Implication Chain

(a -> b) & (b -> c)

If a then b, and if b then c

De Morgan's Law

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

The negation of a conjunction is equivalent to the disjunction of negations

Distributive Law

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

AND distributes over OR

Contradiction

a & ~a

Always false (unsatisfiable)

Tautology

a | ~a

Always true (valid)

Common Mistakes

Missing parentheses

Error
Wrong:a & b | c
Correct:(a & b) | c or a & (b | c)

Reason: Operator precedence is ambiguous without parentheses

Invalid variable names

Error
Wrong:A1 or var-name
Correct:a1 or var_name

Reason: Only lowercase, underscores, and numbers allowed

Missing operator

Error
Wrong:a b
Correct:a & b or a | b

Reason: Need an operator between variables

Double negation error

Error
Wrong:~~a (if expecting a)
Correct:a

Reason: Double negation cancels out (~ ~a is equivalent to a)

Quick Tips

  • Always use parentheses for complex expressions
  • Use T for true and F for false constants
  • Variables must start with a lowercase letter
  • White spaces are ignored during parsing
  • Use the solver page to test your formulas