Combining linear programming and satisfiability solving for resource planning

2001 ◽  
Vol 16 (1) ◽  
pp. 85-99 ◽  
Author(s):  
STEVEN A. WOLFMAN ◽  
DANIEL S. WELD
Keyword(s):  
Artificial Intelligence ◽  
Linear Programming ◽  
Operations Research ◽  
Resource Planning ◽  
Expressive Power ◽  
Conjunctive Normal Form ◽  
Simplex Algorithm ◽  
Form Representation ◽  
Satisfiability Solving ◽  
Planning Problems

Compilation to Boolean satisfiability has become a powerful paradigm for solving artificial intelligence problems. However, domains that require metric reasoning cannot be compiled efficiently to satisfiability even if they would otherwise benefit from compilation. We address this problem by combining techniques from the artificial intelligence and operations research communities. In particular, we introduce the LCNF (Linear Conjunctive Normal Form) representation that combines propositional logic with metric constraints. We present LPSAT (Linear Programming plus SATisfiability), an engine that solves LCNF problems by interleaving calls to an incremental Simplex algorithm with systematic satisfaction methods. We explore several techniques for enhancing LPSAT's efficiency and expressive power by adjusting the interaction between the satisfiability and linear programming components of LPSAT. Next, we describe a compiler that converts metric resource planning problems into LCNF for processing by LPSAT. Finally, the experimental section of the paper explores several optimisations to LPSAT, including learning from constraint failure and randomised cutoffs.

Artificial intelligence and operations research: challenges and opportunities in planning and scheduling

2000 ◽  
Vol 15 (1) ◽  
pp. 1-10 ◽  
Author(s):  
CARLA P. GOMES
Keyword(s):  
Artificial Intelligence ◽  
Real World ◽  
Operations Research ◽  
Expressive Power ◽  
Combinatorial Problems ◽  
The Other ◽  
Planning And Scheduling ◽  
Functional Programming Languages ◽  
Other Hand ◽  
Real World Problems

Both the Artificial Intelligence (AI) and the Operations Research (OR) communities are interested in developing techniques for solving hard combinatorial problems, in particular in the domain of planning and scheduling. AI approaches encompass a rich collection of knowledge representation formalisms for dealing with a wide variety of real-world problems. Some examples are constraint programming representations, logical formalisms, declarative and functional programming languages such as Prolog and Lisp, Bayesian models, rule-based formalism, etc. The downside of such rich representations is that in general they lead to intractable problems, and we therefore often cannot use such formalisms for handling realistic size problems. OR, on the other hand, has focused on more tractable representations, such as linear programming formulations. OR-based techniques have demonstrated the ability to identify optimal and locally optimal solutions for well-defined problem spaces. In general, however, OR solutions are restricted to rigid models with limited expressive power. AI techniques, on the other hand, provide richer and more flexible representations of real-world problems, supporting efficient constraint-based reasoning mechanisms as well as mixed initiative frameworks, which allow the human expertise to be in the loop. The challenge lies in providing representations that are expressive enough to describe real-world problems and at the same time guaranteeing good and fast solutions.

scholarly journals On the intersection of AI and OR

2001 ◽  
Vol 16 (1) ◽  
pp. 1-4 ◽  
Author(s):  
CARLA P. GOMES
Keyword(s):  
Artificial Intelligence ◽  
Linear Programming ◽  
Mathematical Programming ◽  
Operations Research ◽  
Planning And Scheduling ◽  
Search Techniques ◽  
The Individual ◽  
Inference Methods

This is the second of two special issues focusing on the integration of artificial intelligence (AI) and operations research (OR) techniques for solving hard computational problems, with an emphasis on planning and scheduling. Both the AI and the OR community have developed sophisticated techniques to tackle such challenging problems. OR has relied heavily on mathematical programming formulations such as integer and linear programming, while AI has developed constraint-based search techniques and inference methods. Recently, we have seen a convergence of ideas, drawing on the individual strengths of these paradigms.

NEURAL NETWORKS AND LINEAR PROGRAMMING FOR THE SATISFIABILITY PROBLEM

1999 ◽  
Vol 09 (01) ◽  
pp. 11-25
Author(s):  
ANGELO MONFROGLIO
Keyword(s):  
Neural Networks ◽  
Linear Programming ◽  
Optimization Problem ◽  
Propositional Calculus ◽  
Conjunctive Normal Form ◽  
Simplex Algorithm ◽  
Satisfiability Problem ◽  
Huge Amount ◽  
Algorithm Performance ◽  
Linear Programming Formulation

First a Linear Programming formulation is considered for the satisfiability problem, in particular for the satisfaction of a Conjunctive Normal Form in the Propositional Calculus and the Simplex algorithm for solving the optimization problem. The use of Recurrent Neural Networks is then described for choosing the best pivot positions and greatly improving the algorithm performance. The result of hard cases testing is reported and shows that the technique can be useful even if it requires a huge amount of size for the constraint array and Neural Network Data Input.

scholarly journals Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL

2020 ◽  
pp. 233-250
Author(s):  
Ralph Bottesch ◽  
Max W. Haslbeck ◽  
Alban Reynaud ◽  
René Thiemann
Keyword(s):  
Linear Programming ◽  
Branch And Bound ◽  
Decision Procedure ◽  
Simplex Algorithm ◽  
Upper Bounds ◽  
Mixed Integer ◽  
Small Solution ◽  
Code Generator ◽  
Integer Arithmetic ◽  
Termination Proofs

AbstractWe implement a decision procedure for linear mixed integer arithmetic and formally verify its soundness in Isabelle/HOL. We further integrate this procedure into one application, namely into , a formally verified certifier to check untrusted termination proofs. This checking involves assertions of unsatisfiability of linear integer inequalities; previously, only a sufficient criterion for such checks was supported. To verify the soundness of the decision procedure, we first formalize the proof that every satisfiable set of linear integer inequalities also has a small solution, and give explicit upper bounds. To this end we mechanize several important theorems on linear programming, including statements on integrality and bounds. The procedure itself is then implemented as a branch-and-bound algorithm, and is available in several languages via Isabelle’s code generator. It internally relies upon an adapted version of an existing verified incremental simplex algorithm.

scholarly journals A Monotonic Build-Up Simplex Algorithm for Linear Programming

1994 ◽  
Vol 42 (3) ◽  
pp. 556-561 ◽  
Author(s):  
Kurt M. Anstreicher ◽  
Tamás Terlaky
Keyword(s):  
Linear Programming ◽  
Simplex Algorithm
Sign in / Sign up

Export Citation Format

Share Document