next up previous contents
Next: DNF format Up: CNF format Previous: File Header   Contents

Boolean functions

The only Boolean functions accepted in this format are clauses. A clause has the following syntax:

[-]<var> ... [-]<var> 0

where <var> is a variable and '-' in front of a <var> makes it a negative literal and no '-' in front of <var> makes it a positive literal. There are no commas in the variable list and the list is terminated with a 0. Variables may appear in a variable list in any order and are separated by blank characters. For an example see Figure [*], Page [*].

John Franco 2011-09-15