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.