AClib: Algorithm Configuration Library

Reference for scenario: @InProceedings{HutHooLey10-mipconfig, author = {F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Automated Configuration of Mixed Integer Programming Solvers}, booktitle = {Proc.~of CPAIOR-10} year = 2010, pages = {186--202} }

Reference for scenario: @InProceedings{HutHooLey10-mipconfig, author = {F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Automated Configuration of Mixed Integer Programming Solvers}, booktitle = {Proc.~of CPAIOR-10} year = 2010, pages = {186--202} }

Reference for scenario: @InProceedings{HutHooLey10-mipconfig, author = {F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Automated Configuration of Mixed Integer Programming Solvers}, booktitle = {Proc.~of CPAIOR-10} year = 2010, pages = {186--202} }

Reference for scenario: @InProceedings{HutHooLey10-mipconfig, author = {F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Automated Configuration of Mixed Integer Programming Solvers}, booktitle = {Proc.~of CPAIOR-10} year = 2010, pages = {186--202} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

This scenario originates in the Auto-WEKA paper: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Barman domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Blocksworld domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Depots domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Gripper domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on a merged set of all 9 domains from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Parking domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Rover domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Satellite domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the Spanner domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the Fast Downward planner to find an initial satisficing solution on the TPP domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Barman domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Blocksworld domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Depots domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Gripper domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on a merged set of all 9 domains from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Parking domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Rover domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Satellite domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the Spanner domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

Scenario optimizing the runtime for the LPG planner to find an initial satisficing solution on the TPP domain from IPC 2011.

Configurators are given a runtime cutoff of 5 CPU days, with a 900 CPU second runtime cutoff for each target algorithm run.

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2014: http://aclib.net/cssc2014/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

This scenarios originates from the Configurable SAT Solver Competition (CSSC) 2013: http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/

Trains the ctt timetabling solver on the instances of the ITC-2007 international timetabling competition, in which this solver placed third in the post-enrolment track.

We optimize for timetable quality, with 4 CPU days for configuration and a 300 second target algorithm runtime cutoff.

Trains the ctt timetabling solver on the instances of the ITC-2007 international timetabling competition, in which this solver placed third in the post-enrolment track.

We optimize for runtime to find a feasible solution (PAR-10), with 2 CPU days for configuration and a 300 second target algorithm runtime cutoff.

 
-----------------------------------------------------------------
         Multi-Objective Ant Colony Optimization Framework

                Manuel López-Ibáñez and Thomas Stützle
-----------------------------------------------------------------

This scenario requires the programs 'moaco_btsp' (from MOACO in
directory moaco_btsp/), 'nondominated' (from mo-tools/, used for
normalization), and hv (from hv/, for computing the hypervolume). All
of them are implemented in C and need to be compiled. In GNU/Linux and
other operating systems which support Makefiles, the required programs
can be compiled by simply typing 'make' to produce the executables.

Contents

    * Introduction
    * Usage
    * License
    * Download
    * Changelog


------------
Introduction
------------

  Multi-objective optimization problems are problems with several,
  typically conflicting criteria for evaluating solutions. Without any
  a priori preference information, the Pareto optimality principle
  establishes a partial order among solutions, and the output of the
  algorithm becomes a set of nondominated solutions rather than a
  single one.  Various ant colony optimization (ACO) algorithms have
  been proposed in recent years for solving such problems. These
  multi-objective ACO (MOACO) algorithms exhibit different design
  choices for dealing with the particularities of the multi-objective context.

  This program implements the multi-objective ant colony optimization
  (MOACO) framework. This framework is able to instantiate most MOACO
  algorithms from the literature, and also combine components that
  were never studied in the literature.

Relevant literature:

 [1] Manuel López-Ibáñez and Thomas Stützle. The Automatic Design of
     Multi-Objective Ant Colony Optimization Algorithms. IEEE
     Transactions on Evolutionary Computation, 16(6):861–875, 2012.
     doi: 10.1109/TEVC.2011.2182651

 [2] Manuel López-Ibáñez and T. Stützle. Automatic configuration of
     multi-objective ACO algorithms. In M. Dorigo et al., editors, Ant
     Colony Optimization and Swarm Intelligence, 7th International
     Conference, ANTS 2010, volume 6234 of Lecture Notes in Computer
     Science, pages 95–106. Springer, Heidelberg, Germany, 2010.

 [3] Manuel López-Ibáñez and T. Stützle. The impact of design choices
     of multi-objective ant colony optimization algorithms on
     performance: An experimental study on the biobjective TSP. In
     M. Pelikan and J. Branke, editors, Proceedings of the Genetic and
     Evolutionary Computation Conference, GECCO 2010, pages 71–78. ACM
     press, New York, NY, 2010.

 [4] Manuel López-Ibáñez and Thomas Stützle. An Analysis of
     Algorithmic Components for Multiobjective Ant Colony
     Optimization: A Case Study on the Biobjective TSP. In P. Collet
     et al., editors, Artificial Evolution, volume 5975 of Lecture
     Notes in Computer Science, pages 134-145. Springer, Heidelberg,
     Germany, 2010.


------------
Building
------------

The programming language is C, and the software has been tested on
GNU/Linux using GCC >= 4.1.

The unpacked sources contain the following directories: btsp, libmisc,
libpareto, and moaco. Change the current directory to moaco/trunk and
invoke make:

   $ tar xvf moaco-0.1.tar.gz
   $ cd moaco/trunk
   $ make

For extending the code to a new problem, create a new directory
beside btsp, e.g., myproblem, and then implement all functions called
by the moaco and prefixed by Sol. The code can be compiled for the new
problem as:

   $ cd moaco/trunk
   $ make clean
   $ make PROBLEM=myproblem


------------
Usage
------------

An example of invocation is:

   $ cd moaco/trunk
   $ ~/bin/moaco_btsp --input ../../btsp/kroAB100.tsp --time 100 --BicriterionAnt

Other options available are given by the output of the parameter --help.

The instance type handled by the btsp follows the format produced by
the DIMACS benchmark generator [*]. Bi-objective TSP instances can be
constructed by simply concatenating two single-objective instances
such as:

   $ cat euclidA100.tsp euclidB100.tsp > euclidAB100.tsp


[*] http://www2.research.att.com/~dsj/chtsp/download.html


------------
License
------------

This software is Copyright (C) 2010 - 2012
Manuel Lopez-Ibanez and Thomas Stuetzle.

This program is free software (software libre); you can redistribute
it and/or modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2 of the
License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
General Public License for more details.

The file LICENSE contains a copy of the GNU General Public License; if
not, you can obtain a copy of the GNU General Public License at
http://www.gnu.org/copyleft/gpl.html

This software includes code from various sources:

  * The GNU Scientific Library (GSL) is Copyright (C) The GSL Team,
    under the terms of the GPL.

  * moaco_spea2.c uses code from the PISA project Copyright (C) Swiss
    Federal Institute of Technology, Computer Engineering and Networks
    Laboratory, under the terms of the PISA license (PISA_LICENSE.txt).

IMPORTANT NOTE: Please be aware that the fact that this program is
released as Free Software does not excuse you from scientific
propriety, which obligates you to give appropriate credit! If you
write a scientific paper describing research that made substantive use
of this program, it is your obligation as a scientist to (a) mention
the fashion in which this software was used in the Methods section;
(b) mention the algorithm in the References section. The appropriate
citation is:

     Manuel López-Ibáñez and Thomas Stützle. The Automatic Design of
     Multi-Objective Ant Colony Optimization Algorithms. IEEE
     Transactions on Evolutionary Computation, 16(6):861–875, 2012.
     doi: 10.1109/TEVC.2011.2182651

Moreover, as a personal note, I would appreciate it if you would email
manuel.lopez-ibanez@ulb.ac.be with citations of papers referencing this
work so I can mention them to my funding agent and tenure committee.


------------
Download
------------

The latest version can be downloaded from:

    http://iridia.ulb.ac.be/~manuel/moaco


------------
Changelog
------------

Version 0.1

  * This version corresponds to the framework described in:

     Manuel López-Ibáñez and Thomas Stützle. The Automatic Design of
     Multi-Objective Ant Colony Optimization Algorithms. IEEE
     Transactions on Evolutionary Computation, 16(6):861–875, 2012.
     doi: 10.1109/TEVC.2011.2182651

  * moaco: Multi-objective ant colony optimization framework, implementing:
     +  MOAQ
     +  Pareto ACO (PACO)
     +  BicriterionAnt
     +  Multi-Objective Network ACO (MONACO)
     +  m-ACO variant 1 (mACO1)
     +  m-ACO variant 2 (mACO2)
     +  m-ACO variant 3 (mACO3)
     +  m-ACO variant 4 (mACO4)
     +  MACS
     +  COMPETants
  * btsp: Bi-objective travelling salesman problem.
  * libpareto: A small library to handle Pareto (nondominated) sets.
  * libmisc: A library with miscellaneous utilities.

Reference: @InProceedings{ThoHutHooLey13-AutoWEKA, author = {C. Thornton and F. Hutter and H.~H. Hoos and K. Leyton-Brown}, title = {Auto-{WEKA}: Combined Selection and Hyperparameter Optimization of Classification Algorithms}, booktitle = {Proc.~of KDD-2013}, year = 2013, pages = {847-855} }

                            clasp-2.x
          A conflict-driven nogood learning answer set solver 
                 http://www.cs.uni-potsdam.de/clasp/
                  http://potassco.sourceforge.net/

OVERVIEW clasp is an answer set solver for (extended) normal logic programs. It combines the high-level modeling capacities of answer set programming with state-of-the-art techniques from the area of Boolean constraint solving. The primary clasp algorithm relies on conflict-driven nogood learning, a technique that proved very successful for satisfiability checking (SAT). Starting with version 2.0, clasp supports parallel (multithreaded) solving.

clasp is written in (mostly) Standard-C++. It was successfully built and run under Linux (x86-32, x86-64) using gcc and Windows (x86-32, x86-64) using either Microsoft Visual Studio or MinGW.

Detailed information (including a User's manual), source code, and pre-compiled binaries are available at: http://potassco.sourceforge.net/

LICENSE clasp is part of the Potassco project hosted at SourceForge. It is distributed under the GNU Public Licens. See COPYING for details regarding the license.

PACKAGE CONTENTS COPYING - GNU Public License CHANGES - Major changes between versions README - This file configure.{sh,bat} - Simple script that creates Makefiles for building clasp (library and application) app/ - Source code directory of the command-line interface libclasp/ - Directory of the clasp (static) library (sources, documentation, unit tests) libprogram_opts/ - Library for parsing command-line options (needed by app) build_vc/ - Directory containing Visual Studio project files for building clasp tools/ - Some additional files

BUILDING & INSTALLING The preferred way to build clasp is to use make and the provided configure script. You'll need to have the GNU Compiler Collection (GCC) version 3 or better installed in order to build clasp. You'll also need GNU make 3.80 or better. On Microsoft Windows, we recommend using MinGW available from http://www.mingw.org/ You may want to visit http://www.mingw.org/wiki/Getting_Started for detailed instructions on installing MinGW. Make sure to also install MinGW-make.

In the following it is assumed that 'make' is an alias for the installed GNU make. If this is not the case on your system, replace 'make' with the name of the GNU make executable (e.g. gmake). Furthermore, on Microsoft Windows use ./configure.bat instead of ./configure.sh.

clasp's multithread support requires the Intel Threading Building Blocks library (version >= 3.x) which is freely available at: http://threadingbuildingblocks.org/ After downloading and installing you may want to set and export the TBB30_INSTALL_DIR environment variable.

Type ./configure.sh --help to get an overview of all supported build configurations/options.

To build clasp: ./configure.sh cd build/release make

To build clasp with multithread support using TBB30_INSTALL_DIR: ./configure.sh --with-mt cd build/release_mt make

To build clasp with multithread support using custom directory structure: ./configure.sh --with-mt TBB_INCLUDE= TBB_LIB= cd build/release_mt make

To install clasp: make install

By default, 'make install' will install clasp in '/usr/local/bin' You can specify an installation prefix other than '/usr/local' by running the configure-script with the option '--prefix=PATH'. Alternatively, use option '--bindir=PATH' to directly specify the installation path.

Finally, you can always skip installation and simply copy the clasp executable to a directory of your choice.

BUILDING WITH Microsoft Visual Studio In the directory build_vc/ we provide Microsoft Visual Studio project files for building clasp. You can download the freely available express edition of Visual C++ from here: http://www.microsoft.com/express/Downloads/ Once installed: - open build_vc\vc9\clasp\clasp.sln - select the desired solution configuration (typically release_static) - build the "app" project

USAGE clasp reads problem instances either from stdin, e.g cat problem | clasp or from a given file, e.g clasp problem

Beside logic programs in SMODELS-format, clasp also supports SAT-problems in DIMACS-, Max-SAT in (extended) DIMACS-, and PB-problems in OPB and WBO-format.

Type clasp --help to get an overview of the various options supported by clasp.

In addition to printing status information, clasp also provides information about the computation via its exit status. The exit status is: 10: if the problem was found to be satisfiable 20: if the problem was proved to be unsatisfiable 0 : if the satisfiability of problem is not known, because search was either interrupted or not started 127: if clasp ran out of memory Furthermore, the exit status of 1 indicates an error.

A static version of the Fast Downward planning system, as used in the IPC 2011 planning competition and subsequent work in automated configuration for planning.

Provided with permission of the authors, please do not redistribute.

Contact the Fast Downward authors at http://www.fast-downward.org for license details and to see newer versions of the software.

A static version of the LPG-td planning system, as used in the IPC 2011 planning competition and subsequent work in automated configuration for planning.

Provided with permission of the authors, please do not redistribute.

Contact the authors of LPG at http://zeus.ing.unibs.it/lpg/ for license details.

[This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Please contact the authors for an appropriate reference and licensing information. Please see below for the original README.]

Authors: Benjamin Kaufmann, Torsten Schaub, Marius Schneider

University of Potsdam

Contact: manju@cs.uni-potsdam.de

Content: . |-- callstring_generator.rb : original file from the minisat example |-- clasp : static linked binary of clasp 2.1.3 |-- clasp-2.1.3-src/ : sources of clasp 2.1.3 (see http://sourceforge.net/projects/potassco/files/clasp/2.1.3/) |-- clasp-2.1-sat-t1-discrete.txt : discrete configuration space of clasp 2.1 |-- clasp-2.1-sat-t1.txt : continuous configuration space of clasp 2.1 |-- clasp_parser.py : python script for reading the configuration from the file generated by callstring_generator.rb and printing the call string of clasp |-- parameter_parser.py : converts smac like paramters in clasp like parameters |-- README : this file

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Author: Mate Soos, soos.mate@gmail.com Please contact the author for an appropriate reference and licensing information.

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Author: Thach-Thao Duong, thachthaoduong@gmail.com Please contact the author for an appropriate reference and licensing information.

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Author: Thach-Thao Duong, thachthaoduong@gmail.com Please contact the author for an appropriate reference and licensing information.

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Authors: Thach-Thao Duong and Duc Nghia Pham. Contact: thachthaoduong@gmail.com Please contact the authors for an appropriate reference and licensing information.

[This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Author: Armin Biere, biere@jku.at Please contact the author for an appropriate reference. Please see below for the original README; the compilation README file also covers licensing questions.]

see lingeling-ars-df4d2c8-130529/README for compilation

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Author: Norbert Manthey, norbert.manthey@tu-dresden.de Please contact the author for an appropriate reference. Please see license.txt for licensing information.

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Author: Norbert Manthey, norbert.manthey@tu-dresden.de Please contact the author for an appropriate reference. Please see license.txt for licensing information.

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Authors: Daniel Le Berre and Stefanie Roussel. Contact: leberre@cril.fr Please contact the authors for an appropriate reference and licensing information.

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Authors: Cheng-Shen Han and Jie-Hong Roland Jiang. Contact: jhjiang@cc.ee.ntu.edu.tw Please contact the authors for an appropriate reference and licensing information.

This version is taken from the Configurable SAT Solver Competition (CSSC) 2013 (http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/). Authors: Valeriy Balabanov. Contact: balabasik@gmail.com Please contact the authors for an appropriate reference and licensing information.

Author: Domagoj Babic, babic.domagoj@gmail.com Please contact the author concerning licensing information.

Reference: @misc{BabHut07, author = {Domagoj Babi\'c and Frank Hutter}, title = {SPEAR Theorem Prover}, note = {Solver description, {SAT} competition}, year={2007} }

ctt timetabling solver for post-enrolment exam timetabling problems.

This code is the version used for the post-enrolment track of the ITC 2007 international timetabling competition, in which it placed third.

Code is made available with permission from the authors and should not be further distributed.

To compile: make all

To compile the checker: make checksln

To change command line parameters edit the file opag-input.cpp. Then run: make config this will create a new file called ComParser.cpp. Do not modify this file.

       AAAA    CCCC   OOOO   TTTTTT   SSSSS  PPPPP
      AA  AA  CC     OO  OO    TT    SS      PP  PP
      AAAAAA  CC     OO  OO    TT     SSSS   PPPPP
      AA  AA  CC     OO  OO    TT        SS  PP
      AA  AA   CCCC   OOOO     TT    SSSSS   PP

######################################################
##########    ACO algorithms for the TSP    ##########
######################################################

      Version: 1.03 + tuning.patch (see below)
      Author:  Thomas Stuetzle
      Copyright (c) Thomas Stuetzle, 2002


This is the README file to the software package ACOTSP.

This software package was developed by Thomas Stuetzle in connection
with the Book 

[DorStu04] Marco Dorigo and Thomas Stuetzle, "Ant Colony
Optimization", MIT Press, Cambridge, MA, USA, 2004.

The software package is freely available subject to the 
GNU General Public Licence, which is included in file gpl.txt.

If you use ACOTSP in your research, I would appreciate a citation in
your publication(s). Please cite it as

Thomas Stuetzle. ACOTSP, Version 1.0. Available from
http://www.aco-metaheuristic.org/aco-code, 2004.

This software package provides an implementation of various Ant Colony
Optimization (ACO) algorithms for the symmetric Traveling
Salesman Problem (TSP). The ACO algorithms implemented are Ant System,
Elitist Ant System, MAX-MIN Ant System, Rank-based version of Ant
System, Best-Worst Ant System, and Ant Colony System. This is Version
1.0 of ACOTSP; it is in large part identical to the software used to
produce the results in [DorStu04], but it has been slightly adapted to
make the code more readable, more comments were added, and a new
command line parser was generated with opag.

AIMS OF THE SOFTWARE: This software was developed to have one common
code for the various known ACO algorithms that were at some point
applied to the TSP in the literature. The software tries to provide a
reasonably efficient implementation of these ACO algorithms while at
the same time aiming for readability and understandability of the
code.



UPDATES for version 1.03: (Manuel Lopez-Ibanez, Thomas Stuetzle)

- parse.c, InOut.h: Increase filename length limit to 255. Add error
  if limit is passed.

- TSP.c: correction to the computation of the ceiling distances
  (thanks to Ashley Wang for reporting the error).

UPDATES for version 1.02: (Manuel Lopez-Ibanez)

- Avoid rounding issues that may rarely result in broken tours.
  (ants.c: neighbour_choose_and_move_to_next)

- The termination condition is now checked after every local search
  call. (acotsp.c: local_search)

- Avoid division by zero. (ants.c: bwas_pheromone_mutation)

- Defaults for all algorithms follow those given in the ACO book.

- The type of timer can be selected when building. Either
  'make TIMER=dos' or 'make TIMER=unix'.

- New command-line flags: --quiet and --seed

- Information about command-line options is printed to stdout. Only
  errors are printed in stderr.

- Fix various compiler warnings.


UPDATES for version 1.01:

- corrected a memory leak on 64 bit architectures (file ls.c, line 83,
  changed int to long int)

- corrected a problem in MMAS pheromone update (file acotsp.c, line 406, condition corrected to  
        if ( u_gb == 1 && (iteration - restart_found_best > 50))
    )

- corrected a problem in BWAS update (file acotsp.c, line 406, procedure call should read   
        bwas_worst_ant_update( &ant[iteration_worst_ant], best_so_far_ant );
    )   

- corrected a problem in option parsing (file parse.c, line 1032 should read    
        check_out_of_range( nn_ants, 1, 100, "nn_ants");
    )

Thanks to the various users who have reported these problems!


tuning.patch
=============

There are some changes in the ants.c and acotsp.c files. These changes
save the initial tour found:

 ants.c: In function nn_tour adding of the line:
    copy_from_to( &ant[0], best_so_far_ant);

 acotsp.c: In main after the call init_try(n_try);
           adding of write_report(); 

These changes were made due to a bug
(http://sourceware.org/bugzilla/show_bug.cgi?id=13932) in the libc
library, specifically in the pow function only for 64 bits
processors. This was making the execution of acotsp much slower and
not producing any solution before the termination criterion.

./acotsp --time 20 --tries 1 -i 1500-6.tsp --seed 545301 --acs --localsearch 3 --alpha 2.81 --beta 7.68 --rho 0.17 --ants 37 --nnls 9 --q0 0.59 --dlb 1


=========
CONTENTS
=========


The GNU General Public Licence:
gpl.txt

The main control routines, main:
acotsp.c

Procedures to implement the ants behaviour:
ants.c
ants.h

Input / output / statistics routines:
InOut.c
InOut.h

Procedures specific to the TSP:
TSP.c
TSP.h

Local search procedures:
ls.c
ls.h

Additional useful / helping procedure:
utilities.c
utilities.h

Command line parser:
parse.c
parse.h

Time measurement:
timer.h 
dos_timer.c  : default timer implementation based on clock()
unix_timer.c : in case you want to use rusage() instead, edit the
               Makefile to use this one or compile with 'make TIMER=unix'

Makefile

Instances: 
  Some problem instances from TSPLIB: eil51.tsp kroA100.tsp d198.tsp
  lin318.tsp pcb442.tsp att532.tsp rat783.tsp pcb1173.tsp d1291.tsp
  pr2392.tsp. Other TSP instances are available from TSPLIB, the
  webpage for the 8th DIMACS Implementation Challenge on the TSP
  (http://www.research.att.com/~dsj/chtsp/) or the webpage on "Solving
  TSP"


=====
Code
=====


The software was developed in ANSI C under Linux, using the GNU 2.95.3
gcc compiler and extensively tested in this environment. The software
is distributed as a gzipped tar file.

To install the code, first obtain the file ACOTSP.V1.0.tar.gz. Unzip
the file by typing

gunzip ACOTSP.V1.0.tar.gz

and then unpack it by typing 

tar -xvf ACOTSP.V1.0.tar

The software will unpack in a new folder ACOTSP.V1.0 

To compile it under Linux just type 'make' and the executable 'acotsp'
is produced.

Note: The code is written in ANSI C. Hence, the code should be
reasonable portable to other Operating Systems than Linux or Unix.


======
USAGE
======


Given the large number of ACO algorithms, also the number of command
line options is relatively large.

The default parameter settings are such, that MAX-MIN Ant System will
be run using a 3-opt local search, using alpha = 1, beta = 2, rho =
0.5 for a maximum of 10 seconds per each trial for 10 independent
trials. (guess who developed MAX-MIN Ant System ;-)

The executable 'acotsp' provides the following command line options
(given are the short and the long options):

-r, --tries          # number of independent trials
-s, --tours          # number of steps in each trial
-t, --time           # maximum time for each trial
    --seed           # seed for the random number generator 
-i, --tsplibfile     f inputfile (TSPLIB format necessary)
-o, --optimum        # stop if tour better or equal optimum is found
-m, --ants           # number of ants
-g, --nnants         # nearest neighbours in tour construction
-a, --alpha          # alpha (influence of pheromone trails)
-b, --beta           # beta (influence of heuristic information)
-e, --rho            # rho: pheromone trail evaporation
-q, --q0             # q_0: prob. of best choice in tour construction
-c, --elitistants    # number of elitist ants
-f, --rasranks       # number of ranks in rank-based Ant System
-k, --nnls           # No. of nearest neighbors for local search
-l, --localsearch    0: no local search   1: 2-opt   2: 2.5-opt   3: 3-opt
-d, --dlb            1 use don't look bits in local search
-u, --as               apply basic Ant System
-v, --eas              apply elitist Ant System
-w, --ras              apply rank-based version of Ant System
-x, --mmas             apply MAX-MIN ant system
-y, --bwas             apply best-worst ant system
-z, --acs              apply ant colony system
-h, --help             display the help text and exit

Options -u --as, -v --eas, -w --ras, -x --mmas, -y --bwas, -z --acs,
-h, --help don't need arguments, while all the others do.  

A Mandatory option is only the option "-i, --tsplibfile". Here, mandatory
means that without specifying this option, the program won't work,
since there is no input file. 

All the other options take some default values. The default values for
these are:

-r, --tries       : 10
-s, --tours       : 100
-t, --time        : 10 /* seconds */
-o, --optimum     : 1
-m, --ants        : 25
-g, --nnants      : 20
-a, --alpha       : 1
-b, --beta        : 2
-e, --rho         : 0.5
-q, --q0          : 0.0
-c, --elitistants : 100
-f, --rasranks    : 6
-k, --nnls        : 20
-l, --localsearch : 3 /* use 3-opt */
-d, --dlb         : 1 
-u, --as          : 0
-v, --eas         : 0
-w, --ras         : 0 
-x, --mmas        : 1 /* apply MAX-MIN Ant System */
-y, --bwas        : 0
-z, --acs         : 0


The default settings imply that as default MAX-MIN Ant System is run
using a 3-opt local search procedure. Please note that these default
values do not really make sense for some of the algorithms (e.g.,
typically an evaporation of 0.2 is recommended vor MAX-MIN Ant
System); that is, for some of the algorithms the default parameter
settings lead to poor performance (an example is ACS). Hence, when you
use any of the ACO algorithms, make sure you set the appropriate
parameter values. Typically, one may want to adjust the parameters

-t, --time
-o, --optimum
-m, --ants
-b, --beta
-e, --rho 
-q, --q0
-l, --localsearch

Note that only one option among -u --as, -v --eas, -w --ras,
-x --mmas, -y --bwas, -z --acs, is to be specified.

Examples for running an experiments are:

./acotsp -i lin318.tsp -v -t 60. -o 42029 -m 50 -b 5

or

./acotsp --tsplibfile lin318.tsp --acs --rho 0.1 --q0 0.95 --time 60. --optimum 42029 --ants 10


=======
OUTPUT
=======


Every experiment produces three files. These files are 

best.tsplibfilename
cmp.tsplibfilename
stat.tsplibfilename

where tsplibfilename is the instance identifier of the instance under
solution. 

The most important of these is the file "cmp.tsplibfilename". This
file starts with a specification of the parameter settings used to run
the experiment. The section with the comprehensive experimental data
starts with

begin problem tsplibfilename

Next the random number seed for the next trial is given

Then, for each trial statistical information on the development of the
best-so-far solution is given. Each section for a trial starts with

begin try 

Then, each time the algorithm finds a new best solution a line 

best     iteration   tours   time 

is added, where "best" is the tour length of the best-so-far solution;
iteration is the iteration number in which this solution is found;
tours is the number of solutions constructed so far (typically this is
simple iteration X n_ants); and time is the time at which a new
best-so-far solution is found

Each trial is ended by 

end try 

Once all trials are run the line 

end problem tsplibfilename

is added to end the file. 

The file  best.tsplibfilename

collects the information about parameter settings, the best solution
found in each trial, and some additional statistical information.

The file stat.tsplibfilename 

may be used for the output of statistical information on a trial as
generated by the procedure population_statistics(); in InOut.c;
however, it is not heavily used in ACOTSP V1.0. 

Have fun, and if you have any comments please write to 

stuetzle no@spam ulb.ac.be

 This scenario requires the programs 'acotsp' (from ACOTSP-VAR in
directory src/), 'nondominated' (from mo-tools/, used for
normalization), and hv (from hv/, for computing the hypervolume). All
of them are implemented in C and need to be compiled. In GNU/Linux and
other operating systems which support Makefiles, the required programs
can be compiled by simply typing 'make' to produce the executables.

ACOTSP-VAR is a modified version of the ACOTSP software with additional
parameters controlling parameter variation. Further information about
this variant can be found in the paper:

  M. López-Ibáñez and T. Stützle. Automatically improving the anytime
  behaviour of optimisation algorithms. European Journal of
  Operational Research, 2013. doi:10.1016/j.ejor.2013.10.043.

This modified version is
Copyright (c) 2013 Manuel Lopez-Ibanez 

This program is free software (software libre); you can redistribute
it and/or modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2 of the
License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.

IMPORTANT NOTE: Please be aware that the fact that this program is
released as Free Software does not excuse you from scientific
propriety, which obligates you to give appropriate credit! If you
write a scientific paper describing research that made substantive use
of this program, it is your obligation as a scientist to (a) mention
the fashion in which this software was used in the Methods section;
(b) mention the algorithm in the References section. The appropriate
citation is given above.

The original ACOTSP is Copyright (c) Thomas Stuetzle, 2002.
The README and license information of the original ACOTSP can be found
in src/README

The instances ricochet are Copyright (C) 2013 Potassco torsten@cs.uni-potsdam.de. The instances are lincensed under GPLv2.

Distributed by AClib with prior consent from the Author.

Literature (not exactly the same instances as used below; but generated with the advanced encoding on the same board)

@InProceedings{gejokaobsascsc13a, author = "M. Gebser and H. Jost and R. Kaminski and P. Obermeier and O. Sabuncu and T. Schaub and M. Schneider", title = "Ricochet Robots: A transverse {ASP} benchmark", crossref = "lpnmr13", pages = "348-360" } @Proceedings{lpnmr13, title = "Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13)", booktitle = "Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13)", year = 2013, editor = "P. Cabalar and T. Son", volume = 8148, series = "Lecture Notes in Artificial Intelligence", publisher = "Springer-Verlag" }

@InProceedings{schanda_et_al:LIPIcs:2012:3611, author = {Florian Schanda and Martin Brain}, title = {{Using Answer Set Programming in the Development of Verified Software}}, booktitle = {Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)}, pages = {72--85}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-43-9}, ISSN = {1868-8969}, year = {2012}, volume = {17}, editor = {Agostino Dovier and V{\'i}tor Santos Costa}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3611}, URN = {urn:nbn:de:0030-drops-36114}, doi = {http://dx.doi.org/10.4230/LIPIcs.ICLP.2012.72}, annote = {Keywords: Answer Set Programming, verification, SPARK, Ada, contract based verification, safety critical} }

@inproceedings{DBLP:conf/padl/LierlerSTW12, author = {Yuliya Lierler and Shaden Smith and Miroslaw Truszczynski and Alex Westlund}, title = {Weighted-Sequence Problem: ASP vs CASP and Declarative vs Problem-Oriented Solving}, booktitle = {PADL}, year = {2012}, pages = {63-77}, ee = {http://dx.doi.org/10.1007/978-3-642-27694-1_6}, crossref = {DBLP:conf/padl/2012}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/padl/2012, editor = {Claudio V. Russo and Neng-Fa Zhou}, title = {Practical Aspects of Declarative Languages - 14th International Symposium, PADL 2012, Philadelphia, PA, USA, January 23-24, 2012. Proceedings}, booktitle = {PADL}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7149}, year = {2012}, isbn = {978-3-642-27693-4}, ee = {http://dx.doi.org/10.1007/978-3-642-27694-1}, bibsource = {DBLP, http://dblp.uni-trier.de} }

Bi-objective travelling salesman problem (BTSP) instances.
There are Random Uniform Euclidean with sizes between 100 and 1000
cities.
These instances are for all purposes in the public domain.

These instances are provided by the Berkeley Computational Optimization Lab (under http://ieor.berkeley.edu/~atamturk/data/capacitated.lotsizing/cls.data.tar.gz). Please cite them as follows:

@ARTICLE{AM:ls-poly, AUTHOR = {A. Atamt{\"u}rk and J. C. Mu{\~n}oz}, TITLE = {A Study of the Lot-Sizing Polytope}, JOURNAL = {Mathematical Programming}, VOLUME = {99}, PAGES = {443-465}, YEAR = {2004}}

These instances were generated and provided by Bistra Dilkina, using the generator from:

@inproceedings{ghs08:connection, author={Gomes, Carla P. and {van Hoeve}, Willem-Jan and Sabharwal, Ashish}, title={Connections in networks: a hybrid approach}, booktitle=cpaior08, month=may, year=2008, address={Paris, France}, series=lncs, volume=5015, pages={303-307}, publisher = springer-lncs, editor = {L. Perron and M.~A. Trick} }

These instances were generated and provided by Lin Xu, using the generator from:

@INPROCEEDINGS{rcw, author = {Ahmadizadeh, K. and Dilkina, B. and Gomes, C.P. and Sabharwal, A.}, title = {An empirical study of optimization for maximizing diffusion in networks}, booktitle = cp10, pages = {514--521}, year = 2010, series = {LNCS}, volume = {6308}, publisher = {Springer-Verlag} }

These instances were generated by Lin Xu, using the generator from:

@InProceedings{LeyPeaSho00, author = "K. Leyton-Brown and M. Pearson and Y. Shoham", title = "Towards a Universal Test Suite for Combinatorial Auction Algorithms", booktitle = {EC '00: Proceedings of the 2nd ACM conference on Electronic commerce}, pages = "66--76", year={2000}, publisher = {ACM}, address = {New York, NY, USA}, }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset has been proposed by: @article{krizhevsky2009learning, title={Learning multiple layers of features from tiny images}, author={Krizhevsky, Alex and Hinton, Geoffrey}, journal={Master's thesis, Department of Computer Science, University of Toronto}, year={2009} }

This dataset has been proposed by: @article{krizhevsky2009learning, title={Learning multiple layers of features from tiny images}, author={Krizhevsky, Alex and Hinton, Geoffrey}, journal={Master's thesis, Department of Computer Science, University of Toronto}, year={2009} }

This dataset is taken from: @article{bergstra2012random, title={Random search for hyper-parameter optimization}, author={Bergstra, J. and Bengio, Y.}, journal=jmlr, volume={13}, pages={281--305}, year={2012} }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset originates from the KDD cup 2009.

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is taken from: @incollection{LeCunEtAl12, author = {Yann LeCun and L{\'e}on Bottou and Genevieve B. Orr and Klaus-Robert M{\"u}ller}, title = {Efficient BackProp}, booktitle = {Neural Networks: Tricks of the Trade (2nd ed.)}, year = {2012}, pages = {9-48} }

This dataset is taken from: @incollection{LeCunEtAl12, author = {Yann LeCun and L{\'e}on Bottou and Genevieve B. Orr and Klaus-Robert M{\"u}ller}, title = {Efficient BackProp}, booktitle = {Neural Networks: Tricks of the Trade (2nd ed.)}, year = {2012}, pages = {9-48} }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This dataset is part of the UCI machine learning repository: @misc{Asuncion+Newman:2007 , author = "A. Asuncion, D.J. Newman", year = "2007", title = "{UCI} Machine Learning Repository", url = "http://www.ics.uci.edu/$\sim$mlearn/{MLR}epository.html", institution = "University of California, Irvine, School of Information and Computer Sciences" }

This is a set of instances from the Barman planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Barman planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the Blocksworld planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Blocksworld planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the Depots planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Depots planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the Gripper planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Gripper planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from all domains of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from all domains of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the Parking planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Parking planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the Rover planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Rover planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the Satellite planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Satellite planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the Spanner planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the Spanner planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This is a set of instances from the TPP planning domain of the IPC-2011 learning track.

The training set was generated specifically for the FD-autotune submission, while the test set is that used in the competition.

This is a set of instances from the TPP planning domain of the IPC-2011 learning track.

The training set was generated specifically for the ParLPG submission, while the test set is that used in the competition.

This instance set was introduced in the following paper:

@inproceedings{CaptainJack, lauthor = {Tompkins, Dave A. D. and Balint, Adrian and Hoos, Holger H.}, author = {Tompkins, D. A. D. and Balint, A. and Hoos, H. H.}, title = {Captain {Jack}: new variable selection heuristics in local search for {SAT}}, booktitle = {Proc.~of SAT-11}, lseries = {SAT'11}, year = {2011}, lisbn = {978-3-642-21580-3}, llocation = {Ann Arbor, MI}, pages = {302--316}, lnumpages = {15}, lurl = {http://dl.acm.org/citation.cfm?id=2023474.2023506}, lacmid = {2023506}, lpublisher = {Springer-Verlag}, laddress = {Berlin, Heidelberg}, }

This benchmark set consists of CNFs that Sam Bayless derived by unrolling the Hardware Model Checking Competition 2008 (HWMCC 2008) circuits into CNF, using the tool 'aigunroll'.

HWMCC 2008 can be cited as follows: A. Biere. Hardware Model Checking Competition 2008. http://fmv.jku.at/hwmcc/

This benchmark set is a subset of the BMC08 instances used in the Configurable SAT Solver Challenge 2013 (CSSC 2013); instances generated from 60 Intel instances with unclear licensing restrictrions are omitted. If you have access to the full instance set, the original BMC08 training/test split is given in data/BMC08.

These were created using Armin Biere's cnf fuzzer fuzzsat, which generated circuits and translates them into CNFs. We generated many circuits (using the options -i 100 -I 100) and then filtered out all that could be solved by lingeling in < 1 second (on one particular desktop computer).

These are easy regression test instances provided by Sam Bayless for the Configurable SAT Solver Competition (CSSC 2013). They are useful for testing wrappers etc. Note that, since these are not instances for a real configuration scenario, the test set is superfluous. To be syntactically correct, it is chosen as identical to the training set.

These instances are described on page 117 of Balint, A, Belov, A, Heule, M J H & Jaervisalo, M (eds), 2013, Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2013-1, vol. B-2013-1, University of Helsinki, Helsinki.

This is a set of uniform random 3-SAT instances of various sizes that was used for the Configurable SAT Solver Competition (CSSC 2013).

These instances are described on page 115 of Balint, A, Belov, A, Heule, M J H & Jaervisalo, M (eds), 2013, Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2013-1, vol. B-2013-1, University of Helsinki, Helsinki.

This benchmark set consists of 604 SAT-encoded software verification instances generated with the Calysto tool from Domagoj Babic, split into 302 training and 302 test instances. It can be cited as:

@inproceedings{babic07structural-abs, author = {Domagoj Babi\'c and Alan J. Hu}, title = {{Structural Abstraction of Software Verification Conditions}}, booktitle = {Computer Aided Verification: 19th International Conference, CAV 2007}, publisher = {Springer}, series = {LNCS}, volume = {4590}, year = {2007}, pages={366--378}, location = {Berlin, Germany} }

The set was first used for algorithm configuration in: @inproceedings{HutBabHooHu07, author = {F. Hutter and D. Babi\'c and H.~H.~Hoos and A.~J.~Hu}, title = {{Boosting verification by automatic tuning of decision procedures}}, year = {2007}, booktitle = fmcad07, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, editor = {J. Baumgartner and M. Sheeran}, pages = {27--34} }

This is a set of satisfiable uniform random 3-SAT instances at the phase transition with 250 variables that was included in the CSSC distribution as a simple benchmark set to enable a quick configuration run for testing purposes.

These instance were generated with the generator at: http://sourceforge.net/projects/ksatgenerator/, described on page 72 of: Balint, A, Belov, A, Heule, M J H & Jaervisalo, M (eds), 2012, Proceedings of SAT Competition 2012: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2012-2, vol. B-2012-2, University of Helsinki, Helsinki.

Travelling salesman problem (TSP) instances.
There are Random Uniform Euclidean with sizes between 1000 and 3000
cities.
These instances are for all purposes in the public domain.

Travelling salesman problem (TSP) instances.
There are Random Uniform Euclidean with size 3000.
These instances are for all purposes in the public domain.