Skip to content

Fix MaxSATRegressionSuite failure #182

@msakai

Description

@msakai

From #177

MaxSATRegressionSuite result:

% ./testSolver.py --verbose "./toysat --maxsat-compact-v-line --exit-code --maxsat"
./testSolver.py 2024 by Tobias Paxian; run with --help for more information.
Checks a list of wcnfs (with the expected o-value) if the solver runs without errors.

STARTING IN MSE 2024 --> the solver must return one of the following exit codes:
	0 	if it cannot find a solution satisfying the hard clauses or prove unsatisfiability.
	10	if the solver finds a solution satisfying the hard clauses but does not prove it to be unsatisfiabe.
	20	if it finds that the hard clauses are unsatisfiable.
	30	if it finds an optimal solution.

Skipping files due to: upper_bound_violation: 30;

Start searching in 249 instances for issues.

COUNTER: [117/249], next: MSE22Unique/bccf74a9309e2c6c52091971a90e95f48575166cd915116a3c5ec83f5eb393e1.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 43 variables, 5 hard clauses and 257 soft clauses and file size 2550 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/bccf74a9309e2c6c52091971a90e95f48575166cd915116a3c5ec83f5eb393e1.wcnf


COUNTER: [131/249], next: MSE22Unique/51d10addb5086760fe1382e32684ac276e5016294c0091d9920dd5d2c3b9079f.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 178 variables, 406 hard clauses and 300 soft clauses and file size 11798 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/51d10addb5086760fe1382e32684ac276e5016294c0091d9920dd5d2c3b9079f.wcnf


COUNTER: [137/249], next: MSE22Unique/f3b8ed7dc683c85ef0b098fd5a476e86dab0db7f8e2982fd9c3819e2f8e090dc.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 54 variables, 8 hard clauses and 157 soft clauses and file size 1437 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/f3b8ed7dc683c85ef0b098fd5a476e86dab0db7f8e2982fd9c3819e2f8e090dc.wcnf


COUNTER: [184/249], next: MSE22Unique/faf04697cf8b5259f39428c3eb01cded33dee842e143e4460d74683ae22e4004.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 274 variables, 271 hard clauses and 298 soft clauses and file size 8587 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/faf04697cf8b5259f39428c3eb01cded33dee842e143e4460d74683ae22e4004.wcnf


COUNTER: [205/249], next: MSE22Unique/86db83ff8b25868a0f9a46aae8a042bc6fff64b2d543f920120e944835764f12.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 163 variables, 214 hard clauses and 199 soft clauses and file size 6505 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/86db83ff8b25868a0f9a46aae8a042bc6fff64b2d543f920120e944835764f12.wcnf


COUNTER: [230/249], next: MSE22Unique/9c10d3bbff2cba8d3ac57faadcd04214d6b62f9e0346f5db9f0874986808851b.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 411 variables, 4 hard clauses and 248 soft clauses and file size 4645 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/9c10d3bbff2cba8d3ac57faadcd04214d6b62f9e0346f5db9f0874986808851b.wcnf


COUNTER: [240/249], next: MSE22Unique/7a2faca44be5495873a9976f81fc4d8753ebc3645cde7643531861c27f682a63.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 69 variables, 97 hard clauses and 98 soft clauses and file size 2766 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/7a2faca44be5495873a9976f81fc4d8753ebc3645cde7643531861c27f682a63.wcnf


COUNTER: [242/249], next: MSE22Unique/63e94c74f5b6bed45fe01efb2e201086f28c4724cda1af45add73ace207f2542.wcnf        

	ISSUE DETECTED:
		Solver timeout after 50s. WCNF with 178 variables, 291 hard clauses and 166 soft clauses and file size 7889 Bytes.

	Solver call to reproduce error: 
		./toysat --maxsat-compact-v-line --exit-code --maxsat /Users/sakai/src/toysolver/MaxSATRegressionSuite/MSE22Unique/63e94c74f5b6bed45fe01efb2e201086f28c4724cda1af45add73ace207f2542.wcnf


Overall Evaluation:                                                                                             
	Found Issues in 8/249 instances:
		Solver timeout after 50s: 8

Total runtime of script: 462.25s

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions