You're right, doc is very lacking for now. As Gys assumed correctly, when you work in the SAT solving field, using gophersat is very straightforward, but for a

You're right, doc is very lacking for now. As Gys assumed correctly, when you work in the SAT solving field, using gophersat is very straightforward, but for a more wider audience, it is really lacking. A complete documentation and a tutorial about SAT for end users is a priority in the short term, but in a nutshell: 1. You have a problem that can be represented as a propositional formula (i.e boolean values). For instance : you have three employees, and you must have at least one employee working at any moment, and a given employee cannot work both in the morning and in the afternoon. Oh, and employees a and c don't work very well when they are together. You can represent it this way : - e1-m means employee 1 works in the morning, e2-m employee 2 etc. - e1-a means employee 1 works in the afternoon, etc. - all those constraints (called "clauses") must be checked : - e1-m or e2-m or e3-m (at least one employee in the morning) - e1-a or e2-a or e3-a (at least one in the afternoon) - not(e1-m) or not(e1-a) (e1 cannot work both in the morning and in the afternoon) - not(e2-m) or not(e2-a) - not(e3-m) or not(e3-a) - not(e1-m) or not(e3-m) (e1 and e3 can't both work in the morning) - not(e1-a) or not(e3-a) So: - you have a set of clauses, and all clauses must be true, - each clause is a set of literals, and at least one of these literals must be true. 2. In the DIMACS file format, you associate each variable with an integer value (so, e1-m is 1, e2-m is 2, e3-m 3, e1-a 4, e2-a 5, e3-a 6). A negative value indicates the variable is expected to be false (so, -1 means "not(e1-m)"). Then, each line represents a clause and ends with a 0 (for historical reasons). The above problem would be: 1 2 3 0 4 5 6 0 -1 -4 0 -2 -5 0 -3 -6 0 -1 -3 0 -4 -6 0 The file starts with a prolog, which is `p cnf nb-vars nb-clauses`, so the whole file is p cnf 6 7 1 2 3 0 4 5 6 0 -1 -4 0 -2 -5 0 -3 -6 0 -1 -3 0 -4 -6 0 And, when given that input, gophersat answers : SATISFIABLE -1 2 -3 4 -5 -6 Meaning "there is at least one way to solve your problem, for instance both 2 and 4 are true, everything else is false". So, e2 works in the morning, e1 in the afternoon, and e3 stays at home. We will add, very soon, a facility function, to let the user submit this problem not only in a text format, but by providing a list of list of integers. Next step is providing user-friendly, higher-level input formats. Because, yes, providing DIMACS files for a given problem can be tricky and/or boring.