View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
3    *
4    * All rights reserved. This program and the accompanying materials
5    * are made available under the terms of the Eclipse Public License v1.0
6    * which accompanies this distribution, and is available at
7    *  http://www.eclipse.org/legal/epl-v10.html
8    *
9    * Alternatively, the contents of this file may be used under the terms of
10   * either the GNU Lesser General Public License Version 2.1 or later (the
11   * "LGPL"), in which case the provisions of the LGPL are applicable instead
12   * of those above. If you wish to allow use of your version of this file only
13   * under the terms of the LGPL, and not to allow others to use your version of
14   * this file under the terms of the EPL, indicate your decision by deleting
15   * the provisions above and replace them with the notice and other provisions
16   * required by the LGPL. If you do not delete the provisions above, a recipient
17   * may use your version of this file under the terms of the EPL or the LGPL.
18   *
19   * Based on the original MiniSat specification from:
20   *
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   *
27   * Contributors:
28   *   CRIL - initial API and implementation
29   *******************************************************************************/
30  package org.sat4j.sat;
31  
32  import java.awt.BorderLayout;
33  import java.awt.Dimension;
34  import java.awt.FlowLayout;
35  import java.awt.GridBagConstraints;
36  import java.awt.GridBagLayout;
37  import java.awt.event.ActionEvent;
38  import java.awt.event.ActionListener;
39  import java.io.File;
40  import java.io.FileNotFoundException;
41  import java.io.FileOutputStream;
42  import java.io.IOException;
43  import java.io.PrintStream;
44  import java.io.PrintWriter;
45  import java.io.StringWriter;
46  import java.util.ArrayList;
47  import java.util.Collections;
48  import java.util.List;
49  
50  import javax.swing.BoxLayout;
51  import javax.swing.ButtonGroup;
52  import javax.swing.DefaultComboBoxModel;
53  import javax.swing.JButton;
54  import javax.swing.JCheckBox;
55  import javax.swing.JComboBox;
56  import javax.swing.JFileChooser;
57  import javax.swing.JLabel;
58  import javax.swing.JPanel;
59  import javax.swing.JRadioButton;
60  import javax.swing.JScrollPane;
61  import javax.swing.JTabbedPane;
62  import javax.swing.JTextArea;
63  import javax.swing.JTextField;
64  import javax.swing.border.CompoundBorder;
65  import javax.swing.border.EmptyBorder;
66  import javax.swing.border.TitledBorder;
67  
68  import org.sat4j.core.ASolverFactory;
69  import org.sat4j.maxsat.WeightedMaxSatDecorator;
70  import org.sat4j.maxsat.reader.MSInstanceReader;
71  import org.sat4j.minisat.core.ICDCL;
72  import org.sat4j.minisat.core.IOrder;
73  import org.sat4j.minisat.core.IPhaseSelectionStrategy;
74  import org.sat4j.minisat.core.LearnedConstraintsEvaluationType;
75  import org.sat4j.minisat.core.RestartStrategy;
76  import org.sat4j.minisat.core.SearchParams;
77  import org.sat4j.minisat.core.SimplificationType;
78  import org.sat4j.minisat.core.SolverStats;
79  import org.sat4j.minisat.orders.RandomWalkDecorator;
80  import org.sat4j.minisat.orders.VarOrderHeap;
81  import org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator;
82  import org.sat4j.pb.IPBSolver;
83  import org.sat4j.pb.OptToPBSATAdapter;
84  import org.sat4j.pb.PseudoOptDecorator;
85  import org.sat4j.pb.orders.RandomWalkDecoratorObjective;
86  import org.sat4j.pb.orders.VarOrderHeapObjective;
87  import org.sat4j.pb.reader.PBInstanceReader;
88  import org.sat4j.pb.tools.ClausalConstraintsDecorator;
89  import org.sat4j.reader.InstanceReader;
90  import org.sat4j.reader.ParseFormatException;
91  import org.sat4j.reader.Reader;
92  import org.sat4j.sat.visu.ChartBasedVisualizationTool;
93  import org.sat4j.sat.visu.GnuplotBasedSolverVisualisation;
94  import org.sat4j.sat.visu.JChartBasedSolverVisualisation;
95  import org.sat4j.sat.visu.SolverVisualisation;
96  import org.sat4j.sat.visu.TraceComposite;
97  import org.sat4j.sat.visu.VisuPreferences;
98  import org.sat4j.specs.ContradictionException;
99  import org.sat4j.specs.IConstr;
100 import org.sat4j.specs.ILogAble;
101 import org.sat4j.specs.IOptimizationProblem;
102 import org.sat4j.specs.IProblem;
103 import org.sat4j.specs.ISolver;
104 import org.sat4j.specs.ISolverService;
105 import org.sat4j.specs.Lbool;
106 import org.sat4j.specs.RandomAccessModel;
107 import org.sat4j.specs.SearchListener;
108 import org.sat4j.specs.TimeoutException;
109 import org.sat4j.tools.ClausalCardinalitiesDecorator;
110 import org.sat4j.tools.ConflictDepthTracing;
111 import org.sat4j.tools.ConflictLevelTracing;
112 import org.sat4j.tools.DecisionTracing;
113 import org.sat4j.tools.FileBasedVisualizationTool;
114 import org.sat4j.tools.HeuristicsTracing;
115 import org.sat4j.tools.LearnedClausesSizeTracing;
116 import org.sat4j.tools.LearnedTracing;
117 import org.sat4j.tools.MultiTracing;
118 import org.sat4j.tools.SpeedTracing;
119 import org.sat4j.tools.encoding.EncodingStrategy;
120 import org.sat4j.tools.encoding.Policy;
121 
122 /**
123  * 
124  * This panel contains buttons that control restart and clean on solver. It also
125  * displays history of commands.
126  * 
127  * @author sroussel
128  * 
129  */
130 public class DetailedCommandPanel extends JPanel implements SolverController,
131         SearchListener<ISolverService>, ILogAble {
132 
133     private static final String EXACTLY_1 = "Exactly 1:";
134     private static final String EXACTLY_K = "Exactly K:";
135     private static final String AT_MOST_1 = "At Most 1:";
136     private static final String AT_MOST_K = "At Most K:";
137 
138     private Policy encodingPolicy;
139 
140     private static final long serialVersionUID = 1L;
141 
142     public static final EmptyBorder BORDER5 = new EmptyBorder(5, 5, 5, 5);
143 
144     private String ramdisk;
145 
146     private RemoteControlStrategy telecomStrategy;
147     private RandomWalkDecorator randomWalk;
148     private ISolver solver;
149     private Reader reader;
150     private IProblem problem;
151     private ProblemType problemType;
152     private boolean optimizationMode;
153     private boolean equivalenceMode;
154     private boolean lowerMode;
155 
156     private String[] commandLines;
157 
158     private boolean firstStart;
159 
160     private StartSolverEnum startConfig;
161 
162     private StringWriter stringWriter;
163 
164     private JPanel aboutSolverPanel;
165     private JTextArea textArea;
166 
167     private JPanel instancePanel;
168     private static final String INSTANCE_PANEL = "Instance";
169     private JLabel instanceLabel;
170     private static final String INSTANCE = "Path to instance: ";
171     private JTextField instancePathField;
172     private String instancePath;
173     private JButton browseButton;
174     private static final String BROWSE = "Browse";
175 
176     private String whereToWriteFiles;
177 
178     private static final String MINISAT_PREFIX = "minisat";
179     private static final String PB_PREFIX = "pb";
180     private static final String MAXSAT_PREFIX = "maxsat";
181     private JPanel choixSolverPanel;
182     private static final String CHOIX_SOLVER_PANEL = "Solver";
183     private JLabel choixSolver;
184     private static final String CHOIX_SOLVER = "Choose solver: ";
185     private JComboBox listeSolvers;
186 
187     private static final String OPTMIZATION_MODE = "Optimization problem";
188     private JCheckBox optimisationModeCB;
189 
190     private static final String EQUIVALENCE = "Use equivalence instead of implication";
191     private JCheckBox equivalenceCB;
192 
193     private static final String LOWER = "Search solution by lower bounding instead of upper bounding";
194     private JCheckBox lowerCB;
195 
196     private JComboBox atMostKCB;
197     private JComboBox atMost1CB;
198     private JComboBox exactlyKCB;
199     private JComboBox exactly1CB;
200 
201     private JRadioButton solverLineParamLineRadio;
202     private JRadioButton solverLineParamRemoteRadio;
203     private JRadioButton solverListParamListRadio;
204     private JRadioButton solverListParamRemoteRadio;
205 
206     private static final String SOLVER_LINE_PARAM_LINE_CONFIG = "Start customized solver as given in command line";
207     private static final String SOLVER_LINE_PARAM_REMOTE_CONFIG = "Start customized solver as given in command line with configuration given in the remote";
208     private static final String SOLVER_LIST_PARAM_LIST_CONFIG = "Start solver as chosen in list with its default configuration";
209     private static final String SOLVER_LIST_PARAM_REMOTE_CONFIG = "Start solver as chosen in list with configuration given in the remote";
210 
211     private static final String CHOOSE_START_CONFIG = "Choose start configuration : ";
212 
213     private JButton startStopButton;
214     private static final String START = "Start";
215     private static final String STOP = "Stop";
216 
217     private JButton pauseButton;
218     private static final String PAUSE = "Pause";
219     private static final String RESUME = "Resume";
220 
221     private static final String RESTART_PANEL = "Restart strategy";
222     private RestartCommandComponent restartPanel;
223 
224     private static final String RW_PANEL = "Random Walk";
225     private RandomWalkCommandComponent rwPanel;
226 
227     private static final String CLEAN_PANEL = "Learned Constraint Deletion Strategy";
228     private CleanCommandComponent cleanPanel;
229 
230     private PhaseCommandComponent phasePanel;
231     private static final String PHASE_PANEL = "Phase Strategy";
232 
233     private SimplifierCommandComponent simplifierPanel;
234     private static final String SIMPLIFIER_PANEL = "Simplification strategy";
235 
236     private HotSolverCommandComponent hotSolverPanel;
237     private static final String HOT_SOLVER_PANEL = "Hot solver";
238 
239     private JTextArea console;
240 
241     private boolean isPlotActivated;
242 
243     private SolverVisualisation solverVisu;
244     private VisuPreferences visuPreferences;
245 
246     private boolean gnuplotBased = false;
247     private boolean chartBased = false;
248 
249     private RemoteControlFrame frame;
250 
251     public DetailedCommandPanel(String filename, RemoteControlFrame frame) {
252         this(filename, "", frame);
253     }
254 
255     public DetailedCommandPanel(String filename, String ramdisk,
256             RemoteControlFrame frame) {
257 
258         this(filename, ramdisk, new String[0], frame);
259     }
260 
261     public DetailedCommandPanel(String filename, String ramdisk, String[] args,
262             RemoteControlFrame frame) {
263         super();
264 
265         this.encodingPolicy = new Policy();
266 
267         this.frame = frame;
268 
269         this.visuPreferences = new VisuPreferences();
270 
271         this.telecomStrategy = new RemoteControlStrategy(this);
272         this.instancePath = filename;
273         this.ramdisk = ramdisk;
274 
275         this.console = new JTextArea();
276 
277         this.commandLines = args.clone();
278         if (args.length > 0) {
279             this.solver = Solvers.configureSolver(args, this);
280             this.optimizationMode = Solvers.containsOptValue(args);
281         }
282 
283         this.equivalenceMode = false;
284         this.lowerMode = false;
285 
286         this.isPlotActivated = false;
287 
288         if (this.solver != null) {
289             this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_LINE;
290         } else {
291             this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
292         }
293 
294         this.firstStart = true;
295 
296         this.setPreferredSize(new Dimension(800, 800));
297         this.setLayout(new BoxLayout(this, BoxLayout.Y_AXIS));
298 
299         createInstancePanel();
300         createChoixSolverPanel();
301 
302         this.restartPanel = new RestartCommandComponent(RESTART_PANEL, this,
303                 this.telecomStrategy.getRestartStrategy().getClass()
304                         .getSimpleName(), this);
305         this.rwPanel = new RandomWalkCommandComponent(RW_PANEL, this);
306         this.cleanPanel = new CleanCommandComponent(CLEAN_PANEL, this);
307         this.phasePanel = new PhaseCommandComponent(PHASE_PANEL, this,
308                 this.telecomStrategy.getPhaseSelectionStrategy().getClass()
309                         .getSimpleName());
310         this.simplifierPanel = new SimplifierCommandComponent(SIMPLIFIER_PANEL,
311                 this);
312         this.hotSolverPanel = new HotSolverCommandComponent(HOT_SOLVER_PANEL,
313                 this);
314 
315         JScrollPane scrollPane = new JScrollPane(this.console);
316 
317         scrollPane.setPreferredSize(new Dimension(400, 200));
318         scrollPane.getVerticalScrollBar().setValue(
319                 scrollPane.getVerticalScrollBar().getMaximum());
320 
321         MyTabbedPane tabbedPane = new MyTabbedPane();
322 
323         JPanel solverBigPanel = new JPanel();
324         solverBigPanel
325                 .setLayout(new BoxLayout(solverBigPanel, BoxLayout.Y_AXIS));
326         solverBigPanel.add(this.instancePanel);
327         solverBigPanel.add(this.choixSolverPanel);
328 
329         tabbedPane.addTab("Solver", null, solverBigPanel,
330                 "instance & solver options");
331 
332         JPanel restartBigPanel = new JPanel();
333         restartBigPanel.setLayout(new GridBagLayout());
334 
335         GridBagConstraints cRestart = new GridBagConstraints();
336         cRestart.anchor = GridBagConstraints.PAGE_START;
337         cRestart.fill = GridBagConstraints.HORIZONTAL;
338         cRestart.weightx = 1;
339         cRestart.weighty = 1;
340 
341         restartBigPanel.add(this.restartPanel, cRestart);
342 
343         tabbedPane.addTab("Restart", null, restartBigPanel,
344                 "restart strategy & options");
345 
346         JPanel rwPhaseBigPanel = new JPanel();
347         rwPhaseBigPanel.setLayout(new GridBagLayout());
348 
349         GridBagConstraints cP = new GridBagConstraints();
350         cP.anchor = GridBagConstraints.PAGE_START;
351         cP.fill = GridBagConstraints.HORIZONTAL;
352         cP.weightx = 1;
353         cP.weighty = 1;
354 
355         JPanel tmpPhasePanel = new JPanel();
356         tmpPhasePanel.setLayout(new GridBagLayout());
357         GridBagConstraints cPhase = new GridBagConstraints();
358         cPhase.fill = GridBagConstraints.HORIZONTAL;
359         cPhase.weightx = 1;
360         cPhase.weighty = .2;
361 
362         tmpPhasePanel.add(this.rwPanel, cPhase);
363 
364         cPhase.gridy = 1;
365         cPhase.weighty = .2;
366         tmpPhasePanel.add(this.phasePanel, cPhase);
367 
368         cPhase.gridy = 2;
369         tmpPhasePanel.add(this.hotSolverPanel, cPhase);
370 
371         rwPhaseBigPanel.add(tmpPhasePanel, cP);
372 
373         tabbedPane.addTab("Heuristics", null, rwPhaseBigPanel,
374                 "random walk and phase strategy");
375 
376         JPanel clausesBigPanel = new JPanel();
377         clausesBigPanel.setLayout(new GridBagLayout());
378 
379         GridBagConstraints cC = new GridBagConstraints();
380         cC.anchor = GridBagConstraints.PAGE_START;
381         cC.fill = GridBagConstraints.HORIZONTAL;
382         cC.weightx = 1;
383         cC.weighty = 1;
384 
385         JPanel tmpClausesPanel = new JPanel();
386         tmpClausesPanel.setLayout(new GridBagLayout());
387         GridBagConstraints cClauses = new GridBagConstraints();
388         cClauses.fill = GridBagConstraints.HORIZONTAL;
389         cClauses.weightx = 1;
390         cClauses.weighty = .2;
391 
392         tmpClausesPanel.add(this.cleanPanel, cClauses);
393 
394         cClauses.gridy = 1;
395         tmpClausesPanel.add(this.simplifierPanel, cClauses);
396 
397         clausesBigPanel.add(tmpClausesPanel, cC);
398 
399         tabbedPane.addTab("Learned Constraints", null, clausesBigPanel,
400                 "deletion and simplification strategy");
401 
402         this.aboutSolverPanel = new JPanel();
403         this.textArea = new JTextArea("No solver is running at the moment");
404         this.textArea.setColumns(50);
405         this.aboutSolverPanel.add(this.textArea);
406 
407         tabbedPane.addTab("About Solver", null, this.aboutSolverPanel,
408                 "information about solver");
409 
410         this.add(tabbedPane);
411         this.add(scrollPane);
412 
413         this.restartPanel.setRestartPanelEnabled(false);
414         this.rwPanel.setRWPanelEnabled(false);
415         this.cleanPanel.setCleanPanelEnabled(false);
416         this.phasePanel.setPhasePanelEnabled(false);
417         this.simplifierPanel.setSimplifierPanelEnabled(false);
418         this.hotSolverPanel.setKeepSolverHotPanelEnabled(false);
419 
420         this.solverVisu = new JChartBasedSolverVisualisation(
421                 this.visuPreferences);
422 
423         updateWriter();
424     }
425 
426     private void createInstancePanel() {
427         this.instancePanel = new JPanel();
428 
429         this.instancePanel.setName(INSTANCE_PANEL);
430         this.instancePanel.setBorder(new CompoundBorder(new TitledBorder(null,
431                 this.instancePanel.getName(), TitledBorder.LEFT,
432                 TitledBorder.TOP), BORDER5));
433 
434         this.instancePanel.setLayout(new BorderLayout(0, 0));
435 
436         this.instanceLabel = new JLabel(INSTANCE);
437         this.instancePathField = new JTextField(20);
438         this.instancePathField.setText(this.instancePath);
439 
440         this.instanceLabel.setLabelFor(this.instancePathField);
441 
442         this.browseButton = new JButton(BROWSE);
443 
444         this.browseButton.addActionListener(new ActionListener() {
445             public void actionPerformed(ActionEvent e) {
446                 openFileChooser();
447                 updateListOfSolvers();
448             }
449         });
450 
451         this.optimisationModeCB = new JCheckBox(OPTMIZATION_MODE);
452         this.optimisationModeCB.setSelected(this.optimizationMode);
453 
454         this.equivalenceCB = new JCheckBox(EQUIVALENCE);
455         this.equivalenceCB.setSelected(this.equivalenceMode);
456 
457         this.lowerCB = new JCheckBox(LOWER);
458         this.lowerCB.setSelected(this.lowerMode);
459 
460         JPanel tmpPanel11 = new JPanel();
461         tmpPanel11.add(this.instanceLabel);
462         tmpPanel11.add(this.instancePathField);
463         tmpPanel11.add(this.browseButton);
464 
465         JPanel tmpPanel12 = new JPanel();
466         tmpPanel12.setLayout(new BoxLayout(tmpPanel12, BoxLayout.Y_AXIS));
467         tmpPanel12.add(this.optimisationModeCB);
468         tmpPanel12.add(this.equivalenceCB);
469         tmpPanel12.add(this.lowerCB);
470 
471         this.optimisationModeCB.addActionListener(new ActionListener() {
472             public void actionPerformed(ActionEvent e) {
473                 setOptimisationMode(optimisationModeCB.isSelected());
474                 log("use optimization mode: "
475                         + DetailedCommandPanel.this.optimizationMode);
476                 updateListOfSolvers();
477             }
478         });
479 
480         this.equivalenceCB.addActionListener(new ActionListener() {
481             public void actionPerformed(ActionEvent e) {
482                 equivalenceMode = equivalenceCB.isSelected();
483             }
484         });
485 
486         this.lowerCB.addActionListener(new ActionListener() {
487             public void actionPerformed(ActionEvent e) {
488                 lowerMode = lowerCB.isSelected();
489             }
490         });
491 
492         instancePanel.setLayout(new BoxLayout(instancePanel, BoxLayout.Y_AXIS));
493 
494         instancePanel.add(tmpPanel11);
495         instancePanel.add(tmpPanel12);
496     }
497 
498     private void createChoixSolverPanel() {
499         this.choixSolverPanel = new JPanel();
500 
501         this.choixSolverPanel.setName(CHOIX_SOLVER_PANEL);
502         this.choixSolverPanel.setBorder(new CompoundBorder(new TitledBorder(
503                 null, this.choixSolverPanel.getName(), TitledBorder.LEFT,
504                 TitledBorder.TOP), BORDER5));
505 
506         this.choixSolverPanel.setLayout(new BoxLayout(choixSolverPanel,
507                 BoxLayout.Y_AXIS));
508 
509         this.choixSolver = new JLabel(CHOIX_SOLVER);
510 
511         this.listeSolvers = new JComboBox();
512 
513         updateListOfSolvers();
514 
515         JPanel tmpPanel1 = new JPanel();
516         tmpPanel1.add(this.choixSolver);
517         tmpPanel1.add(this.listeSolvers);
518 
519         this.startStopButton = new JButton(START);
520 
521         this.startStopButton.addActionListener(new ActionListener() {
522             public void actionPerformed(ActionEvent e) {
523                 manageStartStopButton();
524             }
525         });
526 
527         this.pauseButton = new JButton(PAUSE);
528         this.pauseButton.setEnabled(false);
529 
530         this.pauseButton.addActionListener(new ActionListener() {
531             public void actionPerformed(ActionEvent e) {
532                 if (DetailedCommandPanel.this.pauseButton.getText().equals(
533                         PAUSE)) {
534                     DetailedCommandPanel.this.pauseButton.setText(RESUME);
535                     DetailedCommandPanel.this.telecomStrategy
536                             .setInterrupted(true);
537                 } else {
538                     DetailedCommandPanel.this.pauseButton.setText(PAUSE);
539                     DetailedCommandPanel.this.telecomStrategy
540                             .setInterrupted(false);
541                 }
542 
543             }
544         });
545 
546         JPanel tmpPanel = new JPanel();
547         tmpPanel.setLayout(new GridBagLayout());
548 
549         GridBagConstraints c = new GridBagConstraints();
550 
551         tmpPanel.setName("Cardinality Constraints Encodings");
552         tmpPanel.setBorder(new CompoundBorder(new TitledBorder(null, tmpPanel
553                 .getName(), TitledBorder.LEFT, TitledBorder.TOP), BORDER5));
554 
555         JLabel atMostKLabel = new JLabel(AT_MOST_K);
556         atMostKCB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
557                 AT_MOST_K).toArray()));
558 
559         JLabel atMost1Label = new JLabel(AT_MOST_1);
560         atMost1CB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
561                 AT_MOST_1).toArray()));
562 
563         JLabel exactlyKLabel = new JLabel(EXACTLY_K);
564         exactlyKCB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
565                 EXACTLY_K).toArray()));
566 
567         JLabel exactly1Label = new JLabel(EXACTLY_1);
568         exactly1CB = new JComboBox(new DefaultComboBoxModel(getListOfEncodings(
569                 EXACTLY_1).toArray()));
570 
571         c.fill = GridBagConstraints.NONE;
572         c.weightx = 0.2;
573         c.gridx = 0;
574         c.gridy = 0;
575         c.anchor = GridBagConstraints.LINE_END;
576 
577         tmpPanel.add(atMostKLabel, c);
578 
579         c.gridx = 0;
580         c.gridy = 1;
581         tmpPanel.add(atMost1Label, c);
582 
583         c.gridx = 2;
584         c.gridy = 1;
585         tmpPanel.add(exactly1Label, c);
586 
587         c.gridx = 2;
588         c.gridy = 0;
589         tmpPanel.add(exactlyKLabel, c);
590 
591         c.fill = GridBagConstraints.HORIZONTAL;
592         c.anchor = GridBagConstraints.LINE_START;
593         c.weightx = 0.8;
594         c.gridx = 1;
595         c.gridy = 0;
596         tmpPanel.add(atMostKCB, c);
597 
598         c.gridx = 3;
599         c.gridy = 0;
600         tmpPanel.add(exactlyKCB, c);
601 
602         c.gridx = 1;
603         c.gridy = 1;
604         tmpPanel.add(atMost1CB, c);
605 
606         c.gridx = 3;
607         c.gridy = 1;
608         tmpPanel.add(exactly1CB, c);
609 
610         JPanel tmpPanel2 = new JPanel();
611         tmpPanel2.setLayout(new GridBagLayout());
612 
613         GridBagConstraints c2 = new GridBagConstraints();
614         c2.anchor = GridBagConstraints.LINE_START;
615         c2.fill = GridBagConstraints.NONE;
616         c2.weightx = 1;
617         c2.gridx = 0;
618 
619         tmpPanel2.setName(CHOOSE_START_CONFIG);
620         tmpPanel2.setBorder(new CompoundBorder(new TitledBorder(null, tmpPanel2
621                 .getName(), TitledBorder.LEFT, TitledBorder.TOP), BORDER5));
622 
623         this.solverLineParamLineRadio = new JRadioButton(
624                 SOLVER_LINE_PARAM_LINE_CONFIG);
625         this.solverLineParamRemoteRadio = new JRadioButton(
626                 SOLVER_LINE_PARAM_REMOTE_CONFIG);
627         this.solverListParamRemoteRadio = new JRadioButton(
628                 SOLVER_LIST_PARAM_REMOTE_CONFIG);
629         this.solverListParamListRadio = new JRadioButton(
630                 SOLVER_LIST_PARAM_LIST_CONFIG);
631 
632         ButtonGroup solverConfigGroup = new ButtonGroup();
633         solverConfigGroup.add(this.solverLineParamLineRadio);
634         solverConfigGroup.add(this.solverLineParamRemoteRadio);
635         solverConfigGroup.add(this.solverListParamListRadio);
636         solverConfigGroup.add(this.solverListParamRemoteRadio);
637 
638         this.solverListParamListRadio.setSelected(true);
639         this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
640 
641         c2.gridy = 0;
642         tmpPanel2.add(this.solverLineParamLineRadio, c2);
643         c2.gridy = 1;
644         tmpPanel2.add(this.solverLineParamRemoteRadio, c2);
645         c2.gridy = 2;
646         tmpPanel2.add(this.solverListParamListRadio, c2);
647         c2.gridy = 3;
648         tmpPanel2.add(this.solverListParamRemoteRadio, c2);
649 
650         JPanel tmpPanel3 = new JPanel();
651         tmpPanel3.setLayout(new FlowLayout());
652         tmpPanel3.add(this.startStopButton);
653         tmpPanel3.add(this.pauseButton);
654 
655         this.choixSolverPanel.add(tmpPanel1);
656         this.choixSolverPanel.add(tmpPanel);
657         this.choixSolverPanel.add(tmpPanel2);
658         this.choixSolverPanel.add(tmpPanel3);
659 
660         atMostKCB.addActionListener(new ActionListener() {
661             public void actionPerformed(ActionEvent e) {
662                 encodingPolicy.setAtMostKEncoding((EncodingStrategy) atMostKCB
663                         .getSelectedItem());
664             }
665         });
666 
667         atMost1CB.addActionListener(new ActionListener() {
668             public void actionPerformed(ActionEvent e) {
669                 encodingPolicy
670                         .setAtMostOneEncoding((EncodingStrategy) atMost1CB
671                                 .getSelectedItem());
672             }
673         });
674 
675         exactlyKCB.addActionListener(new ActionListener() {
676             public void actionPerformed(ActionEvent e) {
677                 encodingPolicy
678                         .setExactlyKEncoding((EncodingStrategy) exactlyKCB
679                                 .getSelectedItem());
680             }
681         });
682 
683         exactly1CB.addActionListener(new ActionListener() {
684             public void actionPerformed(ActionEvent e) {
685                 encodingPolicy
686                         .setExactlyOneEncoding((EncodingStrategy) exactly1CB
687                                 .getSelectedItem());
688             }
689         });
690 
691         this.solverLineParamLineRadio.addActionListener(new ActionListener() {
692             public void actionPerformed(ActionEvent e) {
693                 if (DetailedCommandPanel.this.solverLineParamLineRadio
694                         .isSelected()) {
695                     DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_LINE;
696                 }
697             }
698         });
699 
700         this.solverLineParamRemoteRadio.addActionListener(new ActionListener() {
701             public void actionPerformed(ActionEvent e) {
702                 if (DetailedCommandPanel.this.solverLineParamRemoteRadio
703                         .isSelected()) {
704                     DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_REMOTE;
705                 }
706             }
707         });
708 
709         this.solverListParamListRadio.addActionListener(new ActionListener() {
710             public void actionPerformed(ActionEvent e) {
711                 if (DetailedCommandPanel.this.solverListParamListRadio
712                         .isSelected()) {
713                     DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
714                 }
715             }
716         });
717 
718         this.solverListParamRemoteRadio.addActionListener(new ActionListener() {
719             public void actionPerformed(ActionEvent e) {
720                 if (DetailedCommandPanel.this.solverListParamRemoteRadio
721                         .isSelected()) {
722                     DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_REMOTE;
723                 }
724             }
725         });
726 
727         setChoixSolverPanelEnabled(true);
728 
729         if (this.solver == null) {
730             this.solverLineParamLineRadio.setEnabled(false);
731             this.solverLineParamRemoteRadio.setEnabled(false);
732         }
733 
734         if (this.firstStart) {
735             this.solverLineParamRemoteRadio.setEnabled(false);
736             this.solverListParamRemoteRadio.setEnabled(false);
737         }
738 
739     }
740 
741     public void manageStartStopButton() {
742         if (DetailedCommandPanel.this.startStopButton.getText().equals(START)) {
743             launchSolverWithConfigs();
744             DetailedCommandPanel.this.pauseButton.setEnabled(true);
745             setInstancePanelEnabled(false);
746             DetailedCommandPanel.this.restartPanel.setRestartPanelEnabled(true);
747             DetailedCommandPanel.this.rwPanel.setRWPanelEnabled(true);
748             DetailedCommandPanel.this.cleanPanel.setCleanPanelEnabled(true);
749             DetailedCommandPanel.this.cleanPanel
750                     .setCleanPanelOriginalStrategyEnabled(true);
751             DetailedCommandPanel.this.phasePanel.setPhasePanelEnabled(true);
752             setChoixSolverPanelEnabled(false);
753             DetailedCommandPanel.this.simplifierPanel
754                     .setSimplifierPanelEnabled(true);
755             DetailedCommandPanel.this.hotSolverPanel
756                     .setKeepSolverHotPanelEnabled(true);
757             DetailedCommandPanel.this.startStopButton.setText(STOP);
758             solverListParamListRadio.setSelected(true);
759             startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
760             getThis().paintAll(getThis().getGraphics());
761             DetailedCommandPanel.this.frame
762                     .setActivateTracingEditableUnderCondition(false);
763             frame.setActivateRadioTracing(false);
764         } else {
765 
766             ((ISolver) DetailedCommandPanel.this.problem).expireTimeout();
767             DetailedCommandPanel.this.pauseButton.setEnabled(false);
768             log("Asked the solver to stop");
769             setInstancePanelEnabled(true);
770             setChoixSolverPanelEnabled(true);
771             DetailedCommandPanel.this.startStopButton.setText(START);
772             getThis().paintAll(getThis().getGraphics());
773             DetailedCommandPanel.this.frame.setActivateTracingEditable(true);
774             frame.setActivateRadioTracing(true);
775         }
776     }
777 
778     public String getStartStopText() {
779         return this.startStopButton.getText();
780     }
781 
782     public void setOptimisationMode(boolean optimizationMode) {
783         this.optimizationMode = optimizationMode;
784         this.optimisationModeCB.setSelected(optimizationMode);
785     }
786 
787     public void launchSolverWithConfigs() {
788         ICDCL<?> cdclSolver;
789         ASolverFactory<?> factory;
790         String[] partsSelectedSolver;
791         IOrder order;
792         double proba;
793 
794         String selectedSolver;
795 
796         switch (startConfig) {
797         case SOLVER_LIST_PARAM_REMOTE:
798             selectedSolver = (String) this.listeSolvers.getSelectedItem();
799             partsSelectedSolver = selectedSolver.split("\\.");
800 
801             assert partsSelectedSolver.length == 2;
802             assert partsSelectedSolver[0].equals(MINISAT_PREFIX)
803                     || partsSelectedSolver[0].equals(PB_PREFIX)
804                     || partsSelectedSolver[0].equals(MAXSAT_PREFIX);
805 
806             if (partsSelectedSolver[0].equals(MINISAT_PREFIX)) {
807                 factory = org.sat4j.minisat.SolverFactory.instance();
808             } else if (partsSelectedSolver[0].equals(PB_PREFIX)) {
809                 factory = org.sat4j.pb.SolverFactory.instance();
810             } else {
811                 factory = org.sat4j.maxsat.SolverFactory.instance();
812             }
813             this.solver = (ICDCL<?>) factory
814                     .createSolverByName(partsSelectedSolver[1]);
815 
816             cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
817 
818             this.telecomStrategy.setSolver(cdclSolver);
819 
820             cdclSolver.setRestartStrategy(this.telecomStrategy);
821             cdclSolver.setOrder(this.randomWalk);
822             cdclSolver.getOrder().setPhaseSelectionStrategy(
823                     this.telecomStrategy);
824 
825             this.restartPanel.hasClickedOnRestart();
826             this.rwPanel.hasClickedOnApplyRW();
827             this.phasePanel.hasClickedOnApplyPhase();
828             this.simplifierPanel.hasClickedOnApplySimplification();
829             break;
830 
831         case SOLVER_LINE_PARAM_LINE:
832             this.solver = Solvers.configureSolver(this.commandLines, this);
833 
834             cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
835 
836             this.telecomStrategy.setSolver(cdclSolver);
837             this.telecomStrategy.setRestartStrategy(cdclSolver
838                     .getRestartStrategy());
839             cdclSolver.setRestartStrategy(this.telecomStrategy);
840 
841             this.restartPanel.setCurrentRestart(this.telecomStrategy
842                     .getRestartStrategy().getClass().getSimpleName());
843 
844             order = cdclSolver.getOrder();
845 
846             proba = 0;
847 
848             if (this.optimizationMode) {
849                 if (order instanceof RandomWalkDecoratorObjective) {
850                     this.randomWalk = (RandomWalkDecorator) order;
851                     proba = this.randomWalk.getProbability();
852                 } else if (order instanceof VarOrderHeapObjective) {
853                     this.randomWalk = new RandomWalkDecoratorObjective(
854                             (VarOrderHeapObjective) order, 0);
855                 }
856             } else if (cdclSolver.getOrder() instanceof RandomWalkDecorator) {
857                 this.randomWalk = (RandomWalkDecorator) order;
858                 proba = this.randomWalk.getProbability();
859             } else {
860                 this.randomWalk = new RandomWalkDecorator((VarOrderHeap) order,
861                         0);
862             }
863 
864             this.randomWalk.setProbability(proba);
865             this.rwPanel.setProba(proba);
866             cdclSolver.setOrder(this.randomWalk);
867             this.telecomStrategy.setPhaseSelectionStrategy(cdclSolver
868                     .getOrder().getPhaseSelectionStrategy());
869             cdclSolver.getOrder().setPhaseSelectionStrategy(
870                     this.telecomStrategy);
871             this.phasePanel.setPhaseListSelectedItem(this.telecomStrategy
872                     .getPhaseSelectionStrategy().getClass().getSimpleName());
873             this.simplifierPanel.setSelectedSimplification(cdclSolver
874                     .getSimplifier().toString());
875 
876             this.phasePanel.repaint();
877             break;
878 
879         case SOLVER_LINE_PARAM_REMOTE:
880             this.solver = Solvers.configureSolver(this.commandLines, this);
881 
882             cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
883 
884             cdclSolver.setRestartStrategy(this.telecomStrategy);
885             cdclSolver.setOrder(this.randomWalk);
886             cdclSolver.getOrder().setPhaseSelectionStrategy(
887                     this.telecomStrategy);
888 
889             this.restartPanel.hasClickedOnRestart();
890             this.rwPanel.hasClickedOnApplyRW();
891             this.phasePanel.hasClickedOnApplyPhase();
892             this.simplifierPanel.hasClickedOnApplySimplification();
893             break;
894 
895         default:
896             selectedSolver = (String) this.listeSolvers.getSelectedItem();
897             partsSelectedSolver = selectedSolver.split("\\.");
898 
899             assert partsSelectedSolver.length == 2;
900             assert partsSelectedSolver[0].equals(MINISAT_PREFIX)
901                     || partsSelectedSolver[0].equals(PB_PREFIX)
902                     || partsSelectedSolver[0].equals(MAXSAT_PREFIX);
903 
904             if (partsSelectedSolver[0].equals(MINISAT_PREFIX)) {
905                 factory = org.sat4j.minisat.SolverFactory.instance();
906             } else if (partsSelectedSolver[0].equals(PB_PREFIX)) {
907                 factory = org.sat4j.pb.SolverFactory.instance();
908             } else {
909                 factory = org.sat4j.maxsat.SolverFactory.instance();
910             }
911 
912             this.solver = factory.createSolverByName(partsSelectedSolver[1]);
913 
914             cdclSolver = (ICDCL<?>) this.solver.getSolvingEngine();
915 
916             this.telecomStrategy.setSolver(cdclSolver);
917             this.telecomStrategy.setRestartStrategy(cdclSolver
918                     .getRestartStrategy());
919             cdclSolver.setRestartStrategy(this.telecomStrategy);
920 
921             this.restartPanel.setCurrentRestart(this.telecomStrategy
922                     .getRestartStrategy().getClass().getSimpleName());
923 
924             order = cdclSolver.getOrder();
925 
926             proba = 0;
927 
928             if (this.optimizationMode) {
929                 if (order instanceof RandomWalkDecoratorObjective) {
930                     this.randomWalk = (RandomWalkDecorator) order;
931                     proba = this.randomWalk.getProbability();
932                 } else if (order instanceof VarOrderHeapObjective) {
933                     this.randomWalk = new RandomWalkDecoratorObjective(
934                             (VarOrderHeapObjective) order, 0);
935                 }
936             } else if (cdclSolver.getOrder() instanceof RandomWalkDecorator) {
937                 this.randomWalk = (RandomWalkDecorator) order;
938                 proba = this.randomWalk.getProbability();
939             } else {
940                 this.randomWalk = new RandomWalkDecorator((VarOrderHeap) order,
941                         0);
942             }
943 
944             this.randomWalk.setProbability(proba);
945             this.rwPanel.setProba(proba);
946 
947             cdclSolver.setOrder(this.randomWalk);
948 
949             this.telecomStrategy.setPhaseSelectionStrategy(cdclSolver
950                     .getOrder().getPhaseSelectionStrategy());
951             this.phasePanel.setPhaseListSelectedItem(this.telecomStrategy
952                     .getPhaseSelectionStrategy().getClass().getSimpleName());
953             cdclSolver.getOrder().setPhaseSelectionStrategy(
954                     this.telecomStrategy);
955             this.simplifierPanel.setSelectedSimplification(cdclSolver
956                     .getSimplifier().toString());
957             break;
958         }
959 
960         this.whereToWriteFiles = this.instancePath;
961 
962         if (this.ramdisk.length() > 0) {
963             String[] instancePathSplit = this.instancePath.split("/");
964             this.whereToWriteFiles = this.ramdisk + "/"
965                     + instancePathSplit[instancePathSplit.length - 1];
966         }
967 
968         this.solver.setVerbose(true);
969         initSearchListeners();
970         cdclSolver.setLogger(this);
971 
972         try {
973             switch (problemType) {
974             case PB_OPT:
975                 this.solver = new ClausalConstraintsDecorator(
976                         (IPBSolver) this.solver, this.encodingPolicy);
977                 if (lowerMode) {
978                     this.solver = new ConstraintRelaxingPseudoOptDecorator(
979                             (IPBSolver) solver);
980                 } else {
981                     this.solver = new PseudoOptDecorator((IPBSolver) solver);
982                 }
983 
984                 this.reader = createReader(this.solver, this.instancePath);
985                 this.problem = this.reader.parseInstance(this.instancePath);
986                 this.problem = new OptToPBSATAdapter(
987                         (IOptimizationProblem) this.problem);
988                 break;
989             case CNF_MAXSAT:
990             case WCNF_MAXSAT:
991                 this.solver = new ClausalConstraintsDecorator(
992                         (IPBSolver) this.solver, this.encodingPolicy);
993                 this.solver = new WeightedMaxSatDecorator(
994                         (IPBSolver) this.solver, equivalenceMode);
995 
996                 this.reader = createReader(this.solver, this.instancePath);
997                 this.problem = this.reader.parseInstance(this.instancePath);
998 
999                 if (lowerMode) {
1000                     this.problem = new ConstraintRelaxingPseudoOptDecorator(
1001                             (WeightedMaxSatDecorator) this.problem);
1002                 } else {
1003                     this.problem = new PseudoOptDecorator(
1004                             (WeightedMaxSatDecorator) this.problem, false,
1005                             !equivalenceMode);
1006                 }
1007 
1008                 this.problem = new OptToPBSATAdapter(
1009                         (IOptimizationProblem) this.problem);
1010                 break;
1011             case PB_SAT:
1012                 this.solver = new ClausalConstraintsDecorator(
1013                         (IPBSolver) this.solver, this.encodingPolicy);
1014                 this.reader = createReader(this.solver, this.instancePath);
1015                 this.problem = this.reader.parseInstance(this.instancePath);
1016                 break;
1017             case CNF_SAT:
1018             default:
1019                 this.solver = new ClausalCardinalitiesDecorator<ISolver>(
1020                         this.solver, this.encodingPolicy);
1021                 this.reader = createReader(this.solver, this.instancePath);
1022                 this.problem = this.reader.parseInstance(this.instancePath);
1023                 break;
1024             }
1025 
1026         } catch (FileNotFoundException e) {
1027             log(e.getMessage());
1028         } catch (ParseFormatException e) {
1029             log(e.getMessage());
1030         } catch (IOException e) {
1031             log(e.getMessage());
1032         } catch (ContradictionException e) {
1033             log("Unsatisfiable (trivial)!");
1034             return;
1035         }
1036 
1037         log("# Started solver "
1038                 + this.solver.getSolvingEngine().getClass().getSimpleName());
1039         log("# on instance " + this.instancePath);
1040         log("# Optimisation = " + this.optimizationMode);
1041         log("# Restart strategy = "
1042                 + this.telecomStrategy.getRestartStrategy().getClass()
1043                         .getSimpleName());
1044         log("# Random walk probability = " + this.randomWalk.getProbability());
1045         log("# variables : " + this.solver.nVars());
1046 
1047         Thread solveurThread = new Thread() {
1048             @Override
1049             public void run() {
1050 
1051                 try {
1052                     DetailedCommandPanel.this.stringWriter = new StringWriter();
1053                     if (DetailedCommandPanel.this.problem.isSatisfiable()) {
1054                         log("Satisfiable !");
1055 
1056                         if (DetailedCommandPanel.this.problem instanceof OptToPBSATAdapter) {
1057                             log(((OptToPBSATAdapter) DetailedCommandPanel.this.problem)
1058                                     .getCurrentObjectiveValue() + "");
1059                             DetailedCommandPanel.this.reader
1060                                     .decode(((OptToPBSATAdapter) DetailedCommandPanel.this.problem)
1061                                             .model(new PrintWriter(
1062                                                     DetailedCommandPanel.this.stringWriter)),
1063                                             new PrintWriter(
1064                                                     DetailedCommandPanel.this.stringWriter));
1065                         } else {
1066                             DetailedCommandPanel.this.reader
1067                                     .decode(DetailedCommandPanel.this.problem
1068                                             .model(),
1069                                             new PrintWriter(
1070                                                     DetailedCommandPanel.this.stringWriter));
1071                         }
1072                         log(DetailedCommandPanel.this.stringWriter.toString());
1073                     } else {
1074                         log("Unsatisfiable !");
1075                     }
1076                 } catch (TimeoutException e) {
1077                     log("Timeout, sorry!");
1078                 }
1079             }
1080         };
1081         solveurThread.start();
1082 
1083         if (this.isPlotActivated) {
1084             this.solverVisu.setnVar(this.solver.nVars());
1085             startVisu();
1086         }
1087     }
1088 
1089     public void initSearchListeners() {
1090         List<SearchListener<ISolverService>> listeners = new ArrayList<SearchListener<ISolverService>>();
1091 
1092         if (this.isPlotActivated) {
1093             if (this.gnuplotBased) {
1094                 this.solverVisu = new GnuplotBasedSolverVisualisation(
1095                         this.visuPreferences, this.solver.nVars(),
1096                         this.instancePath, this);
1097                 if (this.visuPreferences.isDisplayClausesEvaluation()) {
1098                     listeners.add(new LearnedTracing(
1099                             new FileBasedVisualizationTool(
1100                                     this.whereToWriteFiles + "-learned")));
1101                 }
1102                 if (this.visuPreferences.isDisplayClausesSize()) {
1103                     listeners.add(new LearnedClausesSizeTracing(
1104                             new FileBasedVisualizationTool(
1105                                     this.whereToWriteFiles
1106                                             + "-learned-clauses-size"),
1107                             new FileBasedVisualizationTool(
1108                                     this.whereToWriteFiles
1109                                             + "-learned-clauses-size-restart"),
1110                             new FileBasedVisualizationTool(
1111                                     this.whereToWriteFiles
1112                                             + "-learned-clauses-size-clean")));
1113                 }
1114                 if (this.visuPreferences.isDisplayConflictsDecision()) {
1115                     listeners
1116                             .add(new ConflictLevelTracing(
1117                                     new FileBasedVisualizationTool(
1118                                             this.whereToWriteFiles
1119                                                     + "-conflict-level"),
1120                                     new FileBasedVisualizationTool(
1121                                             this.whereToWriteFiles
1122                                                     + "-conflict-level-restart"),
1123                                     new FileBasedVisualizationTool(
1124                                             this.whereToWriteFiles
1125                                                     + "-conflict-level-clean")));
1126                 }
1127                 if (this.visuPreferences.isDisplayConflictsTrail()) {
1128                     listeners
1129                             .add(new ConflictDepthTracing(
1130                                     new FileBasedVisualizationTool(
1131                                             this.whereToWriteFiles
1132                                                     + "-conflict-depth"),
1133                                     new FileBasedVisualizationTool(
1134                                             this.whereToWriteFiles
1135                                                     + "-conflict-depth-restart"),
1136                                     new FileBasedVisualizationTool(
1137                                             this.whereToWriteFiles
1138                                                     + "-conflict-depth-clean")));
1139                 }
1140 
1141                 if (this.visuPreferences.isDisplayDecisionIndexes()) {
1142                     listeners.add(new DecisionTracing(
1143                             new FileBasedVisualizationTool(
1144                                     this.whereToWriteFiles
1145                                             + "-decision-indexes-pos"),
1146                             new FileBasedVisualizationTool(
1147                                     this.whereToWriteFiles
1148                                             + "-decision-indexes-neg"),
1149                             new FileBasedVisualizationTool(
1150                                     this.whereToWriteFiles
1151                                             + "-decision-indexes-restart"),
1152                             new FileBasedVisualizationTool(
1153                                     this.whereToWriteFiles
1154                                             + "-decision-indexes-clean")));
1155                 }
1156 
1157                 if (this.visuPreferences.isDisplaySpeed()) {
1158                     listeners
1159                             .add(new SpeedTracing(
1160                                     new FileBasedVisualizationTool(
1161                                             this.whereToWriteFiles + "-speed"),
1162                                     new FileBasedVisualizationTool(
1163                                             this.whereToWriteFiles
1164                                                     + "-speed-clean"),
1165                                     new FileBasedVisualizationTool(
1166                                             this.whereToWriteFiles
1167                                                     + "-speed-restart")));
1168                 }
1169                 if (this.visuPreferences.isDisplayVariablesEvaluation()) {
1170                     listeners.add(new HeuristicsTracing(
1171                             new FileBasedVisualizationTool(
1172                                     this.whereToWriteFiles + "-heuristics")));
1173                 }
1174             }
1175 
1176             else if (this.chartBased) {
1177 
1178                 if (this.solverVisu != null) {
1179                     this.solverVisu.end();
1180                 }
1181 
1182                 this.solverVisu = new JChartBasedSolverVisualisation(
1183                         this.visuPreferences);
1184 
1185                 ((JChartBasedSolverVisualisation) this.solverVisu)
1186                         .setnVar(this.solver.nVars());
1187                 if (this.visuPreferences.isDisplayClausesEvaluation()) {
1188                     listeners
1189                             .add(new LearnedTracing(
1190                                     new ChartBasedVisualizationTool(
1191                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1192                                                     .getClausesEvaluationTrace())));
1193                 }
1194                 if (this.visuPreferences.isDisplayClausesSize()) {
1195                     listeners
1196                             .add(new LearnedClausesSizeTracing(
1197                                     new ChartBasedVisualizationTool(
1198                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1199                                                     .getLearnedClausesSizeTrace()),
1200                                     new ChartBasedVisualizationTool(
1201                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1202                                                     .getLearnedClausesSizeRestartTrace()),
1203                                     new ChartBasedVisualizationTool(
1204                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1205                                                     .getLearnedClausesSizeCleanTrace())));
1206                 }
1207                 if (this.visuPreferences.isDisplayConflictsDecision()) {
1208                     listeners
1209                             .add(new ConflictLevelTracing(
1210                                     new ChartBasedVisualizationTool(
1211                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1212                                                     .getConflictLevelTrace()),
1213                                     new ChartBasedVisualizationTool(
1214                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1215                                                     .getConflictLevelRestartTrace()),
1216                                     new ChartBasedVisualizationTool(
1217                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1218                                                     .getConflictLevelCleanTrace())));
1219                 }
1220                 if (this.visuPreferences.isDisplayConflictsTrail()) {
1221                     listeners
1222                             .add(new ConflictDepthTracing(
1223                                     new ChartBasedVisualizationTool(
1224                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1225                                                     .getConflictDepthTrace()),
1226                                     new ChartBasedVisualizationTool(
1227                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1228                                                     .getConflictDepthRestartTrace()),
1229                                     new ChartBasedVisualizationTool(
1230                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1231                                                     .getConflictDepthCleanTrace())));
1232                 }
1233                 if (this.visuPreferences.isDisplayDecisionIndexes()) {
1234                     listeners
1235                             .add(new DecisionTracing(
1236                                     new ChartBasedVisualizationTool(
1237                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1238                                                     .getPositiveDecisionTrace()),
1239                                     new ChartBasedVisualizationTool(
1240                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1241                                                     .getNegativeDecisionTrace()),
1242                                     new ChartBasedVisualizationTool(
1243                                             new TraceComposite(
1244                                                     ((JChartBasedSolverVisualisation) this.solverVisu)
1245                                                             .getRestartPosDecisionTrace(),
1246                                                     ((JChartBasedSolverVisualisation) this.solverVisu)
1247                                                             .getRestartNegDecisionTrace())),
1248                                     new ChartBasedVisualizationTool(
1249                                             new TraceComposite(
1250                                                     ((JChartBasedSolverVisualisation) this.solverVisu)
1251                                                             .getCleanPosDecisionTrace(),
1252                                                     ((JChartBasedSolverVisualisation) this.solverVisu)
1253                                                             .getCleanNegDecisionTrace()))));
1254                 }
1255                 if (this.visuPreferences.isDisplaySpeed()) {
1256                     listeners
1257                             .add(new SpeedTracing(
1258                                     new ChartBasedVisualizationTool(
1259                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1260                                                     .getSpeedTrace()),
1261                                     new ChartBasedVisualizationTool(
1262                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1263                                                     .getSpeedCleanTrace()),
1264                                     new ChartBasedVisualizationTool(
1265                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1266                                                     .getSpeedRestartTrace())));
1267                 }
1268                 if (this.visuPreferences.isDisplayVariablesEvaluation()) {
1269                     listeners
1270                             .add(new HeuristicsTracing(
1271                                     new ChartBasedVisualizationTool(
1272                                             ((JChartBasedSolverVisualisation) this.solverVisu)
1273                                                     .getHeuristicsTrace())));
1274                 }
1275             }
1276 
1277         }
1278         listeners.add(this);
1279 
1280         this.solver.setSearchListener(new MultiTracing<ISolverService>(listeners));
1281 
1282     }
1283 
1284     public int getNVar() {
1285         if (this.solver != null) {
1286             return this.solver.nVars();
1287         }
1288         return 0;
1289     }
1290 
1291     public void setPhaseSelectionStrategy(IPhaseSelectionStrategy phase) {
1292         this.telecomStrategy.setPhaseSelectionStrategy(phase);
1293         log("Told the solver to apply a new phase strategy :"
1294                 + phase.getClass().getSimpleName());
1295     }
1296 
1297     public void shouldRestartNow() {
1298         this.telecomStrategy.setHasClickedOnRestart(true);
1299     }
1300 
1301     public void setRestartStrategy(RestartStrategy strategy) {
1302         this.telecomStrategy.setRestartStrategy(strategy);
1303         log("Set Restart to " + strategy);
1304     }
1305 
1306     public RestartStrategy getRestartStrategy() {
1307         return this.telecomStrategy.getRestartStrategy();
1308     }
1309 
1310     public SearchParams getSearchParams() {
1311         return this.telecomStrategy.getSearchParams();
1312     }
1313 
1314     public SolverStats getSolverStats() {
1315         return this.telecomStrategy.getSolverStats();
1316     }
1317 
1318     public void init(SearchParams params, SolverStats stats) {
1319         this.telecomStrategy.init(params, stats);
1320         log("Init restart with params");
1321     }
1322 
1323     public void setNbClausesAtWhichWeShouldClean(int nbConflicts) {
1324         this.telecomStrategy.setNbClausesAtWhichWeShouldClean(nbConflicts);
1325         log("Changed number of conflicts before cleaning to " + nbConflicts);
1326     }
1327 
1328     public void setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy() {
1329         this.telecomStrategy
1330                 .setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy(true);
1331         log("Solver now cleans clauses every "
1332                 + this.cleanPanel.getCleanSliderValue()
1333                 + " conflicts and bases evaluation of clauses on activity");
1334     }
1335 
1336     public void setLearnedDeletionStrategyTypeToSolver(
1337             LearnedConstraintsEvaluationType type) {
1338         ((ICDCL<?>) this.solver.getSolvingEngine())
1339                 .setLearnedConstraintsDeletionStrategy(this.telecomStrategy,
1340                         type);
1341         log("Changed clauses evaluation type to " + type);
1342     }
1343 
1344     public LearnedConstraintsEvaluationType getLearnedConstraintsEvaluationType() {
1345         return LearnedConstraintsEvaluationType.ACTIVITY;
1346     }
1347 
1348     public void shouldCleanNow() {
1349         log("Told the solver to clean");
1350         this.telecomStrategy.setHasClickedOnClean(true);
1351     }
1352 
1353     public void setKeepSolverHot(boolean keepHot) {
1354         this.solver.setKeepSolverHot(keepHot);
1355         if (keepHot) {
1356             log("Keep hot solver is now activated");
1357         } else {
1358             log("Keep hot solver is now desactivated");
1359         }
1360     }
1361 
1362     public boolean isGnuplotBased() {
1363         return this.gnuplotBased;
1364     }
1365 
1366     public void setGnuplotBased(boolean gnuplotBased) {
1367         this.gnuplotBased = gnuplotBased;
1368     }
1369 
1370     public boolean isChartBased() {
1371         return this.chartBased;
1372     }
1373 
1374     public void setChartBased(boolean chartBased) {
1375         this.chartBased = chartBased;
1376     }
1377 
1378     public boolean isPlotActivated() {
1379         return this.isPlotActivated;
1380     }
1381 
1382     public void setPlotActivated(boolean isPlotActivated) {
1383         this.isPlotActivated = isPlotActivated;
1384     }
1385 
1386     public void setRandomWalkProba(double proba) {
1387         this.randomWalk.setProbability(proba);
1388         log("Set probability to " + proba);
1389     }
1390 
1391     public void setSimplifier(SimplificationType type) {
1392         ((ICDCL<?>) this.solver.getSolvingEngine()).setSimplifier(type);
1393         log("Told the solver to use " + type);
1394     }
1395 
1396     public List<String> getListOfSolvers() {
1397         ASolverFactory<?> factory;
1398 
1399         List<String> result = new ArrayList<String>();
1400 
1401         factory = org.sat4j.minisat.SolverFactory.instance();
1402         for (String s : factory.solverNames()) {
1403             result.add(MINISAT_PREFIX + "." + s);
1404         }
1405 
1406         factory = org.sat4j.pb.SolverFactory.instance();
1407         for (String s : factory.solverNames()) {
1408             result.add(PB_PREFIX + "." + s);
1409         }
1410 
1411         Collections.sort(result);
1412 
1413         factory = org.sat4j.maxsat.SolverFactory.instance();
1414         for (String s : factory.solverNames()) {
1415             result.add(MAXSAT_PREFIX + "." + s);
1416         }
1417 
1418         Collections.sort(result);
1419 
1420         return result;
1421     }
1422 
1423     public List<String> getListOfSatSolvers() {
1424         ASolverFactory<?> factory;
1425 
1426         List<String> result = new ArrayList<String>();
1427 
1428         factory = org.sat4j.minisat.SolverFactory.instance();
1429         for (String s : factory.solverNames()) {
1430             result.add(MINISAT_PREFIX + "." + s);
1431         }
1432         Collections.sort(result);
1433 
1434         return result;
1435     }
1436 
1437     public List<String> getListOfPBSolvers() {
1438         ASolverFactory<?> factory;
1439 
1440         List<String> result = new ArrayList<String>();
1441 
1442         factory = org.sat4j.pb.SolverFactory.instance();
1443         for (String s : factory.solverNames()) {
1444             result.add(PB_PREFIX + "." + s);
1445         }
1446         Collections.sort(result);
1447 
1448         return result;
1449     }
1450 
1451     public List<String> getListOfMaxsatSolvers() {
1452         ASolverFactory<?> factory;
1453 
1454         List<String> result = new ArrayList<String>();
1455 
1456         factory = org.sat4j.pb.SolverFactory.instance();
1457         for (String s : factory.solverNames()) {
1458             result.add(MAXSAT_PREFIX + "." + s);
1459         }
1460         Collections.sort(result);
1461 
1462         return result;
1463     }
1464 
1465     public List<EncodingStrategy> getListOfEncodings(String typeOfConstraint) {
1466         List<EncodingStrategy> v = new ArrayList<EncodingStrategy>();
1467 
1468         v.add(EncodingStrategy.NATIVE);
1469 
1470         if (typeOfConstraint.equals(AT_MOST_K)
1471                 || typeOfConstraint.equals(AT_MOST_1)) {
1472             v.add(EncodingStrategy.BINARY);
1473             v.add(EncodingStrategy.BINOMIAL);
1474             v.add(EncodingStrategy.COMMANDER);
1475         }
1476         if (typeOfConstraint.equals(AT_MOST_K)) {
1477             v.add(EncodingStrategy.SEQUENTIAL);
1478         }
1479         if (typeOfConstraint.equals(AT_MOST_1)
1480                 || typeOfConstraint.equals(EXACTLY_1)) {
1481             v.add(EncodingStrategy.LADDER);
1482         }
1483         if (typeOfConstraint.equals(AT_MOST_1)) {
1484             v.add(EncodingStrategy.PRODUCT);
1485         }
1486 
1487         return v;
1488     }
1489 
1490     public void log(String message) {
1491         logsameline(message + "\n");
1492     }
1493 
1494     public void logsameline(String message) {
1495         if (this.console != null) {
1496             this.console.append(message);
1497             this.console.setCaretPosition(this.console.getDocument()
1498                     .getLength());
1499             this.console.repaint();
1500         }
1501         this.repaint();
1502     }
1503 
1504     public void openFileChooser() {
1505         JFileChooser fc = new JFileChooser();
1506         int returnVal = fc.showDialog(this, "Choose instance");
1507         if (returnVal == JFileChooser.APPROVE_OPTION) {
1508             File file = fc.getSelectedFile();
1509             this.instancePath = file.getAbsolutePath();
1510             this.instancePathField.setText(this.instancePath);
1511             updateListOfSolvers();
1512         }
1513     }
1514 
1515     protected Reader createReader(ISolver theSolver, String problemname) {
1516         InstanceReader instance = new InstanceReader(theSolver);
1517         switch (problemType) {
1518         case CNF_MAXSAT:
1519         case WCNF_MAXSAT:
1520             instance = new MSInstanceReader((WeightedMaxSatDecorator) theSolver);
1521             break;
1522         case PB_OPT:
1523         case PB_SAT:
1524             instance = new PBInstanceReader((IPBSolver) theSolver);
1525             break;
1526         case CNF_SAT:
1527             instance = new InstanceReader(theSolver);
1528             break;
1529         }
1530 
1531         return instance;
1532     }
1533 
1534     public void updateListOfSolvers() {
1535         List<String> theList = new ArrayList<String>();
1536         String defaultSolver = "";
1537 
1538         if (instancePath == null || instancePath.length() == 0) {
1539             theList = getListOfSolvers();
1540             defaultSolver = "minisat.Default";
1541             problemType = ProblemType.CNF_SAT;
1542             equivalenceCB.setEnabled(false);
1543             lowerCB.setEnabled(false);
1544         } else if (instancePath.endsWith(".cnf")) {
1545             optimisationModeCB.setEnabled(true);
1546             if (optimizationMode) {
1547                 theList.addAll(getListOfMaxsatSolvers());
1548                 theList.addAll(getListOfPBSolvers());
1549                 defaultSolver = "maxsat.Default";
1550                 equivalenceCB.setEnabled(true);
1551                 lowerCB.setEnabled(true);
1552                 problemType = ProblemType.CNF_MAXSAT;
1553                 log("cnf file + opt => pb/maxsat solvers");
1554             } else {
1555                 theList.addAll(getListOfSatSolvers());
1556                 theList.addAll(getListOfPBSolvers());
1557                 defaultSolver = "minisat.Default";
1558                 log("cnf file + non opt => sat/pb solvers");
1559                 problemType = ProblemType.CNF_SAT;
1560                 equivalenceCB.setEnabled(false);
1561                 lowerCB.setEnabled(false);
1562             }
1563         } else if (instancePath.endsWith(".opb")) {
1564             optimisationModeCB.setEnabled(true);
1565             theList.addAll(getListOfPBSolvers());
1566             defaultSolver = "pb.Default";
1567             if (optimizationMode) {
1568                 problemType = ProblemType.PB_OPT;
1569                 equivalenceCB.setEnabled(true);
1570                 lowerCB.setEnabled(true);
1571             } else {
1572                 problemType = ProblemType.PB_SAT;
1573                 equivalenceCB.setEnabled(false);
1574                 lowerCB.setEnabled(false);
1575             }
1576             log("opb file => pb solvers");
1577         } else if (instancePath.endsWith(".wcnf")) {
1578             equivalenceCB.setEnabled(true);
1579             lowerCB.setEnabled(true);
1580             theList.addAll(getListOfMaxsatSolvers());
1581             theList.addAll(getListOfPBSolvers());
1582             defaultSolver = "maxsat.Default";
1583             optimisationModeCB.setSelected(true);
1584             optimisationModeCB.setEnabled(false);
1585             problemType = ProblemType.WCNF_MAXSAT;
1586             log("wcnf file => pb/maxsat solvers");
1587         }
1588         this.listeSolvers.setModel(new DefaultComboBoxModel(theList.toArray()));
1589         this.listeSolvers.setSelectedItem(defaultSolver);
1590         this.choixSolverPanel.repaint();
1591     }
1592 
1593     public void setInstancePanelEnabled(boolean enabled) {
1594         this.instanceLabel.setEnabled(enabled);
1595         this.instancePathField.setEnabled(enabled);
1596         this.browseButton.setEnabled(enabled);
1597         this.instancePanel.repaint();
1598     }
1599 
1600     public void setChoixSolverPanelEnabled(boolean enabled) {
1601         this.listeSolvers.setEnabled(enabled);
1602         this.choixSolver.setEnabled(enabled);
1603         this.solverLineParamLineRadio.setEnabled(enabled);
1604         this.solverLineParamRemoteRadio.setEnabled(enabled);
1605         this.solverListParamListRadio.setEnabled(enabled);
1606         this.solverListParamRemoteRadio.setEnabled(enabled);
1607         this.choixSolverPanel.repaint();
1608     }
1609 
1610     public void setSolverVisualisation(SolverVisualisation visu) {
1611         this.solverVisu = visu;
1612     }
1613 
1614     public void activateGnuplotTracing(boolean b) {
1615         this.isPlotActivated = b;
1616         if (this.solver != null) {
1617             initSearchListeners();
1618         }
1619     }
1620 
1621     public void startVisu() {
1622         this.solverVisu.start();
1623     }
1624 
1625     public void stopVisu() {
1626         this.solverVisu.end();
1627     }
1628 
1629     public VisuPreferences getGnuplotPreferences() {
1630         return this.visuPreferences;
1631     }
1632 
1633     public void setGnuplotPreferences(VisuPreferences gnuplotPreferences) {
1634         this.visuPreferences = gnuplotPreferences;
1635     }
1636 
1637     public DetailedCommandPanel getThis() {
1638         return this;
1639     }
1640 
1641     public ISolver getSolver() {
1642         return (ISolver) this.problem;
1643     }
1644 
1645     private long begin, end;
1646     private int propagationsCounter;
1647 
1648     private int conflictCounter;
1649 
1650     private PrintStream outSolutionFound;
1651 
1652     private void updateWriter() {
1653         try {
1654             this.outSolutionFound = new PrintStream(new FileOutputStream(
1655                     this.whereToWriteFiles + "_solutions.dat"));
1656         } catch (FileNotFoundException e) {
1657             this.outSolutionFound = System.out;
1658         }
1659 
1660     }
1661 
1662     public void init(ISolverService solverService) {
1663         this.conflictCounter = 0;
1664     }
1665 
1666     public void assuming(int p) {
1667     }
1668 
1669     public void propagating(int p, IConstr reason) {
1670         this.end = System.currentTimeMillis();
1671         if (this.end - this.begin >= 2000) {
1672             long tmp = this.end - this.begin;
1673 
1674             this.cleanPanel.setSpeedLabeltext(this.propagationsCounter / tmp
1675                     * 1000 + "");
1676 
1677             this.begin = System.currentTimeMillis();
1678             this.propagationsCounter = 0;
1679         }
1680         this.propagationsCounter++;
1681     }
1682 
1683     public void backtracking(int p) {
1684     }
1685 
1686     public void adding(int p) {
1687     }
1688 
1689     public void learn(IConstr c) {
1690     }
1691 
1692     public void delete(int[] clause) {
1693     }
1694 
1695     public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
1696         this.conflictCounter++;
1697     }
1698 
1699     public void conflictFound(int p) {
1700     }
1701 
1702     public void solutionFound(int[] model,RandomAccessModel lazyModel) {
1703         log("Found a solution !! ");
1704         logsameline(this.stringWriter.toString());
1705         this.stringWriter.getBuffer().delete(0,
1706                 this.stringWriter.getBuffer().length());
1707         this.outSolutionFound.println(this.conflictCounter + "\t");
1708     }
1709 
1710     public void beginLoop() {
1711     }
1712 
1713     public void start() {
1714     }
1715 
1716     public void end(Lbool result) {
1717     }
1718 
1719     public void restarting() {
1720         this.end = System.currentTimeMillis();
1721         if (this.end != this.begin) {
1722             this.cleanPanel.setSpeedLabeltext(this.propagationsCounter
1723                     / (this.end - this.begin) * 1000 + "");
1724         }
1725     }
1726 
1727     public void backjump(int backjumpLevel) {
1728     }
1729 
1730     public void cleaning() {
1731         this.end = System.currentTimeMillis();
1732         this.cleanPanel.setSpeedLabeltext(this.propagationsCounter
1733                 / (this.end - this.begin) * 1000 + "");
1734     }
1735 
1736     public class MyTabbedPane extends JTabbedPane {
1737         private static final long serialVersionUID = 1L;
1738 
1739         @Override
1740         public void setSelectedIndex(int index) {
1741             if (this.getTabCount() == 5 && index == 4) {
1742                 if (DetailedCommandPanel.this.solver != null
1743                         && DetailedCommandPanel.this.startStopButton.getText()
1744                                 .equals(STOP)) {
1745                     String s = DetailedCommandPanel.this.solver.toString();
1746                     String res = DetailedCommandPanel.this.solver.toString();
1747                     int j = 0;
1748                     for (int i = 0; i < s.length(); i++) {
1749                         if (s.charAt(i) != '\n') {
1750                             j++;
1751                         } else {
1752                             j = 0;
1753                         }
1754                         if (j > 80) {
1755                             res = new StringBuffer(res).insert(i, '\n')
1756                                     .toString();
1757                             j = 0;
1758                         }
1759                     }
1760                     DetailedCommandPanel.this.textArea.setText(res);
1761                     DetailedCommandPanel.this.textArea.setEditable(false);
1762                     DetailedCommandPanel.this.textArea.repaint();
1763                     DetailedCommandPanel.this.aboutSolverPanel
1764                             .paint(DetailedCommandPanel.this.aboutSolverPanel
1765                                     .getGraphics());
1766                     DetailedCommandPanel.this.aboutSolverPanel.repaint();
1767                 } else {
1768                     DetailedCommandPanel.this.textArea
1769                             .setText("No solver is running at the moment");
1770                     DetailedCommandPanel.this.textArea.repaint();
1771                     DetailedCommandPanel.this.textArea.setEditable(false);
1772                     DetailedCommandPanel.this.aboutSolverPanel
1773                             .paint(DetailedCommandPanel.this.aboutSolverPanel
1774                                     .getGraphics());
1775                     DetailedCommandPanel.this.aboutSolverPanel.repaint();
1776                 }
1777             }
1778             super.setSelectedIndex(index);
1779         };
1780     }
1781 
1782 }