Examples that Use the B-Prolog Interface to LP/MLP and SAT

Built-ins for modeling for linear programming/mixed integer programming and SAT solvers

• Domain declaration
  • X :: L..U -- integer domains
  • [X1,...,Xn] :: L..U
  • lp_domain(X,L,U) -- real domains
  • lp_domain([X1,...,Xn],L,U)
• Constraints
  • $\ E -- not
  • E $/\ E -- and
  • E $\/ E -- or
  • E $=> E -- imply
  • E $<=> E -- equivalent
  • E $\ E -- xor
  • E $= E -- arithmetic constraints
  • E $\= E
  • E $>= E
  • E $> E
  • E $=< E
  • E $< E
  • $alldifferent(L) -- global
• Solver invocation calls
  • lp_solve(Options,L), lp_solve(L), ip_solve(Options,L), or ip_solve(L)

    
     Start the LP/MIP solver to find a valuation for the variables L 
    	 that satisfies the accumulated constraints. The following options 
    	 are allowed:
    	 min(Exp) -- minimize Exp
    	 max(Exp) -- maximize Exp
    	 dump -- dump the model in some format
     file(File) -- dump the model to File
     format(lp) -- dump the model in the CPLEX lp format 
     format(clp) -- dump the model in CLP format (IP models only)
    

  • sat_solve(Options,L) or sat_solve(L)

    
    	 Start the Sat solver to find a valuation for the variables L
    	 that satisfies the accumulated constraints. If no SAT solver 
    	 is embedded into B-Prolog, the OS command 'satsolver' must be 
    	 provided to invoke a SAT solver on a CNF file. The following 
    	 options are allowed:
    	 min(Exp) -- minimize Exp
    	 max(Exp) -- maximize Exp
    	 dump -- dump the set of constraints in the CNF format
    	 file(File) -- dump to File
    	 cmp_time(Time) -- the compile time is Time
    	 report(Pred) -- call Pred each time a valuation for Vs is 
    	 found during optimization.
    

  • cp_solve(Options,L) or cp_solve(L)

    
    	 Start the CP solver to find a valuation for the variables L
    	 that satisfies the accumulated constraints, where Options may
    	 contain only min(Exp) or max(Exp).
    

  • ip_solve_all(L,Bag), sat_solve_all(L,Bag), cp_solve_all(L,Bag)

    
     Find all the solutions of L using a designated solver.