Test case with 2 contradictory clauses runs forever

[insideoutclub]

Here's the test case:

require("babel-polyfill");
const sat = require("@aureooms/js-sat");

const instance = sat.from.parities([[80], [81]]);
console.log(JSON.stringify(instance));
console.log(sat.decide(instance));

On my x64 Windows box, when I save this as sat.js and run "node sat.js", I get the following:

node sat.js
{"clauses":[[80],[81]],"n":41}

It just spins forever using up one my CPUs. If I change the clauses to [[0], [1]], it runs quickly and correctly decides that these clauses are not satisfiable. Starting around [[50], [51]], things get really slow.

[make-github-pseudonymous-again]

At first sight it seems to be related to the artificially high number of variables (41 in your example sat.from.parities([[80], [81]])).

[make-github-pseudonymous-again]

At first sight it seems to be related to the artificially high number of variables (41 in your example sat.from.parities([[80], [81]])).

Yeah that is definitely the problem. The way SAT0W works is by assigning true or false to some variables, quitting early if a contradiction arises. What happens with your example is that, because this implementation tests assignments on variables in order, it discovers the contradiction only after having assigned a value to each of the n-1 remaining variables. It thus tests all possible 2**(n-1) assignments, without realizing that the contradiction is independent of these assignments...

One way to avoid this problem would be to automatically map the literals down to something more reasonable (like 0 and 1). I don't know if this should be automatic. When I wrote this library, I assumed that someone using sat.from.parities would already have done this mapping. The only mapping that happens in this library is when using sat.from.keys. In that case n is the minimum necessary. Using sat.from.signs would cause the same problem as above.

Another way to reduce the number of variables in your specific example would be to get rid of clauses that have size 1. One could also use implication to model clauses of size 2.

@insideoutclub Does that make sense?

[insideoutclub]

I'm trying to write a reasoner for the board game "Clue"/"Cluedo" like the one specified at http://cs.gettysburg.edu/~tneller/nsf/clue/ There may be up to 147 variables (6 players + 1 Case File) * 21 cards. Each variable represents whether a player holds a card or not. How would I get rid of clauses that have size 1? What does it mean to use implication to model clauses of size 2?

[make-github-pseudonymous-again]

There may be up to 147 variables (6 players + 1 Case File) * 21 cards.

I have no idea if this library is powerful enough to solve your problem. However, I would be willing to help improve it to solve your problem if it is possible.

The first thing you should try is use sat.from.keys to make sure no extra variable is created.

How would I get rid of clauses that have size 1?

If that is not enough, and if you have a lot of size-one clauses, try the following: until there is no size-one clause left, pick one, remove each clause containing the literal of that clause and remove the negated literal from each clause containing one. If there is an empty clause, conclude unsatisfiability.

What does it mean to use implication to model clauses of size 2?

A clause of size 2 [a, b] can be thought of as the implication not a => b or not b => a.

[insideoutclub]

I've moved on. I'm using https://www.npmjs.com/package/boolean-sat instead. Thank-you.

[make-github-pseudonymous-again]

No problem!