Add examples directory, integrate parsing into SAT instantiation

oldgalileo · oldgalileo · commit 08da9317409d · 2020-08-03T14:43:39.000-07:00
diff --git a/dimacs.txt b/dimacs.txt
diff --git a/examples/complex.dimacs b/examples/complex.dimacs
@@ -0,0 +1,19 @@
+c Problem taken from UMiami CS as mentioned in the README
+c The mappings from lettered to numeric literals were done
+c alphabetically: l=1, m=2, n=3, p=4, q=5, r=6, t=7
+c
+c The correct answer should be 0000111 respectively to the
+c mapping above.
+c
+c Note: If attempting to debug or look through the decision
+c tree on this problem, that these are 0 indexed and l is
+c internally represented as 0.
+p cnf 7 8
+-3 -7 0
+2 5 3 0
+1 -2 0
+-1 -5 0
+1 -4 0
+6 4 3 0
+-6 -1 0
+7 0
diff --git a/examples/format-example.dimacs b/examples/format-example.dimacs
@@ -0,0 +1,23 @@
+c The DIMACS format is pretty limited. You use `c` for comments,
+c then start describing the problem using `p`
+
+p cnf 2 2
+
+c Where the `p` signifies that this line is going to set up the
+c parameters. Then you specify what format the SAT problem will
+c be in (it should _always_ be CNF for this project). And finally,
+c you give it two numbers: the number of literals, and the number
+c of clauses. After that, each uncommented line should be:
+
+1 -2 0
+
+c The first two numbers are the literals. Negative literals are
+c negated. The 0 delineates that the line is over, meaning that
+c you could, for instance do something like:
+
+-1
+c Comment in the middle
+2
+0
+
+c This will be properly parsed and output 10 as a possible answer.
diff --git a/examples/simple-unsat.dimacs b/examples/simple-unsat.dimacs
@@ -0,0 +1,6 @@
+c Example of the simplest unsatisfiable SAT problem.
+p cnf 2 4
+ 1  2 0
+-1  2 0
+ 1 -2 0
+-1 -2 0
diff --git a/examples/simple.dimacs b/examples/simple.dimacs
@@ -0,0 +1,5 @@
+c This is a very simple SAT problem where the viable answer
+c is either (1:ON and 2:OFF) or (1:OFF and 2:ON)
+p cnf 2 2
+1 -2 0
+-1 2 0
diff --git a/examples/wiki.dimacs b/examples/wiki.dimacs
@@ -0,0 +1,12 @@
+c Problem taken from the DPLL Wikipedia page as mentioned
+c in the README. Mapping from alphabetical to numeric literals
+c was done in alphabetical order.
+p cnf 4 8
+-1 2 3 0
+1 3 4 0
+1 -3 4 0
+1 3 -4 0
+1 -3 -4 0
+-2 -3 4 0
+-1 2 -3 0
+-1 -2 3 0
diff --git a/src/main.cpp b/src/main.cpp
@@ -1,191 +1,29 @@
-#include <stdio.h>
 #include <vector>
 #include <iostream>
-#include <fstream>
-#include <sstream>
 #include "sat.h"
 
