OKlibrary  0.2.1.6
PseudoBoolean.hpp File Reference

Plans regarding building of pseudo-boolean solvers and libraries. More...

Go to the source code of this file.


Detailed Description

Plans regarding building of pseudo-boolean solvers and libraries.

Todo:
Install pseudo-boolean solvers
Todo:
Tools for PB -> SAT translation
  • We need a list of all tools for the conversion of pseudo-boolean problems to SAT.
  • The input format for the pseudo-boolean problems should be the OPB format used at the pseudo-boolean competitions; see http://www.cril.univ-artois.fr/PB11/format.pdf.
  • Tools:
    • BoolVar allows generation of SAT instances from a pseudo-boolean problem modelled in Java; see "BoolVar/PB".
    • minisat+ allows the translation of a pseudo-boolean problem to SAT using the option "-cnf=":
      • minisat+ also offers the ability to customise how constraints are translated (adders, sorting networks, bdds, "mixed" etc) using the options -ca, -cs, -cb and -cm.
      • However, minisat+ doesn't currently support the new OPB format; see "minisat+ input format".
  • All tools should be installed in the OKlibrary.
Todo:
minisat+ input format
  • The minisat+ input format is the OPB format from PB05; see http://www.cril.univ-artois.fr/PB05/solver_req.html.
  • Since PB06, the "*" between a variable and it's weight has been removed.
  • So instead of writing a pseudo-boolean constraint like:
    +1 * x1 +2 * x2 >= 1;
       
    the format is now:
    +1 x1 +2 x2 >= 1;
       
  • There are several options:
    • A patch for minisat+ which allows it to read the new format.
    • A wrapper script around minisat+ which converts the new OPB format to the old.
    • A script or manual conversion of new OPB files to old, before using minisat+.
  • The best option is to patch minisat+, as the old format is no longer used and we, as users of minisat+, shouldn't have to worry about such things.
Todo:
borg-pb
Todo:
clasp:
Todo:
SAT4J:
Todo:
BoolVar/PB
  • http://arxiv.org/abs/1103.3954 describes a java library for translating pseudo-boolean constraints to CNF.
  • The website is at http://boolvar.sourceforge.net/.
  • BoolVar is a Java library with which one constructs a pseudo-boolean problem in Java, and then translates this to either SAT or OPB (the pseudo-boolean competition format).
  • The ".jar" file is a collection of class files packaged together. It is already compiled.
  • BoolVar does not support the reading in of OPB files and output of a SAT problem as an application.
  • To convert OPB files to SAT, we would have to write an OPB file parser and then use this to construct a pseudo-boolean problem in the BoolVar system.
  • The source is available at http://sourceforge.net/projects/boolvar/files/ .
  • Hopefully the source can be compiled by gcj, and then we can use the applications created.
  • See "Gcj" in Buildsystem/ExternalSources/SpecialBuilds/plans/PseudoBoolean.hpp.
  • Also see "Supporting Java" in Buildsystem/ExternalSources/SpecialBuilds/plans/general.hpp.
  • BoolVar can be compiled to it's constituent class files using gcj-4.5.2 (system-installation on MG's machine):
    ExternalSources/builds/SAT/BoolVar> jar xvf ../../../sources/SAT/BoolVar/BoolVar.0.0.jar
    ExternalSources/builds/SAT/BoolVar> find ./ -iname "*.java" -exec gcj -C {} +
       
  • BoolVar also compiles to native C++ object files:
    ExternalSources/builds/SAT/BoolVar> jar xvf ../../../sources/SAT/BoolVar/BoolVar.0.0.jar
    ExternalSources/builds/SAT/BoolVar> find ./ -iname "*.java" -exec gcj -c {} +
    ExternalSources/builds/SAT/BoolVar> ls
    AtLeastOne.o  Cardinality.o  Conjunction.o  ExactlyOne.o  Literal.o       NotEqual.o   Problem.o         Sorting.o      UnitLowerOrEq.o  Variable.o
    AtMostOne.o   Clause.o       Constraint.o   Function.o    LowerOrEqual.o  PbProblem.o  Propagate.o       Sum.o          UnitNotEqual.o
    boolvar       CnfProblem.o   Disjunction.o  Interval.o    META-INF        PBterm.o     RootConstraint.o  UnitAllDiff.o  UnitSum.o
       
    which creates a ".o" file for each ".java" file.
  • We can then link against these functions from C++ using gcj's Compiled Native Interface (CNI); see http://en.wikipedia.org/wiki/GNU_Compiler_for_Java .

Definition in file PseudoBoolean.hpp.