PB'05 evaluation: solvers page

Category "no optimization function" (SAT)

Category "optimization, small integers" (OPTSMALLINT)

Category "optimization, medium integers" (OPTMEDINT)

Category "optimization, big integers" (OPTBIGINT)

All categories

Some explanations

• #Runs: Number of runs for this solver
• OPT.: solver found an optimum solution (exit code=30 and "s OPTIMUM FOUND" was output) and the provided implicant satisfies each constraint
• WRONG OPT.: solver found an optimum solution (exit code=30 and "s OPTIMUM FOUND" was output) but there exists an implicant which gives a better value to the objective function
• SAT.: solver found a solution (exit code=10 and "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
• UNSAT.: solver proved unsatitisfiability (exit code=20 and "s UNSATISFIABLE" was output)
• WRONG UNSAT.: solver proved unsatitisfiability but was wrong (exit code=20 and "s UNSATISFIABLE" was output)
• UNKNOWN: solver couldn't decide (exit code=0 and "s UNKNOWN" was output)
• Unexp. Exit Code: unexpected exit code (different of 0, 10, 20 and 30) or exit code of 0 without a "s UNKNOWN" line. These runs are considered to give result UNKNOWN
• Timeout (no sol.): solver exceeded the time limit and gave no answer
• Sig. Caught: solver was terminated by a signal (SIGSEGV for example)
• Mismatch: the exit code given doesn't correspond to the solution line
• Verif. failed: solver gave an implicant but it appears that it doesn't satisfy every constraint
• 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.