sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-05-11T12:15:13Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/1Use a specific data structure for binary clauses compatible with reason simpl...2018-05-11T12:15:13ZDaniel Le BerreUse a specific data structure for binary clauses compatible with reason simplificationThe support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because th...The support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.https://gitlab.ow2.org/sat4j/sat4j/-/issues/19Allow creation of clauses, cardinality and pseudo boolean constraints using a...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of clauses, cardinality and pseudo boolean constraints using arrays of primitive typeWhen creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.When creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.https://gitlab.ow2.org/sat4j/sat4j/-/issues/24Add statistics about SAT/UNSAT calls2018-05-11T12:15:13ZDaniel Le BerreAdd statistics about SAT/UNSAT callsWhen doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.When doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.https://gitlab.ow2.org/sat4j/sat4j/-/issues/25Allow input string to be read properly using InputStream or Reader2018-05-11T12:15:13ZDaniel Le BerreAllow input string to be read properly using InputStream or ReaderFor the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is ...For the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is not supported in some readers.
Not a big deal to fix, but need to be done properly.https://gitlab.ow2.org/sat4j/sat4j/-/issues/28Allow easy explanation for OPB file2022-04-09T17:42:39ZDaniel Le BerreAllow easy explanation for OPB fileCurrently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to...Currently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to easily display the unsat core in terms of constraints number (might not be that good because an equality constraint is splitted into 2 constraints).https://gitlab.ow2.org/sat4j/sat4j/-/issues/62Expose solver stats and info programatically2018-05-11T12:15:13ZPablo AbadExpose solver stats and info programaticallyCurrently, the Solver class exposes several methods that can be used to get insight into different solver metrics:
void printStat(PrintWriter out, String prefix)
void printStat(PrintStream out, String prefix)
int nVars()
void printLearnt...Currently, the Solver class exposes several methods that can be used to get insight into different solver metrics:
void printStat(PrintWriter out, String prefix)
void printStat(PrintStream out, String prefix)
int nVars()
void printLearntClausesInfos(PrintWriter out, String prefix)
void printInfos(PrintWriter out, String prefix)
Map<String, Number> getStat()
long getTimeoutMs()
int realNumberOfVariables()
int nConstraints()
While some of these methods may be used while building constraints, most of them return information about the problem being represented and status of the solving process.
Furthermore, some of this information can't be accessed programatically, but printed to a Stream or Writer.
The proposal would be to create an interface that provides methods for retrieving all these information and add a method in Solver that returns an implementation of this interface. Ideally, all the printXXX methods could be moved from Solver into another class that would receive this interface.
Here is a possible draft of this interface:
public interface SolverStats {
int numberOfVars();
int realNumberOfVars();
int nContraints();
void observeStats(StatObserver observer);
void observeConstraintTypes(ConstraintTypeObserver observer);
void observeLearnedConstraintTypes(ConstraintTypeObserver observer);
}
public interface StatObserver {
public void observe(String stat, Number value);
// or a method per value type
}
public interface ConstraintTypeObserver {
public void observe(String type, int count);
}
https://gitlab.ow2.org/sat4j/sat4j/-/issues/93Find a way to factorize the various settings for the solvers2018-07-07T05:11:52ZDaniel Le BerreFind a way to factorize the various settings for the solversThe PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not...The PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not have any dependency to commons CLI, so is a bit different from the two others.
However, we need to find a central class to perform the configuration of solvers: note that in sat package, the configuration of the solvers is done twice, one in DetailedCommandPanel and one in Launcher.
https://gitlab.ow2.org/sat4j/sat4j/-/issues/97Allow Sat4j statistics to be visible using JMX2018-07-07T05:11:52ZDaniel Le BerreAllow Sat4j statistics to be visible using JMXJava allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we c...Java allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we could at least use it for providing an access to the solver statistics while the solver is running.https://gitlab.ow2.org/sat4j/sat4j/-/issues/102API for using an OPB string spec2018-07-07T05:11:52ZMihai BarbuceanuAPI for using an OPB string specHi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going throug...Hi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going through the command line.
Many Thanks,
Mihaihttps://gitlab.ow2.org/sat4j/sat4j/-/issues/114Implement reusable trail2018-07-07T05:11:52ZDaniel Le BerreImplement reusable trailReusable trail is proven to be efficient (used in Lingeling and Knuth SAT13 CDCL solver).
In order to implement future improvements in Sat4j, implementing such feature becomes mandatory.
All details are available here:
http://jsat.ewi.tu...Reusable trail is proven to be efficient (used in Lingeling and Knuth SAT13 CDCL solver).
In order to implement future improvements in Sat4j, implementing such feature becomes mandatory.
All details are available here:
http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_11_vanderTak.pdfhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/115Fix issue in Minisat Expensive Simplification2018-07-07T05:11:53ZDaniel Le BerreFix issue in Minisat Expensive SimplificationThe minisat expensive simplification procedure has been fixed recently to correct a bug that could make the solver spend too much time during conflict minimization. The issue was raised by Allen Van Gelder in a paper (SAT'11 ?).
The code...The minisat expensive simplification procedure has been fixed recently to correct a bug that could make the solver spend too much time during conflict minimization. The issue was raised by Allen Van Gelder in a paper (SAT'11 ?).
The code of minisat available in github contains the fix. We might want to implement our own.
It might be the case that such issue arrises when using cardinality constraints. Need to investigate further.https://gitlab.ow2.org/sat4j/sat4j/-/issues/116Implement decision conflict replacement proposed by Knuth2018-07-07T05:11:53ZDaniel Le BerreImplement decision conflict replacement proposed by KnuthDonald Knuth proposes in SAT13 to swap a regular conflict by a conflict clause containing only decision variables under certain conditions. It is not clear if such proposal works in practice.
All details available here:
http://www-cs-fac...Donald Knuth proposes in SAT13 to swap a regular conflict by a conflict clause containing only decision variables under certain conditions. It is not clear if such proposal works in practice.
All details available here:
http://www-cs-faculty.stanford.edu/~uno/programs/sat13.whttps://gitlab.ow2.org/sat4j/sat4j/-/issues/122Allow the definitions of levels of the heuristic2018-07-07T05:11:53ZDaniel Le BerreAllow the definitions of levels of the heuristicIn some cases, domain knowledge allow the user of the solver to rank the variables to guide the solver.
It would be nice to provide a way to provide such information to Sat4j users.In some cases, domain knowledge allow the user of the solver to rank the variables to guide the solver.
It would be nice to provide a way to provide such information to Sat4j users.3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/134Throw IllegalStateException when calling unsatExplanation to avoid NPE.2018-07-07T05:11:53ZDaniel Le BerreThrow IllegalStateException when calling unsatExplanation to avoid NPE.If a user calls unsatExplanation() on a SAT problem, or before the solver has run, he will get an NPE.
One should throw an IllegalStateException with an appropriate message instead.If a user calls unsatExplanation() on a SAT problem, or before the solver has run, he will get an NPE.
One should throw an IllegalStateException with an appropriate message instead.