Skip to main content

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

rascal-Not specified

Standard format for boolean formulas in conjunctive normal form.

Usage​

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

This format is used by the yearly SAT competition, see https://www.satcompetition.org/ .

Examples​

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;