-std::optional<std::vector<std::vector<std::tuple<int, bool>>>> parse(std::string path) {
-    std::ifstream in(path);
-    std::vector<std::vector<std::tuple<int,bool>>> pc;
-
-    std::string dimacsType;
-    int literals;
-    int clauses;
-    for(std::string line; std::getline(in, line);) {
-        if(line.empty() || line[0] == 'c') continue;
-        // TODO: Throw exception
-        if (line[0] != 'p') {
-            std::cout << "NOT PARAMS" << std::endl;
-            return std::nullopt;
-        }
-        else {
-            char pch;
-            std::stringstream ss(line);
-            ss >> pch >> dimacsType >> literals >> clauses;
-            if(!ss.eof()) {
-                // TODO: Throw exception
-                return std::nullopt;
-            }
-            break;
-        }
-    }
-    std::vector<std::tuple<int, bool>> clause;
-    for(std::string line; std::getline(in, line);) {
-        if(line.empty() || line[0] == 'c') continue;
-        if(line[0] == 'p') return std::nullopt;
-        int literal;
-        std::stringstream ss(line);
-        while(ss >> literal && literal != 0)
-            clause.emplace_back(std::make_tuple(std::abs(literal) - 1, literal < 0));
-        if(literal == 0) {
-            pc.push_back(std::move(clause));
-            clause = {};
-        }
-    }
-    return std::make_optional(pc);
-}
-
-int main() {
-    auto result = parse("/Users/galileo/CLionProjects/sat-solver/dimacs.txt");
-    if(result.has_value()) {
-        for (const auto& a : result.value()) {
-            for(const auto& b : a)
-                std::cout << "(" << std::get<0>(b) << "," << std::get<1>(b) << ") ";
-            std::cout << std::endl;
-        }
-    }
-    {
-        std::cout << "Problem 1: Answer is either 01 or 10\nResult: ";
-        std::vector<std::tuple<int, bool>> p1{
-                std::make_tuple(0, false), std::make_tuple(1, true)
-        };
-        std::vector<std::tuple<int, bool>> p2{
-                std::make_tuple(0, true), std::make_tuple(1, false)
-        };
-        std::vector<std::vector<std::tuple<int, bool>>> pClauses{
-                p1, p2
-        };
-        auto sat = NaiveSAT(2, pClauses);
-        auto result = sat.solve();
-        if (!result.has_value()) {
-            std::cout << "unsatisfiable";
-        }
+void printResults(const std::optional<std::vector<bool>>& result) {
+    if (!result.has_value()) {
+        std::cout << "unsatisfiable" << std::endl;
+    } else {
         for (const auto b : result.value()) {
             std::cout << b;
         }
+        std::cout << std::endl;
     }
-    {
-        std::cout << "\n\nProblem 2: Unsatisfiable\nResult: ";
-        std::vector<std::tuple<int, bool>> q1{
-                std::make_tuple(0, false), std::make_tuple(1, false)
-        };
-        std::vector<std::tuple<int, bool>> q2{
-                std::make_tuple(0, false), std::make_tuple(1, true)
-        };
-        std::vector<std::tuple<int, bool>> q3{
-                std::make_tuple(0, true), std::make_tuple(1, false)
-        };
-        std::vector<std::tuple<int, bool>> q4{
-                std::make_tuple(0, true), std::make_tuple(1, true)
-        };
-        std::vector<std::vector<std::tuple<int, bool>>> qClauses{
-                q1, q2, q3, q4
-        };
-
-        auto sat = NaiveSAT(4, qClauses);
-        auto result = sat.solve();
-        if (!result.has_value()) {
-            std::cout << "unsatisfiable";
-        } else {
-            for (const auto b : result.value()) {
-                std::cout << b;
-            }
-        }
-    }
-
-    {
-        std::cout << "\n\nProblem 3: Answer should be 0000111\nResult: ";
-        std::vector<std::tuple<int, bool>> r1{
-                std::make_tuple(2, true), std::make_tuple(6, true)
-        };
-        std::vector<std::tuple<int, bool>> r2{
-                std::make_tuple(1, false), std::make_tuple(2, false),
-                std::make_tuple(4, false)//, std::make_tuple(0, true)
-        };
-        std::vector<std::tuple<int, bool>> r3{
-                std::make_tuple(0, false), std::make_tuple(1, true)
-        };
-        std::vector<std::tuple<int, bool>> r4{
-                std::make_tuple(0, true), std::make_tuple(4, true)
-        };
-        std::vector<std::tuple<int, bool>> r5{
-                std::make_tuple(0, false), std::make_tuple(3, true)
-        };
-        std::vector<std::tuple<int, bool>> r6{
-                std::make_tuple(5, false), std::make_tuple(2, false), std::make_tuple(3, false)
-        };
-        std::vector<std::tuple<int, bool>> r7{
-                std::make_tuple(5, true), std::make_tuple(0, true)
-        };
-        std::vector<std::tuple<int, bool>> r8{
-                std::make_tuple(6, false)
-        };
-        std::vector<std::vector<std::tuple<int, bool>>> rClauses{
-                r1, r2, r3, r4, r5, r6, r7, r8
-        };
-
-        auto sat = NaiveSAT(7, rClauses);
-        auto result = sat.solve();
-        if (!result.has_value()) {
-            std::cout << "unsatisfiable";
-        } else {
-            for (const auto b : result.value()) {
-                std::cout << b;
-            }
-        }
-    }
+}
 
-    {
-        // Taken from the DPLL Algorithm Wikipedia page
-        std::cout << "\n\nProblem 4: Answer should be 1111 or 1101\nResult: ";
-        std::vector<std::tuple<int, bool>> w1{
-                std::make_tuple(0, true), std::make_tuple(1, false), std::make_tuple(2, false)
-        };
-        std::vector<std::tuple<int, bool>> w2{
-                std::make_tuple(0, false), std::make_tuple(2, false), std::make_tuple(3, false)
-        };
-        std::vector<std::tuple<int, bool>> w3{
-                std::make_tuple(0, false), std::make_tuple(2, false), std::make_tuple(3, true)
-        };
-        std::vector<std::tuple<int, bool>> w4{
-                std::make_tuple(0, false), std::make_tuple(2, true), std::make_tuple(3, false)
-        };
-        std::vector<std::tuple<int, bool>> w5{
-                std::make_tuple(0, false), std::make_tuple(2, true), std::make_tuple(3, true)
-        };
-        std::vector<std::tuple<int, bool>> w6{
-                std::make_tuple(1, true), std::make_tuple(2, true), std::make_tuple(3, false)
-        };
-        std::vector<std::tuple<int, bool>> w7{
-                std::make_tuple(0, true), std::make_tuple(1, false), std::make_tuple(2, true)
-        };
-        std::vector<std::tuple<int, bool>> w8{
-                std::make_tuple(0, true), std::make_tuple(1, true), std::make_tuple(2, false)
-        };
-        std::vector<std::vector<std::tuple<int, bool>>> wClauses{
-                w1, w2, w3, w4, w5, w6, w7, w8
-        };
+int main() {
+    auto simple = NaiveSAT::parse("examples/simple.dimacs");
+    printResults(simple.solve());
+    auto simple_unsat = NaiveSAT::parse("examples/simple-unsat.dimacs");
+    printResults(simple_unsat.solve());
+    auto complex = NaiveSAT::parse("examples/complex.dimacs");
+    printResults(complex.solve());
+    auto wiki = NaiveSAT::parse("examples/wiki.dimacs");
+    printResults(wiki.solve());
+    auto format_example = NaiveSAT::parse("examples/format-example.dimacs");
+    printResults(format_example.solve());
 
-        auto sat = NaiveSAT(4, wClauses);
-        auto result = sat.solve();
-        if (!result.has_value()) {
-            std::cout << "unsatisfiable";
-        } else {
-            for (const auto b : result.value()) {
-                std::cout << b;
-            }
-        }
-    }
     return 0;
 }
diff --git a/src/sat.cpp b/src/sat.cpp
@@ -2,6 +2,8 @@
 #include <vector>
 #include <unordered_map>
 #include <iostream>
+#include <fstream>
+#include <sstream>
 
 std::optional<std::vector<bool>> NaiveSAT::solve() {
     return(this->solve(this->clauses, this->literals));
@@ -142,3 +144,67 @@ std::vector<std::vector<std::tuple<int, bool>>> NaiveSAT::simplify(std::vector<s
     return clauses;
 }
 
+/**
+ * Parse file at path as a DIMACS-compliant file
+ *
+ * @param path to DIMACS file
+ * @return NaiveSAT represenatation of the problem
+ * @throws std::runtime_exception
+ */
+NaiveSAT NaiveSAT::parse(const std::string& path) {
+    std::ifstream in(path);
+    if(!in.is_open())
+        throw std::runtime_error("could not open file at " + path);
+    std::vector<std::vector<std::tuple<int,bool>>> pc;
+
+    std::string dimacsType;
+    int literals;
+    int clauses;
+    // First parse until we get to the parameters
+    for(std::string line; std::getline(in, line);) {
+        if(line.empty() || line[0] == 'c') continue;
+        if (line[0] != 'p') {
+            throw std::runtime_error("found problem contents when expecting parameters");
+        }
+        else {
+            // Throwaway char to read the 'p' into.
+            char pch;
+            std::stringstream ss(line);
+            // Read in the parameters
+            ss >> pch >> dimacsType >> literals >> clauses;
+            // Check that that is both the end of that line,
+            // and that this is a CNF DIMACS file.
+            if(!ss.eof() || dimacsType != "cnf") {
+                throw std::runtime_error("received unexpected parameters");
+            }
+            break;
+        }
+    }
+    // Now we read each of the clauses
+    std::vector<std::tuple<int, bool>> clause;
+    for(std::string line; std::getline(in, line);) {
+        if(line.empty() || line[0] == 'c') continue;
+        if(line[0] == 'p') throw std::runtime_error("found parameters when expecting problem contents");
+
+        int literal;
+        std::stringstream ss(line);
+        // Read into the the clause until we hit the end of the line or a 0
+        // Anything after the 0 is ignored and treated as a comment.
+        while(ss >> literal && literal != 0)
+            clause.emplace_back(std::make_tuple(std::abs(literal) - 1, literal < 0));
+        // If the above loop ended on the 'end of the line' case
+        // and not the 0 case, then we need to continue to add to
+        // the same clause until we hit the 0 case.
+
+        // Once we find the 0 delimiter, we move the clause to the end
+        // of the clauses container, and then reinitialize so it's empty.
+        if(literal == 0) {
+            pc.push_back(std::move(clause));
+            clause = {};
+        }
+    }
+    if(pc.size() != clauses)
+        throw std::runtime_error("invalid number of clauses");
+    return NaiveSAT(literals, pc);
+}
+
diff --git a/src/sat.h b/src/sat.h
@@ -22,6 +22,7 @@ class NaiveSAT : SAT {
     NaiveSAT(int numLiterals, std::vector<std::vector<std::tuple<int, bool>>> clauses)
             : SAT(numLiterals, std::move(clauses)) {};
 public:
+    static NaiveSAT parse(const std::string& path);
     std::optional<std::vector<bool>> solve() override;
 private:
     std::optional<std::vector<bool>> solve(std::vector<std::vector<std::tuple<int,bool>>> clauses, std::vector<bool> literals);

-Original file line number
+Diff line change
@@ @@ -0,0 +1,6 @@ @@
 +c Example of the simplest unsatisfiable SAT problem.
 +p cnf 2 4
 + 1  2 0
 +-1  2 0
 + 1 -2 0
 +-1 -2 0