which enables the user to write scripts involving successive calls to the solver.
The script file contains a list of commands from the following:
cnf <clauses in DIMACS format> end
This command adds the list of clauses between "cnf" and "end" to the sat solver.
The clauses are in dimacs format (zero define the end of a clause).
XOR clauses are still supported by adding x at the beginning of the clause
(more details here).
solve
This command asks the sat solver to find a satisfied assignment for the added CNF.
kill
Executing "kill" command will terminate the run even if there are more commands in the script.
allsols
This command asks the sat solver to find all satisfied assignments for the added CNF.
limitsols <integer x>
This command set a limit on the amount of solutions will be searched and returned by the next "allsols" commands.
When x < 1, the limitation will be removed (=defualt).
output <integer x>
This command declares the relevant literals are 1 to x.
When x < 1, all literals will be relevant (=defualt).
minimize binary <list of literals> 0
solve cnf and try to minimize the literals as they were binary number (LSB is on the left and MSB on the right).
minimize unary <list of literals> 0
Solve cnf and try to minimize the literals as they were unary number (order encoding).
It is recommanded to start a new line after every command and every clause in "cnf ... end" command but it isn't required (whitespace is enough).
The solution file contains the satisified assignments found by the sat solver in the same order they have been found.
The solution file will contains the following:

SAT
<satisfied assignment> 0
The SAT Solver returned a satisified assignment.
Note: If "output x" command has been executed the assignment will contain only varaibles from 1 to x.
UNSAT
The SAT Solver returned there is not satisified assignment for the CNF.
Note: This will be followed by "DONE".
UNSAT ERROR
The SAT solver returned an INCONCLUSIVE solution.
ERROR! <error message>
When an error occured.
DONE
When successfully terminated.
TIMEOUT
When terminated because received SIGINT.
 Search for one/two/all solutions
Script to find a single solution:
cnf
1 2 0
1 2 0
3 4 0
3 4 0
end
solve
kill
Output:
SAT
1 2 3 4 0
DONE
In the above script, replacing "solve" (for finding a solution) with the two commands "limitsols 1" and "allsols" (for finding up to 1 solution) will generate the same single solution.
Script to find up to two solutions:
cnf
1 2 0
1 2 0
3 4 0
3 4 0
end
limitsols 2
allsols
kill
Output:
SAT
1 2 3 4 0
SAT
1 2 3 4 0
DONE
Script to find all solutions:
cnf
1 2 0
1 2 0
3 4 0
3 4 0
end
allsols
kill
Output:
SAT
1 2 3 4 0
SAT
1 2 3 4 0
SAT
1 2 3 4 0
SAT
1 2 3 4 0
DONE
In the above script, adding "limitsols 0" or "limitsols 5" before "allsols" will generate the same output.
 Relevant literls
Script without declaring relevant literals:
cnf
1 2 0
1 2 0
3 4 0
3 4 0
end
allsols
kill
Output:
SAT
1 2 3 4 0
SAT
1 2 3 4 0
SAT
1 2 3 4 0
SAT
1 2 3 4 0
DONE
There are 4 different assignments that satisfy the CNF.
Script with declaring relevant literals:
cnf
1 2 0
1 2 0
3 4 0
3 4 0
end
output 2
allsols
kill
Output:
SAT
1 2 0
SAT
1 2 0
DONE
There are only 2 different assignments that satisfies the cnf when the relevant literals are 1 and 2.
 Minimize binary number
Script which minimize the binary number [4,5,9,10] (lsb first):
cnf
10 9 5 0
4 5 0
1 2 5 0
1 3 5 0
2 3 5 0
1 2 3 4 0
1 2 3 4 0
1 2 3 4 0
1 2 3 4 0
6 7 10 0
6 8 10 0
7 8 10 0
6 7 8 9 0
6 7 8 9 0
6 7 8 9 0
6 7 8 9 0
end
minimize binary 4 5 9 10 0
kill
Output:
SAT
1 2 3 4 5 6 7 8 9 10 0
SAT
1 2 3 4 5 6 7 8 9 10 0
SAT
1 2 3 4 5 6 7 8 9 10 0
UNSAT
DONE
In the first assignment the binary number is [1,1,1,1] = 15
In the second assignment the binary number is [1,0,1,0] = 5
In the third assignment the binary number is [0,1,0,0] = 2
There is no (fourth) assignment when the binary number value < 2.
Therefore the assignment with the minimal value of the binary number is the third assignment.
 Minimize unary number
Script which minimize the unary number [6,7,8,9]:
cnf
1 0
6 0
2 3 0
4 5 0
6 7 0
7 8 0
8 9 0
3 9 0
2 8 0
7 3 0
6 2 0
4 9 0
5 8 0
7 4 0
6 5 0
4 3 8 0
4 3 9 0
4 2 7 0
4 2 8 0
5 3 7 0
5 3 8 0
5 2 6 0
5 2 7 0
3 5 0
3 2 5 4 0
2 4 0
end
minimize unary 6 7 8 9 0
kill
Output:
SAT
1 2 3 4 5 6 7 8 9 0
SAT
1 2 3 4 5 6 7 8 9 0
UNSAT
DONE
In the first assignment the unary number is [1,1,1,0] = 3
In the second assignment the unary number is [1,1,0,0] = 2
There is no (third) assignment when the unary number value < 2.
Therefore the assignment with the minimal value of the binary number is the second assignment.
 Successive calls
Script:
cnf
1 2 0
1 2 0
3 4 0
3 4 0
1 3 0
2 4 0
end
solve
cnf 1 0 2 3 0 end
solve
cnf 3 0 end
solve
cnf 4 2 0 3 4 0 1 4 0 end
solve
kill
Output:
SAT
1 2 3 4 0
SAT
1 2 3 4 0
UNSAT
DONE
The third solve command cause the sat solver to be in UNSAT state, therefore the run will be terminated and the rest of the script will be ignored.