Boolean Satisfiability

[xLeachimx]

No description provided.

[joshuaguerin]

Looks pretty good so far. I’d like to sit down and play with the input generation a bit.

A couple of things occur to me at first glance:

• Could you describe the nature of the simplification predicates at the start of the code? I like to avoid (where possible) leaving anything up to the reader.
• Do you think you could whip up a quick printer? The predicates are actually substantially readable, but for large instances the predicates take up a bit of room. Perhaps something as simple as a sorted list of true variables on a line, and another of false (with labels)?
• I think a similar explanation for the reader: "% Clause satisfiability” Perhaps there could be a colon, then state exactly what you are looking for?
• In the example, could you speak to what max sat looks like as well, perhaps with regard to the same instance?

I’ll have to sit down in a while an do some tinkering with running things, but this is a smart addition.

I’ve never actually thought to represent SAT this way because I typically default to something like Minisat. Pretty cool. I would think it introduces a new category. Need to figure out the best way to say it.

[xLeachimx]

To address the given points:

1. Simplification might be poor word usage. It refers to using a single predicate whenever I need to discuss that something is a literal or a clause, thus I can use literal(X) rather than using clause(_,L), which would also require a |L| somewhere in case a literal is only used in clauses where it is negated.
2. Yeah, no problem. Perhaps render into html where we could display three sections: the true list, false list, colored text version of the instance highlighting which literals (or their negation) are true, and thus showing manually each clause is satisfied.
3. Probably right there, will need to think about how to phrase what I mean.
4. Yeah, probably need a different example because Max-SAT (or at least the unweighted version this solves) would just be the same since it maximizes clause satisfaction, perhaps two examples used for both, one satisfiable and one unsatisfiable.

[joshuaguerin]

For the docs, just remember to document the actual thoughts behind the lines. Role can be important, too, but we are going for people who don’t know the systems.

For rendering I’d go even simpler: ASCII should do the trick (see the subset sum, sudoku, or wolf/goat/cabbage).

I’m trying to keep outputs as simple and consistent as possible. One of the few exceptions right now is graphviz.

Different examples could work, or a single statement with a satisfying assignment that is smaller than the maximal version.

Either way, best not to leave some of the definitions up to the imagination if we can avoid it.