Skip to main content

module lang::dimacs::\syntax::Dimacs


Standard format for boolean formulas in conjunctive normal form.


import lang::dimacs::\syntax::Dimacs;

This format is used by the yearly SAT competition, see .


This is a sample .cnf file:

c A sample .cnf file.
p cnf 3 2
1 -3 0
2 3 -1 0

syntax L

layout L = [\t\ \r]*;

syntax Comment

lexical Comment = comment: "c" ![\n]* "\n";

syntax Prologue

lexical Prologue = prologue: "p" "cnf" Number variables Number clauses ![\n]* "\n";

syntax Number

lexical Number 
= positive: [0-9]+ !>> [0-9]
| non-assoc negative: "-" Number number

syntax Dimacs

start syntax Dimacs
= Prologue prologue {Line "\n"}+ lines "\n";

syntax Line

syntax Line 
= disjunct: Disjunct disjunct
| comment: Comment comment

syntax Disjunct

syntax Disjunct = Number+ numbers;