Module formula 

Logic and formula problems.

Problems whose input is a boolean formula or circuit:

• Satisfiability: Boolean satisfiability (SAT) with CNF clauses
• NAESatisfiability: Not-All-Equal satisfiability with CNF clauses
• KSatisfiability: K-SAT where each clause has exactly K literals
• Maximum2Satisfiability: MAX-2-SAT — maximize satisfied 2-literal clauses
• NonTautology: Find a falsifying assignment for a DNF formula
• OneInThreeSatisfiability: Exactly one literal true per clause (1-in-3 SAT)
• Planar3Satisfiability: 3-SAT restricted to planar variable-clause incidence graphs
• CircuitSAT: Boolean circuit satisfiability
• QuantifiedBooleanFormulas: Quantified Boolean Formulas (QBF) — PSPACE-complete

Structs

Assignment

An assignment in a circuit: outputs = expr.

BooleanExpr

A boolean expression tree.

CNFClause

A clause in conjunctive normal form (CNF).

Circuit

A boolean circuit as a sequence of assignments.

CircuitSAT

The Circuit SAT problem.

KSatisfiability

K-Satisfiability problem where each clause has exactly K literals.

Maximum2Satisfiability

Maximum 2-Satisfiability problem where each clause has exactly 2 literals.

NAESatisfiability

Not-All-Equal Boolean Satisfiability (NAE-SAT) in CNF form.

NonTautology

Non-Tautology problem.

OneInThreeSatisfiability

One-in-Three Satisfiability problem.

Planar3Satisfiability

Planar 3-Satisfiability problem.

QuantifiedBooleanFormulas

Quantified Boolean Formulas (QBF) problem.

Satisfiability

Boolean Satisfiability (SAT) problem in CNF form.

Enums

BooleanOp

Boolean expression node types.

Quantifier

Quantifier type for QBF variables.