DEPQBF(1) General Commands Manual DEPQBF(1)NAME
depqbf - a solver for quantified boolean formulae
SYNOPSIS
depqbf [options ...] [NUM] [FILE]
DESCRIPTION
depqbf is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form. It is based on the DPLL algorithm
for QBF with conflict-driven clause and solution-driven cube learning. By analyzing the structure of a formula, DepQBF tries to identify
independent variables. In addition to other benefits, this often increases freedom for decision making. See also the JSAT system descrip-
tion of DepQBF 0.1 from QBFEVAL'10 for references and a brief outline of the idea.
depqbf reads QBF formulas in QDIMACS format. If FILE is not given, it reads its input from stdin. It complies with input/output standards
as required by QBFEVAL'10.
OPTIONS
depqbf accepts the following options:
-h, --help
Print usage information.
--version
Print version.
--pretty-print
Only parse and print formula.
-v Increase verbosity incrementally.
NUM Optional: time-out after NUM seconds.
FILE Optional: read input from FILE.
EXIT STATUS
The exit status is 10 if the QBF formula given as input is satisfiable, and 20 if it is unsatisfiable; any other exit code indicates that
the formula was not solved.
SEE ALSO picosat(1), minisat(1), clasp(1).
AUTHOR
depqbf was written by Florian Lonsing <florian.lonsing@jku.at>.
This manual page was written by Thomas Krennwallner <tkren@kr.tuwien.ac.at>,
August 26, 2011 DEPQBF(1)
Check Out this Related Man Page
LPS2PBES(1) User Commands LPS2PBES(1)NAME
lps2pbes - generate a PBES from an LPS and a state formula
SYNOPSIS
lps2pbes [OPTION]... --formula=FILE [INFILE [OUTFILE]]
DESCRIPTION
Convert the state formula in FILE and the LPS in INFILE to a parameterised boolean equation system (PBES) and save it to OUTFILE. If OUT-
FILE is not present, stdout is used. If INFILE is not present, stdin is used.
OPTIONS
OPTION can be any of the following:
-fFILE, --formula=FILE
use the state formula from FILE
-t, --timed
use the timed version of the algorithm, even for untimed LPS's
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
Standard options:
-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
--log-level=LEVEL
display intermediate messages up to and including level
-h, --help
display help information
--version
display version information
AUTHOR
Written by Wieger Wesselink; Tim Willemse.
REPORTING BUGS
Report bugs at <http://www.mcrl2.org/issuetracker>.
COPYRIGHT
Copyright (C) 2012 Technische Universiteit Eindhoven.
This is free software. You may redistribute copies of it under the terms of the Boost Software License
<http://www.boost.org/LICENSE_1_0.txt>. There is NO WARRANTY, to the extent permitted by law.
SEE ALSO
See also the manual at <http://www.mcrl2.org/mcrl2/wiki/index.php/User_manual/lps2pbes>.
lps2pbes mCRL2 toolset 201202.0 (Release) April 2012 LPS2PBES(1)
For people who want to pull a number of lines from a long file using a specific formula
n (number of iterations in a loop)
a (offset number)
b (stretch factor)
example with n {1..100}
for (( n=1; n<101; n++ )); do awk -v n=$n 'NR==a+(b*n)' a=0 b=1 inputfile >>outputfile (2 Replies)
Hello,
Im trying to work on a small script for a formula converting temperatures, Celsius to fahrenheit.
I have a formula, and it works.... it works every way I try it. But it keeps giving me the wrong results every time with expr.
The formula for C to F would be:
divide by 5, multiply by... (12 Replies)
Hi, I was wondering if someone could help with what is probably a fairly easy problem. I have two variables, i is between 1-5, j is between 11-15
I'd like to produce this:
1_11
2_12
3_13
4_14
5_15
Each number goes up incrementally with the other.
But my shoddy code is not... (5 Replies)
Dear Masters,
Kindly need your helps for this issue..
I face a formula as a picture...
the input file is
A DEPT Vp Vs rho VPperVS
------------------------ ------------ ------------ ------------
700 151.9218 121.9269 ... (11 Replies)