PB'05: solvers page (tabular format)

• Category "no optimization function" (SAT)
  This is the category of problems which do not include an objective function. Since there's no optimization to perform, the expected answer is either SAT or UNSAT.
• Category "optimization, small integers" (OPTSMALLINT)
  The benchmarks in this category contain an objective function which sould be minimized. They use only small integers, which means that they contain no constraint with a sum of coefficients greater than 2²⁰ (20 bits). The expected answer is OPTIMUM FOUND or UNSAT (possibly SAT when a solver finds a model but cannot prove it is the optimum solution).
• Category "optimization, medium integers" (OPTMEDINT)
  The benchmarks in this category contain an objective function which sould be minimized. This category contains the set of benchmarks which are neither SMALLINT, nor BIGINT. That means that no number in the file is greater than 2³⁰ (30 bits) but there's at least one constraint with a sum of coefficients greater than 2²⁰ (20 bits). The expected answer is OPTIMUM FOUND or UNSAT (possibly SAT when a solver finds a model but cannot prove it is the optimum solution).
• Category "optimization, big integers" (OPTBIGINT)
  The benchmarks in this category contain an objective function which sould be minimized. The constraints may contain big integers, which mean that at least one number in the file is greater than 2³⁰ (30 bits). The expected answer is OPTIMUM FOUND or UNSAT (possibly SAT when a solver finds a model but cannot prove it is the optimum solution).

Not all solvers had support for each of these categories. Here are the capabilities for each solver:

A note about a few remaining bugs

As one can see, a few bugs still appeared in a few solvers. Here's what we know about these minor bugs.

On one single instance, solver Pueblo outputs a solution which did not satisfy all constraints. According to its author, that problem was caused by an objective function that contains terms with both positive and negative coefficients, which was not correctly handled by the solver. The problem has been fixed since then.

Because of a missing flush in its signal handler, minisat+ never outputs a complete solution on the "v " line and therefore, all its SAT answer are counted as NO CERTIFICATE.

On 3 instances classified as NO CERTIFICATE, solver sat4jPseudo required more than two seconds to output a solution when it received a SIGTERM and was therefore killed before it could provide a complete solution.

The wrong UNSAT answers of vallst_0.9.258 seem to be caused by an error in the script (a 'grepres' command is called but not found).

Category "no optimization function" (SAT)

Category "optimization, small integers" (OPTSMALLINT)

Category "optimization, medium integers" (OPTMEDINT)

Category "optimization, big integers" (OPTBIGINT)

All categories

Some explanations

• #Benchs: Number of benchs for this solver
• UNSAT.: solver proved unsatitisfiability ("s UNSATISFIABLE" was output)
• OPT.: solver found an optimum solution ("s OPTIMUM FOUND" was output), the provided implicant satisfies each constraint and no solver gave a better solution
• SAT.: solver found a solution ("s SATISFIABLE" was output) and the provided implicant satisfies each constraint
• SAT (timeout): solver exceeded the time limit but was able to find a solution ("s SATISFIABLE" was output) and the provided implicant satisfies each constraint
• SAT (out of mem.): solver exceeded the memory limit but was able to find a solution ("s SATISFIABLE" was output) and the provided implicant satisfies each constraint
• UNKNOWN: solver couldn't decide ("s UNKNOWN" was output)
• UNKNOWN (timeout): solver exceeded the time limit and gave no answer. These runs are considered to give result UNKNOWN
• UNKNOWN (out of mem.): solver exceeded the memory limit and gave no answer. These runs are considered to give result UNKNOWN.
• UNKNOWN (exit code): solver didn't output a solution line and terminated with an unexpected exit code (different of 0, 10, 20 and 30). These runs are considered to give result UNKNOWN.
• Sig. Caught: solver was terminated by a signal (SIGSEGV for example) and didn't output a solution line
• NO CERT.: solver answered SATISFIABLE but either didn't provide a certificate (the "v " line) or either gave a truncated certificate (which doesn't end in a new line)
• WRONG CERT.: solver gave an implicant but it appears that it doesn't satisfy every constraint
• WRONG OPT.: solver found an optimum solution ("s OPTIMUM FOUND" was output) but there exists an implicant which gives a better value to the objective function
• WRONG UNSAT.: solver proved unsatisfiability but was wrong ("s UNSATISFIABLE" was output)
• Misc: This is a internal check. It counts the runs that don't fall into one of the previous category. Should be 0 if categories are exhaustive and mutually exclusive. Will be negative if categories are not mutually exclusive and positive if categories are not exhaustive.