1/** \file
2 * \brief Tests for Minisat wrapper
3 *
4 * \author Stephan Beyer (satisfiableTest by Robert Zeranski)
5 *
6 * \par License:
7 * This file is part of the Open Graph Drawing Framework (OGDF).
8 *
9 * \par
10 * Copyright (C)<br>
11 * See README.md in the OGDF root directory for details.
12 *
13 * \par
14 * This program is free software; you can redistribute it and/or
15 * modify it under the terms of the GNU General Public License
16 * Version 2 or 3 as published by the Free Software Foundation;
17 * see the file LICENSE.txt included in the packaging of this file
18 * for details.
19 *
20 * \par
21 * This program is distributed in the hope that it will be useful,
22 * but WITHOUT ANY WARRANTY; without even the implied warranty of
23 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
24 * GNU General Public License for more details.
25 *
26 * \par
27 * You should have received a copy of the GNU General Public
28 * License along with this program; if not, see
29 * http://www.gnu.org/copyleft/gpl.html
30 */
31
32#include <ogdf/basic/Graph.h>
33#include <ogdf/external/Minisat.h>
34#include <resources.h>
35
36static void satisfiableTest()
37{
38 Minisat::Formula F;
39 Minisat::Model model;
40
41 F.addClause(std::vector<int>{-1, -2, -3, 4});
42
43 F.newVars(11);
44
45 for (int i = 1; i < 10; i++) {
46 Minisat::clause c = F.newClause();
47 if (i % 2 == 0) {
48 c->add(i);
49 }
50 else {
51 c->add(-i);
52 }
53 c->add(i+1);
54 F.finalizeClause(c);
55 }
56
57 bool satisfiable = F.solve(model);
58
59 AssertThat(satisfiable, IsTrue());
60#if 0
61 std::cout << "#vars = " << F.getVariableCount() << std::endl;
62 std::cout << "#clauses = " << F.getClauseCount() << std::endl;
63 if (val) {
64 model.printModel();
65 }
66 F.reset();
67#endif
68}
69
70static void nonsatisfiableTest()
71{
72 Minisat::Formula F;
73 Minisat::Model model;
74 F.addClause(std::vector<int>{1, 2});
75 F.addClause(std::vector<int>{1, -2, 3});
76 F.addClause(std::vector<int>{-1, 2});
77 F.addClause(std::vector<int>{-1, -2});
78 F.addClause(std::vector<int>{-3});
79
80 bool satisfiable = F.solve(model);
81
82 AssertThat(satisfiable, IsFalse());
83}
84
85static void readDIMACSTest()
86{
87 Minisat::Formula formula;
88 std::stringstream ss{ResourceFile::get("minisat/satisfiable.txt")->data()};
89 AssertThat(formula.readDimacs(ss), IsTrue());
90 Minisat::Model model;
91 bool satisfiable = formula.solve(model);
92 AssertThat(satisfiable, IsTrue());
93
94 formula.addClause(std::vector<int>{3});
95 satisfiable = formula.solve(model);
96 AssertThat(satisfiable, IsFalse());
97}
98
99go_bandit([]() {
100 describe("Minisat wrapper", []() {
101 it("solves a satisfiable formula", []() {
102 satisfiableTest();
103 });
104 it("solves a non-satisfiable formula", []() {
105 nonsatisfiableTest();
106 });
107 it("reads a DIMACS file and is able to solve the formula and change it", []() {
108 readDIMACSTest();
109 });
110 });
111});
112