lib/smt/src/dimacs.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! Reads and writes Boolean formulas in conjunctive normal form as plain text. The format is DIMACS
2 //! CNF: a `p cnf V C` header gives the variable and clause counts, `c` lines are comments, and each
3 //! clause lists its literals as signed variable numbers, 1-based, ending with 0.
4 //!
5 //! Other SAT tools and benchmark collections exchange formulas as text, so a caller needs to load
6 //! such a file into a solver and to print a solver's clauses for another tool. A text written
7 //! elsewhere may be malformed, or may disagree with its own header about how many clauses it holds.
8 //!
9 //! Variable 1 of the text is the solver's variable 0, and a negative number is the negated literal.
10 //! The reader treats the header's clause count as a check and its variable count as a floor: a
11 //! clause may name a variable past the count, and the solver grows to hold it. The writer prints
12 //! every clause the solver holds, learned clauses the solver kept included, so a text written after
13 //! a solve can hold more clauses than were added.
14 const std = @import("std");
15 const sat = @import("sat/root.zig");
16
17 /// The errors `parse` returns for a malformed text, besides the allocator's and the solver's, so
18 /// code that reports why a DIMACS text was refused can switch on them. A header count that fails to
19 /// parse as a number returns the error of `std.fmt.parseInt`, which this set leaves out. `parse`
20 /// returns an inferred error set.
21 pub const ParseError = error{
22 /// A `p` line whose kind differs from `cnf` or that lacks a count.
23 InvalidHeader,
24 /// A clause token other than a 32-bit signed integer, or a last clause missing a closing 0.
25 InvalidLiteral,
26 /// The number of clauses differs from the header's count.
27 ClauseCountMismatch,
28 };
29
30 /// Returns a new solver that allocates with `allocator` and holds the variables and clauses of the
31 /// DIMACS text `source`, so code can load a formula written by another tool, then solve the
32 /// returned solver. The caller owns the solver and frees it with `deinit`. Lines are trimmed of
33 /// spaces, tabs and carriage returns, and blank lines and lines starting with `c` are skipped. A
34 /// `p cnf V C` line adds V variables and sets C as the expected clause count. The parser accepts a
35 /// text without a header, and a second header adds its variables and replaces the expected count. A
36 /// clause may span lines, and one line may hold more than one clause: each 0 ends one. A lone 0 is
37 /// the empty clause. The call returns `InvalidHeader`, `InvalidLiteral` and `ClauseCountMismatch`
38 /// as their tags describe, and the errors of `std.fmt.parseInt` for a header count that fails to
39 /// parse as a number. The literal -2147483648 makes the call panic.
40 pub fn parse(allocator: std.mem.Allocator, source: []const u8) !sat.Solver {
41 var solver = sat.Solver.init(allocator);
42 errdefer solver.deinit();
43 var expected_clauses: ?usize = null;
44 var clauses_seen: usize = 0;
45 var clause: std.ArrayList(sat.Literal) = .empty;
46 defer clause.deinit(allocator);
47 var lines = std.mem.splitScalar(u8, source, '\n');
48 while (lines.next()) |raw_line| {
49 const line = std.mem.trim(u8, raw_line, " \t\r");
50 if (line.len == 0 or line[0] == 'c') continue;
51 var tokens = std.mem.tokenizeAny(u8, line, " \t\r");
52 const first = tokens.next() orelse continue;
53 if (std.mem.eql(u8, first, "p")) {
54 const kind = tokens.next() orelse return ParseError.InvalidHeader;
55 if (!std.mem.eql(u8, kind, "cnf")) return ParseError.InvalidHeader;
56 const variable_count = try std.fmt.parseInt(usize, tokens.next() orelse return ParseError.InvalidHeader, 10);
57 expected_clauses = try std.fmt.parseInt(usize, tokens.next() orelse return ParseError.InvalidHeader, 10);
58 var index: usize = 0;
59 while (index < variable_count) : (index += 1) _ = try solver.addVariable();
60 continue;
61 }
62 var current: ?[]const u8 = first;
63 while (current) |token| {
64 const value = std.fmt.parseInt(i32, token, 10) catch return ParseError.InvalidLiteral;
65 if (value == 0) {
66 try solver.addClause(clause.items);
67 clause.clearRetainingCapacity();
68 clauses_seen += 1;
69 } else {
70 try clause.append(allocator, try sat.Literal.fromDimacs(value));
71 }
72 current = tokens.next();
73 }
74 }
75 if (clause.items.len > 0) return ParseError.InvalidLiteral;
76 if (expected_clauses) |expected| {
77 if (expected != clauses_seen) return ParseError.ClauseCountMismatch;
78 }
79 return solver;
80 }
81
82 /// Writes `solver` as DIMACS CNF: a `p cnf V C` header, then one line per clause of its literals
83 /// and a closing 0, so code can hand a solver's formula to another tool. An empty clause added to
84 /// the solver appears once, as a line holding only 0, and the header counts it. The function writes
85 /// every clause the solver holds, learned clauses the solver kept included. The call returns only
86 /// the writer's errors.
87 pub fn write(writer: *std.Io.Writer, solver: *const sat.Solver) std.Io.Writer.Error!void {
88 const empty_clauses: usize = @intFromBool(solver.has_empty_clause);
89 try writer.print("p cnf {d} {d}\n", .{
90 solver.variableCount(),
91 solver.clauseCount() + empty_clauses,
92 });
93 if (solver.has_empty_clause) {
94 try writer.writeAll("0\n");
95 }
96 for (solver.clauses.items) |clause| {
97 for (clause.literals) |literal| {
98 try writer.print("{d} ", .{literal.toDimacs()});
99 }
100 try writer.writeAll("0\n");
101 }
102 }
103
104 test "DIMACS writer preserves the empty clause" {
105 var solver = sat.Solver.init(std.testing.allocator);
106 defer solver.deinit();
107 _ = try solver.addVariable();
108 try solver.addClause(&.{sat.Literal.positive(0)});
109 try solver.addClause(&.{});
110 var buffer: [64]u8 = undefined;
111 var stream = std.Io.Writer.fixed(&buffer);
112 try write(&stream, &solver);
113 const text = stream.buffered();
114 try std.testing.expect(std.mem.indexOf(u8, text, "p cnf 1 2\n") != null);
115 try std.testing.expect(std.mem.indexOf(u8, text, "\n0\n") != null);
116
117 var parsed = try parse(std.testing.allocator, text);
118 defer parsed.deinit();
119 try std.testing.expectEqual(sat.Status.unsat, try parsed.solve());
120 }
121
122 test "DIMACS parser builds satisfiable formula" {
123 var solver = try parse(std.testing.allocator,
124 \\c example
125 \\p cnf 2 2
126 \\1 2 0
127 \\-1 0
128 \\
129 );
130 defer solver.deinit();
131 try std.testing.expectEqual(sat.Status.sat, try solver.solve());
132 }
133
134 test "DIMACS writer roundtrips clauses" {
135 var solver = sat.Solver.init(std.testing.allocator);
136 defer solver.deinit();
137 const a = try solver.addVariable();
138 const b = try solver.addVariable();
139 try solver.addClause(&.{ sat.Literal.positive(a), sat.Literal.negative(b) });
140 var buffer: [256]u8 = undefined;
141 var stream = std.Io.Writer.fixed(&buffer);
142 try write(&stream, &solver);
143 const text = stream.buffered();
144 try std.testing.expect(std.mem.indexOf(u8, text, "p cnf 2 1\n") != null);
145 try std.testing.expect(std.mem.indexOf(u8, text, "1 -2 0\n") != null);
146 }