Fix a bug where only positive assumptions were accepted

dirkschumacher · Mar 4, 2018 · ea4f8c2 · ea4f8c2
1 parent 2243675
commit ea4f8c2
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/index.js b/index.js
@@ -21,7 +21,7 @@ const isValidAssumptions = (assumptions, nvars) => {
   // TODO: check for duplicates
   return Array.isArray(assumptions) &&
          assumptions.every(Number.isInteger) &&
-         assumptions.every(x => x >= 1 && x <= nvars)
+         assumptions.map(Math.abs).every(x => x >= 1 && x <= nvars)
 }
 
 const picosat_sat = (formula, assumptions) => {

diff --git a/package.json b/package.json
@@ -1,6 +1,6 @@
 {
   "name": "picosat",
-  "version": "1.0.1",
+  "version": "1.0.2",
   "description": "picosat SAT solver",
   "main": "index.js",
   "files": [

diff --git a/test.js b/test.js
@@ -12,11 +12,11 @@ test("it solves a simple problem", (t) => {
 
 test("it supports assumptions", (t) => {
   const formula = [[1, 2], [-1, 2]]
-  const assumptions = [1, 2]
+  const assumptions = [-1, 2]
   const result = picosat_sat(formula, assumptions)
   t.equal(result.satisfiable, true)
   t.equal(result.solution.length, 2)
-  t.equal(result.solution[0], 1)
+  t.equal(result.solution[0], -1)
   t.equal(result.solution[1], 2)
   t.end()
 })